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:7837@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20160421T110000
DTEND;TZID=Europe/Paris:20160421T110000
DTSTAMP:20241120T204848Z
URL:https://www.i2m.univ-amu.fr/evenements/b-reduction-et-developpement-de
 -taylor-2-3/
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.\n\nIl reste à établir que\, dans
  ce 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 l
 es combinaisons linéaires de termes avec ressources\, contenant la traduc
 tion de la β-réduction via le développement de Taylor\, tout en étant 
 compatible avec la normalisation des termes avec ressources. Je détailler
 ai cette solution en expliquant les problèmes qui se posent et les choix 
 techniques qui permettent de les résoudre. J’expliquerai également en 
 quoi cette approche permet d’introduire une alternative robuste aux arbr
 es de Böhm comme notion de forme normale généralisée\, dans un cadre n
 on uniforme.
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