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?