In the form above you can input:
T;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.