<p>A denotational model of the lambda calculus is a framework where lambda terms are represented <em>and</em> the computational process of beta-reduction is &quot;collapsed&quot;, or &quot;abstracted away&quot;, in the sense that the interpretation in the model is stable by beta reduction (and expansion).</p>
<p>Turing machines can represent lambda terms and simulate beta reduction. Luckily, it is not important to enter into the details of the correspondence in order to answer your question. The point is simply that it is a <em>simulation</em>, requiring computation. Therefore, beta reduction is not collapsed, and Turing machines do not provide a denotational model of the lambda calculus.</p>

CC BY-SA 4.0
2024-07-22T08:28:31.267Z
And you can positively prove that there is no simulation by Turing machines which happens to collapse $\beta$-reduction?
Andrej Bauer
CC BY-SA 4.0
2024-07-22T13:02:39.910Z
A simulation that collapses beta reduction sounds like an oxymoron. I think that it is impossible to properly discuss the issue without looking more closely at how Turing machines simulate the lambda calculus, but I am not sure it is worth it, since the question was not a technical one. A relevant paper is Della Penna, Intrigila & Manzonetto's 
"Addressing Machines as models of lambda-calculus" (2022), where the simulation provided by a notion of machine (but not Turing's) is turned into a denotational model via a certain quotient.
Beniamino Accattoli
CC BY-SA 4.0
2024-07-21T23:19:45.987Z
2024-07-21T23:19:45.987Z
Beniamino Accattoli
<p>I am wondering whether it is correct to say that Turing machines are models of, say, the lambda calculus, in the model theoretical sense. Lambda calculus and Turing machines are equivalent formulations of effective computation, but when we talk about models of lambda calculus we turn to models like Scott domains. Could we not simply think of Turing machines as a semantic model of the lambda calculus?</p>
<p>If not, what am I getting wrong? Is it because they are equivalent, and not that Turing machines preserve the relevant formal structure of the lambda calculus?</p>

CC BY-SA 4.0
2024-07-22T08:29:35.640Z
What does "model-theoretic sense" mean? Are you talking about first-order logic and models of first-order theories (which would be the wrong thing to talk about), or the very specific notion of a $\lambda$-model?
Andrej Bauer
<lambda-calculus><turing-machines><model-theory>
Are Turing Machines Models?
user73165
# Are Turing Machines Models?

(Asked by: username_0 on 2024-07-21)

I am wondering whether it is correct to say that Turing machines are models of, say, the lambda calculus, in the model theoretical sense. Lambda calculus and Turing machines are equivalent formulations of effective computation, but when we talk about models of lambda calculus we turn to models like Scott domains. Could we not simply think of Turing machines as a semantic model of the lambda calculus?

If not, what am I getting wrong? Is it because they are equivalent, and not that Turing machines preserve the relevant formal structure of the lambda calculus?

**Tags:** lambda-calculus, turing-machines, model-theory
> **Comments:**
> **username_1**: What does "model-theoretic sense" mean? Are you talking about first-order logic and models of first-order theories (which would be the wrong thing to talk about), or the very specific notion of a $\lambda$-model?  

---

## 1 answers

### Answer by username_2 on 2024-07-21. Score: 3 | Accepted answer

A denotational model of the lambda calculus is a framework where lambda terms are represented *and* the computational process of beta-reduction is "collapsed", or "abstracted away", in the sense that the interpretation in the model is stable by beta reduction (and expansion).

Turing machines can represent lambda terms and simulate beta reduction. Luckily, it is not important to enter into the details of the correspondence in order to answer your question. The point is simply that it is a *simulation*, requiring computation. Therefore, beta reduction is not collapsed, and Turing machines do not provide a denotational model of the lambda calculus.

> **Comments:**
> **username_1**: And you can positively prove that there is no simulation by Turing machines which happens to collapse $\beta$-reduction?  
> **username_2**: A simulation that collapses beta reduction sounds like an oxymoron. I think that it is impossible to properly discuss the issue without looking more closely at how Turing machines simulate the lambda calculus, but I am not sure it is worth it, since the question was not a technical one. A relevant paper is Della Penna, Intrigila & Manzonetto's  "Addressing Machines as models of lambda-calculus" (2022), where the simulation provided by a notion of machine (but not Turing's) is turned into a denotational model via a certain quotient.  

---

