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

We show that the normal form of the Taylor expansion of a $\lambda$-term is isomorphic to its B\"ohm 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...

Full description

Bibliographic Details
Main Authors: Federico Olimpieri, Lionel Vaux Auclair
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2022-01-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/6701/pdf