<p>What Neel said, and also the following.</p>

<p>I would like to emphasize (<a href="http://math.andrej.com/2008/02/06/representations-of-uncomputable-and-uncountable-sets/" rel="noreferrer">again</a>, <a href="https://cstheory.stackexchange.com/questions/1037/what-does-it-mean-that-there-are-differing-views-on-how-computations-are-represen/">again</a> and <a href="http://drops.dagstuhl.de/opus/volltexte/2009/2257/" rel="noreferrer">again</a>) that representation of input and output matters. If we are allowed to change representations, we can achieve just about anything (for example, make any given function computable). So, passing from a representation of functions $\mathbb{N} \to \mathbb{N}$ by $\lambda$-terms to a representation by Gödel numbers is <em>not</em> acceptable if our model of computation is $\lambda$-calculus (because then the currying operation becomes uncomputable by $\lambda$-calculus).</p>

<p>A statement which is realizable in the $\lambda$-term model but not in the Turing machine model is "not every function $\mathbb{N} \to \mathbb{N}$ has a Gödel code", which is kind of silly. I will try to come up with a better one and edit this answer.</p>

<hr>

<p><strong>Edit on 2013-10-07:</strong> Here is what I meant by "currying becomes uncomputable". Suppose we use the untyped $\lambda$-calculus as our computational model, but then we decide that we should represent maps $\mathbb{N} \to \mathbb{N}$ with Gödel codes (of Turing machines, encoded as Church numerals). Sounds harmless, right? After all we believe the mantra "Turing machines and $\lambda$-calculus are equivalent".</p>

<p>Well, for this new representation to actually be a valid representation of $\mathbb{N} \to \mathbb{N}$, we need also to realize application and currying (because to "represent functions" means the same thing as "to represent an exponential object"). Specifically, we need a $\lambda$-term $\mathtt{app}$ such that, whenever the Church numeral $\overline{n}$ represents $f : \mathbb{N} \to \mathbb{N}$ then $f(k)$ is represented by $\mathtt{app} \; \overline{n} \; \overline{k}$. (Here I write $\overline{n}$ for the Church numeral representing the number $n$.) Such an $\mathtt{app}$ is readily available because it amounts to an interpreter for Turing machines, implemented in the $\lambda$-calculus.</p>

<p>But how about currying? For that we need the following. Suppose $X$ is a represented set. Given any map $f : X \times \mathbb{N} \to \mathbb{N}$ computed by a $\lambda$-term $t$, we need to show that the transposition $\tilde{f} : X \to (\mathbb{N} \to \mathbb{N})$ is also computed by some $\lambda$-term $s$. But consider the example where $X$ is the set o fmaps $\mathbb{N} \to \mathbb{N}$ represented by $\lambda$-terms, and $f$ is application. Then $\tilde{f}$ would be a map which acts as identity on $\mathbb{N} \to \mathbb{N}$, but its realizer is a $\lambda$-term that converts $\lambda$-terms representing maps $\mathbb{N} \to \mathbb{N}$ to corresponding Gödel codes. Such a $\lambda$-term does not exist (for example because it would be discontinuous in a topological semantic model).</p>

<p>You may attempt to object that I should not have used the specific represented set $X$ of maps $\mathbb{N} \to \mathbb{N}$ represented by $\lambda$-terms, because we "agreed" that those should be represented by Gödel codes. But you would be wrong. First of all, I could have used a different $X$ with a more complicated proof which would elude you but still accomplish the same result. Second of all, $X$ is there in the category and the definition of exponential requires that currying work with respect to <em>all</em> objects. You have to respect the category. You cannot just randomly butcher it and take some objects out (well, you can but then you are a butcher).</p>

CC BY-SA 2.5
2011-03-10T00:52:03.813Z
still waiting for that better example...
Jacques Carette
CC BY-SA 2.5
2011-03-12T21:54:26.300Z
Well, I can think of many statements which are realizable with Turing machines but not with $\lambda$-terms. I suppose you want the opposite. Hmmm.
Andrej Bauer
CC BY-SA 3.0
2013-10-05T23:31:57.767Z
I don't get how currying can become incomputable. You should be able to reuse the s-m-n theorem, since its proof constructs a function on first-order data (naturals). By the Church-Turing thesis, this behavior on naturals can be implemented as a lambda term (which uses native functions internally, but I don't see how that's forbidden). One can similarly prove the u-t-m theorem, so according to [your post](http://math.andrej.com/2008/02/06/representations-of-uncomputable-and-uncountable-sets/) we should be done. What am I missing?
Blaisorblade
CC BY-SA 3.0
2013-10-07T07:52:32.403Z
I explained in the answer what it means that currying becomes uncomputable, namely that the suggested object is not an exponential in the category of represented sets.
Andrej Bauer
CC BY-SA 3.0
2013-11-20T20:34:18.797Z
Thanks for the explanation! Unfortunately I can't upvote again. I can follow most technical details; I am not familiar with topological models, but I'm anyway familiar with "you can't inspect functions in functional programming/λ-calculus".
Your last paragraph also explains why I can't go through s-m-n, because the currying given by s-m-n produces Gödel codes again, not standard functions as you require. I'll be meditating over that paragraph.
Blaisorblade
CC BY-SA 3.0
2010-09-09T21:46:53.320Z
2013-10-07T07:51:57.120Z
2017-04-13T12:32:28.077Z
Andrej Bauer
<p>Here is another way to think about the question, that does not mention types or higher-order functions. As Andrej pointed out, translations or encodings do a lot of computation. Of course, this can't be avoided when comparing models but we can ask if a <em>double translation</em> e.g. from lambda-calculus to Turing machines and back again, is definable or computable within the origin model. For example, that from lambda-calculus to Turing machines (i.e the corresponding Kleene-algebra on the natural numbers) and back is not lambda-definable, since otherwise equality of normal forms would be definable. See</p>
<p>@article{JAY201976, title = &quot;Intensional computation with higher-order functions&quot;, journal = &quot;Theoretical Computer Science&quot;, volume = &quot;768&quot;, pages = &quot;76 - 90&quot;, year = &quot;2019&quot;, issn = &quot;0304-3975&quot;, doi = &quot;doi.org/10.1016/j.tcs.2019.02.016&quot;, url = &quot;sciencedirect.com/science/article/pii/S0304397519301227&quot;, author = &quot;Barry Jay&quot;</p>
<p>In recent work I have shown that my <em>tree calculus</em> supports <em>meaningful translations</em> to and from a novel lambda-calculus called VA-calculus. The double translation to VA-calculus is not definable but the double translation to tree calculus is. The evaluation rules for these combinational calculi have been given in recent tweets by me. The larger story is developed in a finished monograph &quot;Reflective Programs in Tree Calculus&quot; which will be published by Springer-Nature. The proofs have been formally verified in a Coq package called coq-tree-calculus available from GitHub. <a href="https://github.com/barry-jay-personal/tree-calculus" rel="nofollow noreferrer">https://github.com/barry-jay-personal/tree-calculus</a>. The frontmatter of the book and the tweets can be found there as tweets_on_trees.pdf</p>

CC BY-SA 4.0
2020-09-28T07:55:28.977Z
Could you add a reference to your work?
Christian Komusiewicz
CC BY-SA 4.0
2020-09-29T23:36:42.000Z
they have been edited into the answer
Barry Jay
CC BY-SA 4.0
2020-09-23T00:45:29.630Z
2020-09-29T23:36:09.800Z
2020-09-29T23:36:09.800Z
Barry Jay
<p>John Longley has a very extensive survey article discussing the issues involved, <a href="http://homepages.inf.ed.ac.uk/jrl/Research/notions1.pdf">"Notions of Computability at Higher Type"</a>. </p>

<p>The basic idea is that the Church-Turing thesis is only about functions from $\mathbb{N} \to \mathbb{N}$ -- and there's more to computation than that! In particular, when we write programs, we make use of functions of higher type (such as $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$). </p>

<p>In order to fully define a model of higher type computation, we need to specify the <em>calling convention</em> for functions, in order to allow one function to call another function it receives as an argument. In lambda calculus, the standard calling convention is that we represent functions by lambda-terms, and the only thing you can do with a lambda in the lambda calculus is to apply it. In typical encodings with Turing machines, we pass functions as arguments by fixing a particular Godel encoding, and then strings representing the index of the machine you want to pass as an argument. </p>

<p>The difference in encoding means that you can analyze the syntax of the argument with a TM-style encoding, and you cannot with a standard lambda-calculus representation. So if you receive a lambda-term for a function of type $\mathbb{N} \to \mathbb{N}$, you can only test its behavior by passing it particular $n$'s -- you can't analyze the structure of the term in any way. This is just not enough information to figure out the code of the lambda term.</p>

<p>One thing worth noting is that with higher types, if a language is less expressive at one order, it is <em>more</em> expressive one order up, because functions are contravariant. So similarly there are functions you can write in LC that you can't with a TM-style encoding (because they rely on the fact that you can pass functional arguments and know that the receiver can't look inside the function you give it).</p>

<p>EDIT: Here's an example of a function definable in PCF, but not in TM+Goedel encodings. I'll declare the <code>isAlwaysTrue</code> function</p>

<pre><code> isAlwaysTrue : ((unit → bool) → bool) → bool
</code></pre>

<p>which should return true if its argument ignores its argument and always returns true, should return false if its argument returns false on any inputs, and goes into a loop if its argument goes into a loop on any inputs. We can define this function pretty easily, as follows:</p>

<pre><code>isAlwaysTrue p = p (λ(). true) ∧ p (λ(). false) ∧ p (λ(). ⊥)
</code></pre>

<p>where <code>⊥</code> is the looping computation and <code>∧</code> is the and operator on booleans. This works because there are only three inhabitants of <code>unit → bool</code> in PCF, and so we can exhaustively enumerate them. However, in a TM+Goedel-encoding style model, <code>p</code> could test how long its argument takes to return an answer, and return different answers based on that. So the implementation of <code>isAlwaysTrue</code> with TMs would fail to meet the spec. </p>

CC BY-SA 3.0
2013-10-05T21:02:50.403Z
I just realized I had forgot to accept an answer, though I meant to accept yours. Sorry!
Blaisorblade
CC BY-SA 3.0
2016-02-14T07:00:42.040Z
“The difference in encoding means that you can analyze the syntax of the argument with a TM-style encoding, and you cannot with a standard lambda-calculus representation.”: but if you have representations for function composition? Also, what you say seems to suggest HOL is more than a theory of a typed lambda calculus, it's more than that?
Hibou57
CC BY-SA 3.0
2016-02-14T07:13:21.813Z
Also, what about this: https://www.cs.virginia.edu/~evans/cs150/classes/class39/lecture39.pdf . Is this wrong in some way?
Hibou57
CC BY-SA 3.0
2016-09-14T10:33:10.737Z
Dear Neel, do you have an example for a function which can be realized in the lambda calculus model but not in the Turing model?
Ingo Blechschmidt
CC BY-SA 3.0
2016-09-14T13:14:17.433Z
@Ingo: yes, but I'm traveling for the next week or so and can't do much posting. Ping me again then and I'll add one.
Neel Krishnaswami
CC BY-SA 3.0
2016-09-26T19:26:13.670Z
@Neel: I hereby ping you again. :-) I'm still interested in the question and would appreciate one or two keywords or pointers to the literature.
Ingo Blechschmidt
CC BY-SA 3.0
2016-09-30T15:14:12.623Z
@IngoBlechschmidt: Here you go! Third-order is weird. :)
Neel Krishnaswami
CC BY-SA 3.0
2016-10-11T08:29:51.283Z
Thank you very much for taking the time to add the example! However I must admit that I don't understand it fully. Don't the morphisms in realizability theory have to be extensional? In my understanding, `p` may test how long its argument takes to return an answer and use this information for calculations, but the end result has to be independent of this information. (As soon as I've understood the example, I'll collect your's and Andrej's (in a different thread) on an nLab page so everybody can profit from a clear overview.)
Ingo Blechschmidt
CC BY-SA 4.0
2022-11-18T19:41:46.280Z
A bit of an ambiguity in the `isAlwaysTrue` example: what is the desired output if `p` sometimes returns false and sometimes goes into a loop? Which one we can define seems to depend on whether `^` is short-circuiting.
Caleb Stanford
CC BY-SA 2.5
2010-09-09T21:56:02.183Z
this is an excellent survey. thanks for the link !
Suresh Venkat
CC BY-SA 3.0
2010-09-09T10:59:11.547Z
2016-10-11T09:13:57.707Z
2016-10-11T09:13:57.707Z
Neel Krishnaswami
<p>I have three related subquestions, which are highlighted by bullet points below (no, they could not be split, if you are wondering).
Andrej Bauer wrote, <a href="https://cstheory.stackexchange.com/questions/625/relationship-between-turing-machine-and-lambda-calculus/715#715">here</a>, that some functions are realizable through a Turing machine, but not through lambda-calculus. A key step of his reasoning is:</p>

<blockquote>
  <p>However, if we use the lambda
  calculus, then [the program] c is supposed to
  compute a numeral representing a
  Turing machine out of a lambda term
  representing a function f. This cannot
  be done (I can explain why, if you ask
  it as a separate question).</p>
</blockquote>

<ul>
<li>I would like to see an explanation/informal proof.</li>
</ul>

<p>I don't see how to apply Rice's theorem here; it would apply to the problem "are this turing machine T and this lambda-term L equivalent?", because applying this predicate to equivalent terms gives the same result. However, the required function might compute different, but equivalent, TMs for different, but equivalent, lambda-terms.</p>

<ul>
<li>Moreover, if the problem is with introspection of a lambda-term, I think that passing a Gödel encoding of a lambda-term would be also acceptable, wouldn't it?</li>
</ul>

<p>On the one hand, given that his example involves computing, in the lambda calculus, the number of steps needed by a Turing Machine to complete a given task, I'm not very surprised.</p>

<ul>
<li>But since here lambda-calculus can't solve a Turing-machine-related problem, I wonder whether one can define a similar problem for lambda-calculus and prove it unsolvable for Turing machines, or there is actually a difference in power in favor of Turing Machines (which would surprise me).</li>
</ul>

<computability><lambda-calculus><turing-machines>
Realizability theory: difference in power between Lambda calculus and Turing Machines
Blaisorblade
# Realizability theory: difference in power between Lambda calculus and Turing Machines

(Asked by: username_0 on 2010-09-09)

I have three related subquestions, which are highlighted by bullet points below (no, they could not be split, if you are wondering).
username_1 wrote, [here](https://cstheory.stackexchange.com/questions/625/relationship-between-turing-machine-and-lambda-calculus/715#715), that some functions are realizable through a Turing machine, but not through lambda-calculus. A key step of his reasoning is:

> However, if we use the lambda
> calculus, then [the program] c is supposed to
> compute a numeral representing a
> Turing machine out of a lambda term
> representing a function f. This cannot
> be done (I can explain why, if you ask
> it as a separate question).

* I would like to see an explanation/informal proof.

I don't see how to apply Rice's theorem here; it would apply to the problem "are this turing machine T and this lambda-term L equivalent?", because applying this predicate to equivalent terms gives the same result. However, the required function might compute different, but equivalent, TMs for different, but equivalent, lambda-terms.

* Moreover, if the problem is with introspection of a lambda-term, I think that passing a Gödel encoding of a lambda-term would be also acceptable, wouldn't it?

On the one hand, given that his example involves computing, in the lambda calculus, the number of steps needed by a Turing Machine to complete a given task, I'm not very surprised.

* But since here lambda-calculus can't solve a Turing-machine-related problem, I wonder whether one can define a similar problem for lambda-calculus and prove it unsolvable for Turing machines, or there is actually a difference in power in favor of Turing Machines (which would surprise me).

**Tags:** computability, lambda-calculus, turing-machines


---

## 3 answers

### Answer by username_5 on 2010-09-09. Score: 73 | Accepted answer

John Longley has a very extensive survey article discussing the issues involved, "Notions of Computability at Higher Type". 
The basic idea is that the Church-Turing thesis is only about functions from $\mathbb{N} \to \mathbb{N}$ -- and there's more to computation than that! In particular, when we write programs, we make use of functions of higher type (such as $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$). 
In order to fully define a model of higher type computation, we need to specify the calling convention for functions, in order to allow one function to call another function it receives as an argument. In lambda calculus, the standard calling convention is that we represent functions by lambda-terms, and the only thing you can do with a lambda in the lambda calculus is to apply it. In typical encodings with Turing machines, we pass functions as arguments by fixing a particular Godel encoding, and then strings representing the index of the machine you want to pass as an argument. 
The difference in encoding means that you can analyze the syntax of the argument with a TM-style encoding, and you cannot with a standard lambda-calculus representation. So if you receive a lambda-term for a function of type $\mathbb{N} \to \mathbb{N}$, you can only test its behavior by passing it particular $n$'s -- you can't analyze the structure of the term in any way. This is just not enough information to figure out the code of the lambda term.
One thing worth noting is that with higher types, if a language is less expressive at one order, it is more expressive one order up, because functions are contravariant. So similarly there are functions you can write in LC that you can't with a TM-style encoding (because they rely on the fact that you can pass functional arguments and know that the receiver can't look inside the function you give it).
EDIT: Here's an example of a function definable in PCF, but not in TM+Goedel encodings. I'll declare the isAlwaysTrue function
 isAlwaysTrue : ((unit → bool) → bool) → bool

which should return true if its argument ignores its argument and always returns true, should return false if its argument returns false on any inputs, and goes into a loop if its argument goes into a loop on any inputs. We can define this function pretty easily, as follows:
isAlwaysTrue p = p (λ(). true) ∧ p (λ(). false) ∧ p (λ(). ⊥)

where ⊥ is the looping computation and ∧ is the and operator on booleans. This works because there are only three inhabitants of unit → bool in PCF, and so we can exhaustively enumerate them. However, in a TM+Goedel-encoding style model, p could test how long its argument takes to return an answer, and return different answers based on that. So the implementation of isAlwaysTrue with TMs would fail to meet the spec.

> **Comments:**
> **username_9**: this is an excellent survey. thanks for the link !  
> **username_0**: I just realized I had forgot to accept an answer, though I meant to accept yours. Sorry!  
> **username_6**: “The difference in encoding means that you can analyze the syntax of the argument with a TM-style encoding, and you cannot with a standard lambda-calculus representation.”: but if you have representations for function composition? Also, what you say seems to suggest HOL is more than a theory of a typed lambda calculus, it's more than that?  
> **username_6**: Also, what about this: https://www.cs.virginia.edu/~evans/cs150/classes/class39/lecture39.pdf . Is this wrong in some way?  
> **username_7**: Dear Neel, do you have an example for a function which can be realized in the lambda calculus model but not in the Turing model?  
> **username_5**: @Ingo: yes, but I'm traveling for the next week or so and can't do much posting. Ping me again then and I'll add one.  
> **username_7**: @Neel: I hereby ping you again. :-) I'm still interested in the question and would appreciate one or two keywords or pointers to the literature.  
> **username_5**: @IngoBlechschmidt: Here you go! Third-order is weird. :)  
> **username_7**: Thank you very much for taking the time to add the example! However I must admit that I don't understand it fully. Don't the morphisms in realizability theory have to be extensional? In my understanding, `p` may test how long its argument takes to return an answer and use this information for calculations, but the end result has to be independent of this information. (As soon as I've understood the example, I'll collect your's and Andrej's (in a different thread) on an nLab page so everybody can profit from a clear overview.)  
> **username_8**: A bit of an ambiguity in the `isAlwaysTrue` example: what is the desired output if `p` sometimes returns false and sometimes goes into a loop? Which one we can define seems to depend on whether `^` is short-circuiting.  

---

### Answer by username_1 on 2010-09-09. Score: 35

What Neel said, and also the following.

I would like to emphasize ([again](http://math.andrej.com/2008/02/06/representations-of-uncomputable-and-uncountable-sets/), [again](https://cstheory.stackexchange.com/questions/1037/what-does-it-mean-that-there-are-differing-views-on-how-computations-are-represen/) and [again](http://drops.dagstuhl.de/opus/volltexte/2009/2257/)) that representation of input and output matters. If we are allowed to change representations, we can achieve just about anything (for example, make any given function computable). So, passing from a representation of functions $\mathbb{N} \to \mathbb{N}$ by $\lambda$-terms to a representation by Gödel numbers is *not* acceptable if our model of computation is $\lambda$-calculus (because then the currying operation becomes uncomputable by $\lambda$-calculus).

A statement which is realizable in the $\lambda$-term model but not in the Turing machine model is "not every function $\mathbb{N} \to \mathbb{N}$ has a Gödel code", which is kind of silly. I will try to come up with a better one and edit this answer.

---

**Edit on 2013-10-07:** Here is what I meant by "currying becomes uncomputable". Suppose we use the untyped $\lambda$-calculus as our computational model, but then we decide that we should represent maps $\mathbb{N} \to \mathbb{N}$ with Gödel codes (of Turing machines, encoded as Church numerals). Sounds harmless, right? After all we believe the mantra "Turing machines and $\lambda$-calculus are equivalent".

Well, for this new representation to actually be a valid representation of $\mathbb{N} \to \mathbb{N}$, we need also to realize application and currying (because to "represent functions" means the same thing as "to represent an exponential object"). Specifically, we need a $\lambda$-term $\mathtt{app}$ such that, whenever the Church numeral $\overline{n}$ represents $f : \mathbb{N} \to \mathbb{N}$ then $f(k)$ is represented by $\mathtt{app} \; \overline{n} \; \overline{k}$. (Here I write $\overline{n}$ for the Church numeral representing the number $n$.) Such an $\mathtt{app}$ is readily available because it amounts to an interpreter for Turing machines, implemented in the $\lambda$-calculus.

But how about currying? For that we need the following. Suppose $X$ is a represented set. Given any map $f : X \times \mathbb{N} \to \mathbb{N}$ computed by a $\lambda$-term $t$, we need to show that the transposition $\tilde{f} : X \to (\mathbb{N} \to \mathbb{N})$ is also computed by some $\lambda$-term $s$. But consider the example where $X$ is the set o fmaps $\mathbb{N} \to \mathbb{N}$ represented by $\lambda$-terms, and $f$ is application. Then $\tilde{f}$ would be a map which acts as identity on $\mathbb{N} \to \mathbb{N}$, but its realizer is a $\lambda$-term that converts $\lambda$-terms representing maps $\mathbb{N} \to \mathbb{N}$ to corresponding Gödel codes. Such a $\lambda$-term does not exist (for example because it would be discontinuous in a topological semantic model).

You may attempt to object that I should not have used the specific represented set $X$ of maps $\mathbb{N} \to \mathbb{N}$ represented by $\lambda$-terms, because we "agreed" that those should be represented by Gödel codes. But you would be wrong. First of all, I could have used a different $X$ with a more complicated proof which would elude you but still accomplish the same result. Second of all, $X$ is there in the category and the definition of exponential requires that currying work with respect to *all* objects. You have to respect the category. You cannot just randomly butcher it and take some objects out (well, you can but then you are a butcher).

> **Comments:**
> **username_2**: still waiting for that better example...  
> **username_1**: Well, I can think of many statements which are realizable with Turing machines but not with $\lambda$-terms. I suppose you want the opposite. Hmmm.  
> **username_0**: I don't get how currying can become incomputable. You should be able to reuse the s-m-n theorem, since its proof constructs a function on first-order data (naturals). By the Church-Turing thesis, this behavior on naturals can be implemented as a lambda term (which uses native functions internally, but I don't see how that's forbidden). One can similarly prove the u-t-m theorem, so according to [your post](http://math.andrej.com/2008/02/06/representations-of-uncomputable-and-uncountable-sets/) we should be done. What am I missing?  
> **username_1**: I explained in the answer what it means that currying becomes uncomputable, namely that the suggested object is not an exponential in the category of represented sets.  
> **username_0**: Thanks for the explanation! Unfortunately I can't upvote again. I can follow most technical details; I am not familiar with topological models, but I'm anyway familiar with "you can't inspect functions in functional programming/λ-calculus". Your last paragraph also explains why I can't go through s-m-n, because the currying given by s-m-n produces Gödel codes again, not standard functions as you require. I'll be meditating over that paragraph.  

---

### Answer by username_3 on 2020-09-23. Score: 2

Here is another way to think about the question, that does not mention types or higher-order functions. As Andrej pointed out, translations or encodings do a lot of computation. Of course, this can't be avoided when comparing models but we can ask if a *double translation* e.g. from lambda-calculus to Turing machines and back again, is definable or computable within the origin model. For example, that from lambda-calculus to Turing machines (i.e the corresponding Kleene-algebra on the natural numbers) and back is not lambda-definable, since otherwise equality of normal forms would be definable. See

@article{JAY201976, title = "Intensional computation with higher-order functions", journal = "Theoretical Computer Science", volume = "768", pages = "76 - 90", year = "2019", issn = "0304-3975", doi = "doi.org/10.1016/j.tcs.2019.02.016", url = "sciencedirect.com/science/article/pii/S0304397519301227", author = "username_3"

In recent work I have shown that my *tree calculus* supports *meaningful translations* to and from a novel lambda-calculus called VA-calculus. The double translation to VA-calculus is not definable but the double translation to tree calculus is. The evaluation rules for these combinational calculi have been given in recent tweets by me. The larger story is developed in a finished monograph "Reflective Programs in Tree Calculus" which will be published by Springer-Nature. The proofs have been formally verified in a Coq package called coq-tree-calculus available from GitHub. <https://github.com/barry-jay-personal/tree-calculus>. The frontmatter of the book and the tweets can be found there as tweets\_on\_trees.pdf

> **Comments:**
> **username_4**: Could you add a reference to your work?  
> **username_3**: they have been edited into the answer  

---

