Taylor expansion of lambda-terms

 `T`: `S0`:
Overview Syntax rules Examples

In the form above you can input:

• a lambda-term `T`;
• a simple term `S0` appearing in the Taylor expansion of the Böhm tree of `T`.

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.