- Title: Telescopic mappings in typed lambda calculus
- Author: N.G. de Bruijn
- Date: 1991
- URL: https://www.win.tue.nl/automath/archive/pdf/aut103.pdf
In Automath (see [I] ,[3] ,[4]) the implementation of mathematical functions is a simple matter if the domain of the function is a type, but becomes slightly awkward if that domain is a part of a type.
For example, if the type is the type of real numbers (let us assume it has been called "real"), and if we take as the domain the interval $`(3,7)`$ (the set of all $`x`$ with $`3 < x < 7`$), then the function value at a point $`b`$ can be obtained only if apart from the value of $`b`$ we provide a proof for $`3 < b < 7`$.
Let us call the class of all such proofs $`P(b)`$.
So for a function call we have to provide two expressions, $`b`$ and $`u`$, and to establish the typings $`b : \text{real}, u : P(b)`$.
Therefore the partial function has to be implemented in Automath by means of two lambda abstractors instead of a single one.
With the Automath notation for typed lambdas (see section 2); these abstractors are $`[x : \text{real}][y : P(x)]`$.
If, for example, the function is complex-valued, then its type becomes $`[x : \text{real}][y : P(x)]\text{compl}`$.
In such a sequence of two or more abstractors the type of the second may depend on the variable in the first, the type of the third may depend on the variables of the first two, etc.
It reminds of an old-fashioned telescope consisting of a sequence of segments of decreasing width, where each segment can be shifted into the previous one.
That is why these abstractor strings are called telescopes.
