Seminario di Logica - F. Olimpieri

Link identifier #identifier__69134-1Link identifier #identifier__61281-2

15 Giugno 2018, ore 11:30
Dipartimento di Matematica e Fisica, Aula 311
Largo San Leonardo Murialdo, 1 - Roma

On the Taylor expansion of lambda-terms and the groupoid structure of their approximants

Federico Olimpieri (I2m, Aix-Marseille Universite')

Abstract. We show that the normal form of the Taylor expansion of a lambda-term is isomorphic to its Böhm tree, improving Ehrhard and Regnier’s original proof along three independent directions. First, we simplify the final step of the proof by following the left reduction strategy directly in the resource calculus, avoiding to introduce an abstract machine ad-hoc. We also introduce a groupoid of permutations of copies of arguments in a rigid variant of the resource calculus, and relate the coefficients of Taylor expansion with this structure, while Ehrhard and Regnier worked with groups of permutations of occurrences of variables. Finally, we extend all the results to a non-deterministic setting: by contrast with previous attempts, we show that the uniformity property that was crucial in Ehrhard and Regnier’s approach can be preserved in this setting.

Per informazioni:
Vito Michele Abrusci
Link identifier