BEGIN:VCALENDAR VERSION:2.0 PRODID:-//wp-events-plugin.com//7.2.3.1//EN TZID:Europe/Paris X-WR-TIMEZONE:Europe/Paris BEGIN:VEVENT UID:8209@i2m.univ-amu.fr DTSTART;TZID=Europe/Paris:20141215T110000 DTEND;TZID=Europe/Paris:20141215T130000 DTSTAMP:20241210T143809Z URL:https://www.i2m.univ-amu.fr/evenements/une-etude-combinatoire-du-lambd a-calcul-avec-ressources-uniforme/ SUMMARY:Jean-Baptiste Midez (I2M\, Aix-Marseille Université): Une étude c ombinatoire du lambda-calcul avec ressources uniforme DESCRIPTION:Jean-Baptiste Midez: Thèse de doctorat en Mathématiques\n\nSo us la direction de Laurent Régnier.\n\nSoutenue le 15-12-2014\n\nà Aix-M arseille \, dans le cadre de Ecole Doctorale Mathématiques et Informatiq ue de Marseille (Marseille) .\n\nLe président du jury était Thomas Ehrha rd.\n\nLe jury était composé de Michele Pagani\, Lionel Vaux.\n\nLes rap porteurs étaient Daniel Hirschkoff\, Lorenzo Tortora de falco.\n\nLe lamb da-calcul avec ressources est une variante du lambda-calcul fondée sur la linéarité : les lambda-termes avec ressources sont aux lambda-termes ce que sont les polynômes aux fonctions réelles\, c'est à dire des approx imations multi-linéaires. En particulier les réductions dans le lambda-c alcul avec ressources peuvent être vues comme des approximations des beta -réductions\, mais la contrainte de linéarite a des conséquences import antes\, notamment la forte normalisation de la réduction avec ressources. Pour ainsi dire\, la beta-réduction est obtenue par passage à la limite des réductions avec ressources qui l'approximent. Cette thèse étudie l es aspects combinatoires\, très riches\, du lambda-calcul avec ressources . On commence par définir précisément la notion de réduction avec ress ource associée à une beta-réduction: étant donné un lambda-terme t\, un approximant s de celui-ci et t' une beta-réduction de t\, on lui assoc ie une réduction avec ressources (appelée gamma-réduction) de s qui ré duit les «mêmes» redex que celle de t et produit un ensemble S' d'appro ximants de t'. Cette définition permet de retrouver une preuve légèreme nt plus intuitive de l'un des théorèmes fondamentaux de la théorie\, qu i permet également de le généraliser. Dans un second temps on étudie l es relations «familiales» entre termes avec ressources\, la question cen trale étant de caractériser le fait que deux termes avec ressources sont des réduits d'un même terme. Ce problème central et difficile n'est pa s pleinement résolu\, mais la thèse présente plusieurs résultats prél iminaires et développe les bases d'une théorie pour arriver à cette fin .\n\nA combinatory study of uniforme resource lambda-calculus\n\nThe resou rce lambda-calculus is a variant of lambda-calculus based on linearity: re source lambda-terms are to lambda-terms as polynomials are to real functio ns. In particular reductions in resource lambda-calculus can be viewed as approximations of beta-reductions. But the linearity constraint has import ant consequences\, especially the strong normalisation of resource reducti on. So to speak\, beta-reduction is obtained by passage to the limit of re source reduction which approximates it. This thesis is a study of the comb inatory aspect of resource lambda-calculus. First\, we define precisely th e notion of resource reduction associated to beta-reduction: let t be a la mbda-term\, s an approximant of t and t' a beta-reduction of t\, we associ ate a resource reduction (called gamma-reduction) of s which reducts the " same" redex as the beta-reduction of t and this generates a set S' of appr oximants of t'. This definition allows to find a new proof (who is more in tuitive) of one of the fundamental theorems of this theory and it also all ows to generalize it. Then we study the "family" relations between resourc e lambda-terms. The main question is to characterize the resource lambda-t erms which are reducts of same term. This central problem is hard and not completely resolved\, but this thesis exhibits several preliminary results and lays the foundations of a theory aimed at resolving it.\n\nhttp://www .theses.fr/s120015 ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2 020/01/Jean-Baptiste_Midez.jpg CATEGORIES:Soutenance de thèse,AGLR,Logique et Interactions END:VEVENT BEGIN:VTIMEZONE TZID:Europe/Paris X-LIC-LOCATION:Europe/Paris BEGIN:STANDARD DTSTART:20141026T020000 TZOFFSETFROM:+0200 TZOFFSETTO:+0100 TZNAME:CET END:STANDARD END:VTIMEZONE END:VCALENDAR