Logical Approaches to Computational Barriers

Böhm trees, Krivine machine and the Taylor expansion of ordinary lambda-terms

Speaker:
| Thomas Ehrhard |

Author(s): |
Thomas Ehrhard and Laurent Regnier |

We show that, given an ordinary lambda-term M and a normal resource lambda-term u which appears in the normal form of the Taylor expansion of M, the unique resource term t of the Taylor expansion of M whose normal form contains u can be obtained by running the Krivine abstract machine on M. This result, combined with a previous result of the same authors, alows to show that, in the ordinary lambda-calculus, Taylor expansion and normalization commute - by normalizing an ordinary lambda-term, we mean here computing its Böhm tree.

websites: Arnold Beckmann | 2006-04-20 |