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

<p>The lambda calculus is <em>extensional</em>, 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. </p>

CC BY-SA 4.0
2018-06-27T13:54:00.080Z
2018-06-27T13:54:00.080Z
Neel Krishnaswami
<p>Ł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 <em>not</em> in combinatory logic, since its naive interpretation of lambda-abstraction <em>always</em> 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.</p>
<p>However, quotation <em>is</em> definable in tree-calculus, as are various self-interpreters. All this is covered in my forthcoming book &quot;Reflective Programs in Tree Calculus&quot; (Springer-Nature). Some frontmatter is already available at <a href="https://github.com/barry-jay-personal/tree-calculus/tweets_on_trees.pdf" rel="nofollow noreferrer">Tweets on Trees</a> with the coq proofs of all theorems at the same site, but one level up. There is also a refereed paper <a href="https://dl.acm.org/doi/10.1145/3162067" rel="nofollow noreferrer">Recursive Programs in Normal Form</a>.</p>

CC BY-SA 4.0
2020-10-01T02:36:25.977Z
Thanks for your answer Barry. And welcome in our cstheory community :)
Łukasz Lew
CC BY-SA 4.0
2020-10-02T22:25:06.383Z
Glad to join in, Łukasz.
Barry Jay
CC BY-SA 4.0
2020-09-30T21:57:55.420Z
2020-09-30T21:57:55.420Z
Barry Jay
<p>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) $. </p>

<p>The situation is similar in Sharing Graphs. 
The same $\eta$ equality is presented in the first figure of Lemma 3.4 in <a href="http://www.lipn.univ-paris13.fr/~mazza/papers/CombSem-MSCS.pdf" rel="noreferrer"> 'A denotational semantics for the symmetric interaction combinators'</a>. Moreover the second figure in the same presents second $\eta$ equality dealing with 'contraction'. As the lemma states, both equalities together are complete.</p>

<p>In one 'quote' definition it is enough to suspend every cut in lambda calculus i.e. application. Section 3.3 in <a href="http://compilers.cs.ucla.edu/popl16/popl16-full.pdf" rel="noreferrer">Breaking Through the Normalization Barrier:
A Self-Interpreter for F-omega</a> 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).</p>

<p>If you want to go a bit outside of lambda calculus, take a look at 
<a href="https://www.researchgate.net/publication/220315256_A_combinatory_account_of_internal_structure" rel="noreferrer">A combinatory account of internal structure</a>. It might be just what you need.</p>

<p>There's a chance that <a href="https://link.springer.com/content/pdf/10.1007/11693024_8.pdf" rel="noreferrer">Pure Pattern calculus</a> will be relevant to your goals as well.</p>

<p>For implementations have a look at <a href="https://github.com/Barry-Jay?tab=repositories" rel="noreferrer">Barry Jay's github</a>.</p>

CC BY-SA 4.0
2018-06-28T03:22:09.017Z
That connects a lot of dots.
MaiaVictor
CC BY-SA 4.0
2018-06-27T19:25:30.767Z
2018-06-27T19:25:30.767Z
Łukasz Lew
<p>Suppose we implement the λ-calculus inside the λ-calculus itself with λ-encodings and Bruijn indices:</p>

<pre><code>Lam = λ body .        λ Lam . λ App . λ Var . Lam body
App = λ fun . λ arg . λ Lam . λ App . λ Var . App fun arg
Var = λ idx .         λ Lam . λ App . λ Var . Var idx
</code></pre>

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

<pre><code>quote(λ f . λ x . f (f x)) 
</code></pre>

<p>Would return:</p>

<pre><code>Lam (Lam (App (Var 1) (App (Var 1) (Var 0))))
</code></pre>

<p>If not, is it possible if given a type?</p>

<pre><code>quote(Arr(Arr(T,T),Arr(T,T)), λ f . λ x . f (f x)))
</code></pre>

<p>Where <code>Arr(Arr(T,T),Arr(T,T))</code> represents that the term we want to quote has the following STLC type: <code>(o -&gt; o) -&gt; o -&gt; o</code>.</p>

CC BY-SA 4.0
2018-06-27T08:07:34.973Z
There are non-terminating lambda-expressions. There are infinitely many ways to express the same function. How would quote deal with it?
Dmitri Urbanowicz
CC BY-SA 4.0
2018-06-27T12:30:40.590Z
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
<type-theory><lambda-calculus>
Is it possible to create a "quote" function that, given a native λ-term, returns its λ-encoded representation?
MaiaVictor
# Is it possible to create a "quote" function that, given a native λ-term, returns its λ-encoded representation?

(Asked by: username_0 on 2018-06-27)

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.

**Tags:** type-theory, lambda-calculus

> **Comments:**
> **username_1**: There are non-terminating lambda-expressions. There are infinitely many ways to express the same function. How would quote deal with it?  
> **username_2**: 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.  

---

## 3 answers

### Answer by username_5 on 2018-06-27. Score: 8 | Accepted answer

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'](http://www.lipn.univ-paris13.fr/~mazza/papers/CombSem-MSCS.pdf). 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](http://compilers.cs.ucla.edu/popl16/popl16-full.pdf) 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](https://www.researchgate.net/publication/220315256_A_combinatory_account_of_internal_structure). It might be just what you need.

There's a chance that [Pure Pattern calculus](https://link.springer.com/content/pdf/10.1007/11693024_8.pdf) will be relevant to your goals as well.

For implementations have a look at [username_4's github](https://github.com/Barry-Jay?tab=repositories).

> **Comments:**
> **username_0**: That connects a lot of dots.  

---

### Answer by username_3 on 2018-06-27. Score: 9

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 by username_4 on 2020-09-30. Score: 3

username_5 and username_3 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](https://github.com/barry-jay-personal/tree-calculus/tweets_on_trees.pdf) 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](https://dl.acm.org/doi/10.1145/3162067).

> **Comments:**
> **username_5**: Thanks for your answer Barry. And welcome in our cstheory community :)  
> **username_4**: Glad to join in, Łukasz.  

---

