×

Non finitely generated types and \(\lambda\)-terms combinatoric representation cost. (English. Abridged French version) Zbl 0962.03009

Summary: We consider here two linked questions about the representation of \(\lambda\)-terms from combinators (i.e., from closed \(\lambda\)-terms).
The first one was raised by R. Statman and deals with simply typed \(\lambda\)-calculus: can we find for a given type \(A\) a finite set of typed combinators generating through applications every closed \(\lambda\)-term of the type \(A\) up to \(\beta\eta\)-equivalence? We show that this cannot be done for the type: \(\mathbb{L}= (o\to o)\to o\), \((o^2\to o)\to o\).
The second question is about pure \(\lambda\)-calculus: how far from a pure \(\lambda\)-term \(t\) is any of its combinatoric representations \(M\), the distance between them being measured by the length of the reduction: \(M\twoheadrightarrow t?\) We prove that given any integer \(k\) and any finite set \({\mathcal C}\) of pure combinators there is a closed normal \(\lambda\)-term \(t\) such that the \(\beta\)-normalization of any of its combinatoric representations from \({\mathcal C}\) requires more than \(k\) complete developments.

MSC:

03B40 Combinatory logic and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI