|Böhm trees, Krivine machine and the Taylor expansion of ordinary lambda-terms |
Auteur(s): Ehrhard Thomas, Regnier Laurent
Conference: Second Conference on Computability in Europe, CiE 2006 (Swansea, GB, 2006-06-29)
Ref HAL: hal-00150273_v1
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