Is it possible to create a "quote" function that, given a native λ-term, returns its λ-encoded representation?

Question

Suppose we implement the λ-calculus inside the λ-calculus itself with λ-encodings and Bruijn indices:

Lam = λ body .        λ Lam . λ App . λ Var . Lam body
App = λ fun . λ arg . λ Lam . λ App . λ Var . App fun arg
Var = λ idx .         λ Lam . λ App . λ Var . Var idx

Is it possible to implement a quote() function that, given a native term, returns its own λ-encoded representation? For example:

quote(λ f . λ x . f (f x)) 

Would return:

Lam (Lam (App (Var 1) (App (Var 1) (Var 0))))

If not, is it possible if given a type?

quote(Arr(Arr(T,T),Arr(T,T)), λ f . λ x . f (f x)))

Where Arr(Arr(T,T),Arr(T,T)) represents that the term we want to quote has the following STLC type: (o -> o) -> o -> o.

Answer 1

Neel is exactly right. The simplest example of extensionality is $\eta$ equality. I.e. there is no well typed lambda term that will differentiate between $(\lambda x . f x)$ and $ (f) $.

The situation is similar in Sharing Graphs. The same $\eta$ equality is presented in the first figure of Lemma 3.4 in 'A denotational semantics for the symmetric interaction combinators'. Moreover the second figure in the same presents second $\eta$ equality dealing with 'contraction'. As the lemma states, both equalities together are complete.

In one 'quote' definition it is enough to suspend every cut in lambda calculus i.e. application. Section 3.3 in Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega defines it in System-F setting. (In terms of Sharing Graphs, it is enough to 'suspend' every cut i.e. put a node between 2 principal ports facing each other).

If you want to go a bit outside of lambda calculus, take a look at A combinatory account of internal structure. It might be just what you need.

There's a chance that Pure Pattern calculus will be relevant to your goals as well.

For implementations have a look at Barry Jay's github.

Answer 2

No, this is not possible, assuming you want to go from an arbitrary lambda term to some first-order AST.

The lambda calculus is extensional, which means that the lambda calculus cannot distinguish between two lambda-terms which are behaviourally equivalent. Eg, if you have terms implementing quick sort and merge sort, then no other lambda-term can distinguish them, since they are both extensionally the same function. As a result, full quotation is impossible, since it should let you get different source code for those two terms.

Answer 3

Łukasz Lew and Neel Krishnaswami are right; quotation is well-defined only for terms in normal form. This excludes recursive programs in traditional lambda-calculus but not in combinatory logic, since its naive interpretation of lambda-abstraction always produces normal forms (by breaking all redexes). Now that quotation is well-defined, we can ask if it is definable as a combinator. The answer is no, since combinatory logic, like lambda-calculus, is extensional, so cannot distinguish, for example, the identity functions SKK and SKS.

However, quotation is definable in tree-calculus, as are various self-interpreters. All this is covered in my forthcoming book "Reflective Programs in Tree Calculus" (Springer-Nature). Some frontmatter is already available at Tweets on Trees with the coq proofs of all theorems at the same site, but one level up. There is also a refereed paper Recursive Programs in Normal Form.