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:8450@i2m.univ-amu.fr DTSTART;TZID=Europe/Paris:20240610T140000 DTEND;TZID=Europe/Paris:20240610T180000 DTSTAMP:20241209T160900Z URL:https://www.i2m.univ-amu.fr/evenements/soutenance-de-these-taylor-appr oximation-and-infinitary-lambda-calculi/ SUMMARY:Rémy Cerda (I2M\, Aix-Marseille Université): Taylor Approximation and Infinitary Lambda-Calculi DESCRIPTION:Rémy Cerda: Composition du jury\n\n Ugo DAL LAGO Rapporteur P rofessore ordinario\, Università di Bologna\n Giulio MANZONETTO Préside nt\, Professeur des universités\, Université Paris Cité\n Laurent REGN IER Co-directeur\, Professeur des universités\, Aix-Marseille université \n Christine TASSON Rapporteure\, Professeure des universités\, ISAE-Sup aero\n Femke VAN RAAMSDONK Examinatrice\, Assistant professor\, Vrije uni versiteit Amsterdam\n Lionel VAUX AUCLAIR Directeur\, Maître de confére nces\, Aix-Marseille université\n\nRésumé\nDepuis son introduction par Church\, le λ-calcul a joué un rôle majeur dans un\nsiècle de dévelop pement de l’informatique théorique et de la logique mathéma-\ntique\, mais aussi dans la naissance de nombreux langages de programmation.\nUne p ropriété cruciale de ce calcul est qu’il n’est pas normalisant en g énéral\, de\nsorte qu’un intérêt croissant a porté sur la recherche d’approximations de sa dy-\nnamique. Les outils « classiques » d’ap proximation\, nés dans les années 1970\ndans le sillage des sémantiques de Scott\, sont essentiellement sémantiques.\nLes outils basés sur le d éveloppement de Taylor\, introduits dans les années 2000\npar Ehrhard et Regnier\, proposent à l’inverse une approximation dynamique\nde la β- réduction. Puisant ses inspirations dans le développement de la logique\ nlinéaire\, le développement de Taylor traduit le λ-calcul vers un calc ul « à res-\nsources » multilinéaire\, muni d’une dynamique finitair e. Un théorème de com-\nmutation (entre approximation et normalisation) fait notamment l’efficacité de\ncette approche\, et en justifie le succ ès. La notion d’arbre de Böhm est centrale\ndans cette ligne de recher che. Née de l’idée que les termes normalisants ne sont\npas les seuls à avoir un sens calculatoire\, elle généralise la notion de forme nor-\ nmale en constituant une «forme normale à l’infini». La compréhensio n de la\nnature coinductive de cet objet a mené dans les années 1990 à l’introduction de\nλ-calculs infinitaires. Dans ces calculs\, les terme s et les réductions peuvent être\ninfinis et\, dans le cas du calcul 001 -infinitaire\, l’arbre de Böhm est la notion de\nforme normale à l’i nfini (sans guillemets).\nL’idée qui guide cette thèse est que le λ-c alcul 001-infinitaire se prête à une gé-\nnéralisation de l’approxim ation de Taylor où\, en particulier\, les arbres de Böhm\nseraient des «citoyens ordinaires». L’approximation du λ-calcul fini\, et notam-\n ment de ses propriétés de normalisation\, devient alors un cas particuli er de\nl’approximation du calcul infinitaire. Cela est permis par le pri ncipal résultat\nde la thèse\, qui établit que la dynamique du calcul à ressources est à même de\nsimuler la β-réduction infinitaire via le développement de Taylor.\nPour arriver à ce résultat\, nous faisons d ’abord un détour par une présentation\nabstraite d’une syntaxe « mi xte » (inductive et coinductive) d’ordre supérieur\,\nà l’aide d’ un formalisme nominal généralisant des travaux récents introduisant\nde s types coalgébriques avec lieurs. Cela nous permet de définir formellem ent\ndes coalgèbres de classes d’α-équivalence de λ-termes infinitai res (chapitre 1).\nDans un second temps\, nous définissons les λ-calculs infinitaires à l’aide d’une\nprésentation coinductive\, puis nous r appelons leurs principales propriétés ainsi\nque leur lien avec les thé ories classiques de l’approximation de la β-réduction\n(chapitre 2). E nsuite\, nous présentons le λ-calcul à ressources comme un cas\nparticu lier d’une réécriture avec sommes\, et distinguons ses versions qualit a-\ntive et quantitative (chapitre 3).\nDans une seconde partie consacrée à l’approximation de Taylor propre-\nment dite\, nous commençons par introduire le développement de Taylor\ndes λ-termes infinitaires et prou vons le théorème de simulation annoncé\,\ndans sa forme qualitative pui s quantitative. Nous démontrons l’efficacité de\nce théorème en le m ettant à l’œuvre\, proposant notamment une nouvelle\npreuve de conflue nce pour le λ-calcul 001-infinitaire (chapitre 4). Nous nous\npenchons é galement sur la conservativité de la propriété de simulation\, et\ndém ontrons l’existence surprenante d’un contre-exemple à cette propriét é\nréciproque (chapitre 5). Enfin\, nous étendons notre travail au cadr e paresseux\,\nc’est-à-dire celui du λ-calcul 101-infinitaire\, et nou s démontrons un théorème\nde commutation pour les arbres de Lévy-Longo (chapitre 6).\nMots-clefs : lambda-calcul\, réécriture infinitaire\, d éveloppement de Taylor\,\napproximation de programmes\, sémantique quant itative.\nAbstract\nSince its introduction by Church\, the λ-calculus has played a major role in a cen-\ntury of development in theoretical compute r science and mathematical logic\,\nas well as in the birth of numerous pr ogramming languages. A crucial prop-\nerty of this calculus is that it is not normalising in general\, leading to growing\ninterest in finding appro ximations to its dynamics. The ‘classic’ approximation\ntools\, which emerged in the 1970s in the wake of Scott’s semantics\, are essen-\ntial ly semantic. The tools based on Taylor expansion\, introduced in the 2000s \nby Ehrhard and Regnier\, conversely propose a dynamic approximation of t he\nβ-reduction. Drawing its inspiration from the development of linear l ogic\, Tay-\nlor expansion translates the λ-calculus into a multilinear ‘resource’ calculus\,\nequipped with finitary dynamics. A commutation theorem (between approxi-\nmation and normalisation) makes this approach p articularly effective\, and jus-\ntifies its success.\nThe notion of Böhm tree is central to this line of research. Associated with the\nidea that normalising terms are not the only computationally meaningful ones\,\nit g eneralises the notion of normal form by constituting an ‘infinite normal \nform’. Understanding the coinductive nature of this object led in the 1990s to\nthe introduction of infinitary λ-calculi. In these calculi\, te rms and reductions\ncan be infinite and\, in the case of the 001-infinitar y calculus\, the Böhm tree is\nthe notion of infinite normal form (withou t quotes).\nThe idea guiding this thesis is that the 001-infinitary λ-cal culus lends itself to\na generalisation of the Taylor approximation where\ , in particular\, Böhm trees\nwould be ‘ordinary citizens’. The appro ximation of the finite λ-calculus\, and\nin particular its normalisation properties\, then becomes a special case of the\napproximation of the infi nitary calculus. This is enabled by the main result of\nthe thesis\, which establishes that the dynamics of the resource calculus is able\nto simula te the infinitary β-reduction via Taylor expansion.\nTo arrive at this re sult\, we first make a diversion via an abstract presentation\nof a ‘mix ed’ (inductive and coinductive) higher-order syntax\, using a nominal\nf ormalism generalising recent work on coalgebraic types with binders. This\ nallows us to formally define coalgebras of α-equivalence classes of infi nite λ-\nterms (chapter 1). In a second step\, we define infinitary λ-ca lculi using a coin-\nductive presentation\, then recall their main propert ies as well as their connec-\ntion with classical theories of approximatio n of the β-reduction (chapter 2).\nThen\, we present the resource λ-calc ulus as a special case of a rewriting with\nsums\, and distinguish its qua litative and quantitative flavours (chapter 3). CATEGORIES:Soutenance de thèse,AGLR,Logique et Interactions LOCATION:Luminy\, Campus des Sciences de Luminy\, Marseille\, 13009\, Franc e X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=Campus des Sciences de Lumi ny\, Marseille\, 13009\, France;X-APPLE-RADIUS=100;X-TITLE=Luminy:geo:0,0 END:VEVENT BEGIN:VTIMEZONE TZID:Europe/Paris X-LIC-LOCATION:Europe/Paris BEGIN:DAYLIGHT DTSTART:20240331T030000 TZOFFSETFROM:+0100 TZOFFSETTO:+0200 TZNAME:CEST END:DAYLIGHT END:VTIMEZONE END:VCALENDAR