# On an automatic translation of typed lambda calculus in untyped lambda calculus

I have a question regarding the "compilation" of typed lambda calculus in untyped lambda calculus.

Take for example the inductive definition of lists, with introduction rules: and: We can automatically derive the elimination rule and the computation rules (here omitted as they are well known), as well as an interpretation in untyped lambda calculus: $[\![Nil]\!] = \lambda x.\lambda y.x$ $[\![Cons(a,l)]\!] = \lambda x.\lambda y.y \> [\![a]\!] \> ([\![l]\!] \> x \> y)$ $[\![ListCata(l,n,c)]\!] = [\![l]\!] \>[\![n]\!] \> [\![c]\!]$

This "automatic definition" can be done, up to my knowledge, if we are defining an inductive type $I$ such that the occurrences of $I$ in the premises of the introduction rules are strictly positive.

It seems to me that the power of this method lies in his generality: I only have to state my introduction rules and I automatically get a translation in a language I know how to execute, in this case untyped lambda calculus.

Now, I'm interested in a better understanding of this type of translation, in different directions:

• Where has this schema been first defined? Are there papers regarding this translation?
• What are the limits of this approach? For example, can I extend this process to more inductive types, to co-inductive types, to a polymorphic lambda calculus, to dependent types?
• What if I'd like, given a definition of an inductive type, "compile" the code in, for example, SKI calculus, or another system of symbolic computation? Is there any work done in this direction?
• Could one hope to give an inductive definition of the underlying "computational machine", and get automatically a translation?

The translation process you describe is often referred to as the Church encoding, and it is rather well studied in the literature. Presumably it was first given by Church soon after the definition of the $\lambda$-calculus itself (some details appear here).
The question about compiling to combinators seems unrelated. Of course it is possible to represent every $\lambda$-term using combinators, and using combinators as targets for compilation is another well studied subject (see e.g. Hudak & Kranz).
• I'm not sure what you mean by the last question. By definition, a combinatorially complete set of combinators comes equiped with a translation from pure $\lambda$-terms. On thing I can say, is that the many many papers of Olivier Danvy on the theory of abstract machines for the $\lambda$-calculus may be of interest, see e.g. A Functional Correspondence between Evaluators and Abstract Machines.