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

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.

• There are non-terminating lambda-expressions. There are infinitely many ways to express the same function. How would quote deal with it? – Dmitri Urbanowicz Jun 27 '18 at 8:07
• What is the domain and codomain of the quote function? If the domain is ASTs, then such a quotation function exists trivially, so that's probably not what you have in mind. – Martin Berger Jun 27 '18 at 12:30

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.

• That connects a lot of dots. – MaiaVictor Jun 28 '18 at 3:22

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.

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

• Thanks for your answer Barry. And welcome in our cstheory community :) – Łukasz Lew Oct 1 '20 at 2:36
• Glad to join in, Łukasz. – Barry Jay Oct 2 '20 at 22:25