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

Auteur(s): Ehrhard Thomas, Regnier Laurent

Conference: Second Conference on Computability in Europe, CiE 2006 (Swansea, GB, 2006-06-29)
Actes de conférence: Logical Approaches to Computational Barriers, vol. p.186-197 (2006)

Ref HAL: hal-00150273_v1
DOI: 10.1007/11780342_20
Exporter : BibTex | endNote

We introduce and study a version of Krivine's machine which provides a precise information about how much of its argument is needed for performing a computation. This information is expressed as a term of a resource lambda-calculus introduced by the authors in a recent article; this calculus can be seen as a fragment of the differential lambda-calculus. We use this machine to show that Taylor expansion of lambda-terms (an operation mapping lambda-terms to generally infinite linear combinations of resource lambda-terms) commutes with Boehm tree computation.

Commentaires: 12 pages