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:7852@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20160331T110000
DTEND;TZID=Europe/Paris:20160331T123000
DTSTAMP:20241120T205552Z
URL:https://www.i2m.univ-amu.fr/evenements/b-reduction-et-developpement-de
 -taylor/
SUMMARY:Lionel Vaux (I2M\, Aix-Marseille Université): β-réduction et dé
 veloppement de Taylor
DESCRIPTION:Lionel Vaux: Ehrhard et Regnier ont montré au milieu des anné
 es 2000 que le développement de Taylor d’un λ-terme pur est toujours n
 ormalisable\, et que sa forme normale correspond exactement à l’arbre d
 e Böhm du λ-terme. Leurs techniques reposent fortement sur une propriét
 é d’uniformité des λ-termes et sont de ce fait assez fragiles : on ne
  peut pas les transposer à des extensions non déterministes par exemple.
  Et d’ailleurs\, en présence de sommes\, le développement de Taylor d
 ’un terme n’est pas toujours normalisable.\nDans des travaux récents 
 avec Michele Pagani et Christine Tasson\, en partie publiés dans FoSSaCS 
 2016\, nous avons donné une caractérisation de la normalisabilité (fort
 e\, faible\, de tête) d’un λ-terme M comme une propriété de finitude
  de son développement de Taylor T(M). Une conséquence (et la motivation 
 principale) de ces travaux est que le développement de Taylor des λ-term
 es normalisables est lui-même normalisable\, et ce y compris dans des var
 iantes non déterministes du λ-calcul.\nIl reste à établir que\, dans c
 e cas\, normalisation et développement de Taylor commutent : NF(T(M)) = T
 (NF(M)). Je propose pour cela de définir une notion de réduction sur les
  combinaisons linéaires de termes avec ressources\, contenant la traducti
 on de la β-réduction via le développement de Taylor\, tout en étant co
 mpatible avec la normalisation des termes avec ressources. Je détaillerai
  cette solution en expliquant les problèmes qui se posent et les choix te
 chniques qui permettent de les résoudre. J’expliquerai également en qu
 oi cette approche permet d’introduire une alternative robuste aux arbres
  de Böhm comme notion de forme normale généralisée\, dans un cadre non
  uniforme.\n
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20160327T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR