6
$\begingroup$

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: Nil introduction and: Cons introduction

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?
Improve this question
$\endgroup$

1 Answer 1

Reset to default
6
$\begingroup$

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).

One way to see it is as a "control inversion", where an instance of pattern matching on an element of an inductive type simply becomes an application of each branch to the term.

This translation doesn't necessarily have to be to the untyped calculus: the usual Church encoding of (positive) data-types in System F results in well-typed terms! In general this extends to polymorphism and dependent types without difficulty, though the induction principles for those types can not be proven inside the type theories themselves! (See e.g. Geuvers for a proof).

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).

Improve this answer
$\endgroup$
2
  • $\begingroup$ As always, thanks for the answer. What about the last question? Could we hope to compile in an arbitrary machine if we give some form of specification? Do you know any work in that direction? $\endgroup$
    – meditans
    Jul 11, 2015 at 22:05
  • $\begingroup$ 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. $\endgroup$
    – cody
    Jul 12, 2015 at 14:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.