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 DOI: 10.1007/11780342_20 Exporter : BibTex | endNote Résumé: 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 |