Joly, Thierry Non finitely generated types and \(\lambda\)-terms combinatoric representation cost. (English. Abridged French version) Zbl 0962.03009 C. R. Acad. Sci., Paris, Sér. I, Math. 331, No. 8, 581-186 (2000). 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 Keywords:representation of \(\lambda\)-terms from combinators; simply typed \(\lambda\)-calculus; pure \(\lambda\)-calculus PDFBibTeX XMLCite \textit{T. Joly}, C. R. Acad. Sci., Paris, Sér. I, Math. 331, No. 8, 581--186 (2000; Zbl 0962.03009) Full Text: DOI