Taylor expansion of lambda-terms

Overview Syntax rules Examples

In the form above you can input:

It returns the simple term S appearing in the Taylor expansion of T whose normal form contains S0.

A brief explanation

(See the paper Uniformity and the Taylor expansion of ordinary lambda-terms for the long version)

Simple terms are particular differential terms that resemble lambda-terms (see the syntax rules); they are built from variables using lambda-abstraction and bunch application, that is application of a simple term to a bunch where a bunch may be viewed as a (commutative) product of simple terms. As in lambda-calculus the bunch application is linear in the function but also (and this is the difference with lambda-calculus) in each factor appearing in the argument bunch.

An approximant of a lambda-term T is a simple term S that appears (with a nonzero coefficient) in the Taylor expansion of T. An approximant of T is more or less the term T in which each application has been replaced by a bunch application. For example [x]<x>{}, [x]<x>x, [x]<x>x^2, ... are the approximants of the term delta=[x](x)x and [f][x]<f>{<f>{}.(<f>x^3)^2} is an approximant of the Church numeral [f][x](f)(f)x.

There is a strong relation between approximants of T and approximants of the normal form T0 of T (more generally the Böhm tree of T). In particular, one may prove that each S0 approximating T0 comes from a unique S approximating T by the reduction rules of the resource calculus, that is by derivation.

In a next paper we will show how one can use an environment machine for call-by-name lambda-calculus to compute this unique S given T and S0. In the meantime we wrote a program in Ocaml that illustrates this. You can try this program using the form above (also see the examples page), browse the Ocaml source or download it.