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`

.

(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.