Computability in Europe 2006
Logical Approaches to Computational Barriers

Special Session Talk:
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

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