Lambda calculus + Church numerals

Neel asked:

Quote:

>Incidentally, for languages with multiple argument functions, is there

>some theory as nice as de Bruijn indices to formalize the frame/offset

>pairs used to build environments there?

Yes indeed. I looked at the problem in the context of Bohm's separability

theorem. The problem arose in the representation of Bohm trees, which are

potentially infinite lambda-terms, represented as layers of head normal forms.

Each layer has the shape \x1 x2 ... xn.h(M1, ..., Mp) where h is the head

variable. The correct extension of de Bruijn indices to this situation is to

represent h with a pair of natural numbers. One names the layer above where h

is bound, a la de Bruijn. The other one indexes in the layer. For instance,

if h is x2, then it is represented as Index(0,2); 0 since h is locally bound, and

2 because the local indexing goes left to right, and NOT right to left as we

would have thought by the de Bruijn analogy. Left to right is the proper

way because we want the indexing to be invariant by eta-expansion.

Details may be found in section 1.7 of my paper "An analysis of Bohm's theorem"

Theoretical Computer Science 121 (1993) 145-167 where all definitions are given

as executable CAML programs - no handvawing with maths, just explicit ML code.

I was very pleased to basically rediscover the ALGOL display mechanism.

It may also be pointed out that I had no difficulty computing on infinite Bohm

trees in a strict language. No flames intended, of course.

--

Gerard Huet

----------------------------------------------

INRIA -- BP 105 -- F-78153 Le Chesnay Cedex

Tel.: +33 1 39 63 54 60 Fax: +33 1 39 63 56 84

WWW: http://pauillac.inria.fr/~huet/index.html

----------------------------------------------