<p>Pure untyped $\lambda$-calculus is Turing complete, i.e., a partial number-theoretic map is computable if, and only if, it is definable in the untyped $\lambda$-calculus. The computational power of typed $\lambda$-calculus is much smaller. For example, if we add a type of natural numbers <code>nat</code> to the typed $\lambda$-calculus, together with $0$, successor, and primitive recursion, we get what is commonly known as Gödel's $T$. It computes the primitive recursive functions only (and they are all total).</p>

<p>The untyped $\lambda$-calculus does not have a reasonable interpretation under the Curry-Howard correspondence, while the typed $\lambda$-calculus corresponds precisely to intuitionistic propositional calculus.</p>

<p>Models of typed $\lambda$-calculus are precisely the cartesian-closed categories. Models of the untyped $\lambda$-calculus are less well-behaved. While it is possible to talk about them, they are certainly not studied as widely as cartesian-closed categories.</p>

<p>We can also entertain ourselves by asking "Which is more general?" At face value the untyped $\lambda$-calculus seems more general because it is easy to embed the typed one into the untyped one (by forgetting types). But we can embed the untyped $\lambda$-calculus into the typed $\lambda$-calculus by positing a primitive type <code>U</code> together with isomorphisms <code>lambda : U -&gt; (U -&gt; U)</code> and <code>gamma : (U -&gt; U) -&gt; U</code>. On the semantic side this corresponds to Dana Scott's observation that every model of the untyped $\lambda$-calculus arises as a reflexive object in a cartesian closed category, i.e., given a model $\mathbb{U}$ of the untyped $\lambda$-calculus we can find a category $\mathcal{C}$ (if my memory serves me right, it is the idempotent splitting of $\mathbb{U}$), such that the $\mathbb{U}$ can be seen as an object of the presheaf category $[\mathcal{C}^{\mathrm{op}}, \mathsf{Set}]$ (via Yoneda embedding) satisfying the equation $\mathbb{U} \cong \mathbb{U}^{\mathbb{U}}$.</p>

<p>References:</p>

<ul>
<li><p>Dana S. Scott: "<a href="http://dx.doi.org/10.1016/S0049-237X%2808%2971262-X">Lambda Calculus: Some Models, Some Philosophy</a>", Studies in Logic and the Foundations of Mathematics, Volume 101, 1980, Pages 223-265, The Kleene Symposium</p></li>
<li><p>Hendrik Pieter Barendregt: "<a href="http://books.google.com/books?id=ZdydJZVue50C&amp;lpg=PP1&amp;dq=barendregt&amp;pg=PP1#v=onepage&amp;q&amp;f=false">The lambda calculus: its syntax and semantics</a>", Elsevier, 1984.</p></li>
</ul>

CC BY-SA 4.0
2023-07-04T18:17:50.850Z
"But we can embed the untyped λ-calculus into the typed λ-calculus by positing a primitive type U ..." I see this intuitively, but I can't reconcile it with the fact that only terminating computations can be expressed in the STLC whereas any Turing computation can be done in the ULC. Logically too, the ULC can express more than simple intuitionistic propositions
Motorhead
CC BY-SA 4.0
2023-07-05T10:36:11.907Z
If you add stuff to a theory meta-theorems about the theory may become false. Case in point: STLC is strongly normalizing, but STLC with an additional type `U` isomorphic to `U → U` is not. Why would this be surprising?
Andrej Bauer
CC BY-SA 4.0
2023-07-06T00:36:30.987Z
When moving from the ULC to the STLC it seems many of the online articles I've looked at brush over the fact that its not just about giving the terms types. The ULC simply had computation steps that were carried out by \beta and \alpha rules. The STLC adds typing judgments and more importantly, inference rules. These have no analogue in the ULC
Motorhead
CC BY-SA 4.0
2023-07-06T10:11:05.957Z
"Moving from ULC to STLC" is not a precise notion. We have at least two ways of doing it, both present in this discussion. The first is to take ULC, adjoint to it types and typing information, and restrict terms to the well-typed ones (thereby invalidating some terms). The second one is the embedding of ULC into STLC with a universal type $U$, as suggested above, in which *all* terms of ULC are translated to typeable terms (and all have type $U$). If we want to make progress in this discusssion, you'll have to be more precise about what you mean.
Andrej Bauer
CC BY-SA 4.0
2023-07-06T17:01:29.430Z
Sure, I can try and explain my concern a little better. If you take your 1st option, STLC = ULC + types/judgments + type inference rules. The inference rules in particular are a significant addition to the ULC which had nothing but term rewriting. From a pedagogical point of view, it seems to me at least that difference is really worth pointing out.
Motorhead
CC BY-SA 4.0
2023-07-06T18:47:38.410Z
Or you can say that ULC is just like STLC, except that there is only one type $U$ and the typing rules are silly.
Andrej Bauer
CC BY-SA 4.0
2023-08-04T17:06:15.347Z
"If you add stuff to a theory meta-theorems about the theory may become false". I'm sure you're technically right, but it just seems bizarre to then claim that its still STLC. I mean when I call something X I would expect that the properties of X pertain to it, ie you can add properties but not remove them. To me its like saying I can characterize rectangles as squares by eliminating the property that all sides have the same length.
Motorhead
CC BY-SA 4.0
2023-08-04T19:59:39.500Z
STLC can mean several things and you need to be careful. It might mean "pure STLC", or STLC + constants + equations, etc. And you can't seriously argue by using vague analogies, such as "squares and rectangles".
Andrej Bauer
CC BY-SA 2.5
2011-04-03T07:11:17.273Z
2011-04-03T07:19:31.527Z
2011-04-03T07:19:31.527Z
Andrej Bauer
<p>A fairly comprehensive discussion of this stuff can be found in this book: <a href="http://www.elsevier.com/wps/find/bookdescription.cws_home/706927/description#description">Lectures on the Curry-Howard Isomorphism</a>.  This is based on the freely available older version: <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385">Lectures on the Curry-Howard Isomorphism</a>.</p>

CC BY-SA 2.5
2011-04-03T17:12:24.157Z
2011-04-03T17:12:24.157Z
Marc Hamann
<p>Your table is a bit confused; here's a better one.</p>

<ul>
<li>Untyped lambda calculus -- no logical interpretation, as Andrej notes</li>
<li>Simply typed lambda calculus -- intuitionistic propositional logic</li>
<li>Polymorphic lambda calculus -- pure second-order logic (ie, without first-order quantifiers)</li>
<li>Dependent types -- generalization of first-order logic</li>
<li>Calculus of constructions -- generalization of higher-order logic</li>
</ul>

<p>Type dependency is more general than first-order quantification, since it turns proofs into objects you can quantify over. Lambda calculi corresponding to ordinary intuitionistic FOL exist, but are not widely used enough to have a special name -- people tend to go straight to dependent types.</p>

<p>You can also relate the syntactic form of a calculus to logical systems, as well.</p>

<ul>
<li>Combinator calculi (eg, SKI combinators) -- Hilbert-style systems</li>
<li>A-normal form -- sequent calculus </li>
<li>Ordinary typed lambda calculus -- natural deduction</li>
</ul>

CC BY-SA 2.5
2011-04-04T20:10:52.957Z
fantastic! thanks.  helps me realize the motivation/distinction for these different calculi, and will certainly help me keep a base understanding when i read more about it
jon_darkstar
CC BY-SA 2.5
2011-04-07T19:46:50.883Z
I would also include typed lambda calculi with no logical interpretation, such as PCF.  

Also, there are lots of cool lambda-calculi that correspond to other logic, such as the linear lambda calculus.
Sam Tobin-Hochstadt
CC BY-SA 3.0
2011-04-13T14:55:18.730Z
@Sam: Good point. "No logical interpretation" is really too strong, since it really means "unrestricted self-reference allowed", which *combined* with variable reuse leads to inconsistency. But some set theories based on linear logic support naive comprehension schemes without any inconsistency.
Neel Krishnaswami
CC BY-SA 3.0
2011-04-21T20:41:05.060Z
certainly, some ways you can add some things to lambda calculus without being inconsistent.  But there are many interesting, typed, lambda calculi with no logical interpretation in exactly the sense of the untyped lambda calculus.
Sam Tobin-Hochstadt
CC BY-SA 2.5
2011-04-03T12:23:22.390Z
2011-04-03T12:23:22.390Z
Neel Krishnaswami
<p>Can anyone explain briefly (if thats possible!) or refer me to a reference, summarizing the differences between untyped lambda calculus and the more common typed lambda calculi?</p>
<p>I'm particularly looking for statements of their expressive power, equivalences to logic/arithmetic systems or computation methods, and analogies to programming languages if applicable.</p>
<p>While I certainly intend to read, something like a reference table outlining the calculi and their equivalences/differences/place in the hierarchy would be a HUGE reference for helping me sort them out.</p>
<p>Not saying the below is correct, just trying to sketch together some of the impressions i have to see if they at least serve as a starting point (or something to correct!)</p>
<blockquote>
<p>Untyped lambda calculus - eq. to first order logic - cannot do X</p>
<p>Simply typed lambda calculus - eq to ... logic, related to Lisp?</p>
<p>'Polymorphic' lambda calc -
etc.</p>
<p>Calculus of Constructions - intutionist logic?</p>
<p>Combinatory Logic - comparable to ??? typed lambda calculus, related to APL/J kind of languages</p>
</blockquote>
<p>If this ties into the lambda cube and its three axes all the better.</p>
<p>While I'm familiar with the basics of lambda calculus and programming with functional languages, I have never wrapped my head around, or made any significant connections to, the type systems involved and different flavors of lambda (and maybe pi?) calculi.</p>
<p>When I attempt to research this i cant help but find myself sidetracked, opening up many browser tabs and branching in so many directions I never get into any of them with any depth!</p>
<p>I'm not sure if what I'm asking for is reasonable, but hopefully at the very least I've painted enough of a picture to suggest some reading that can explain what im looking for?</p>

CC BY-SA 2.5
2011-04-02T23:14:55.983Z
a visualization of lambda cube, if perhaps referring to it can help with explanation http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm
jon_darkstar
CC BY-SA 2.5
2011-04-03T18:00:21.780Z
A personal story: when I was first learning typed and untyped lambda calculus, I was always confused by why I should care about the typed non-Turing complete calculi. This often made me lose interest. On the other hand, I was never bothered by this when thinking about complexity and efficient computation. Eventually someone connected the two strands for me in [this answer](http://cstheory.stackexchange.com/questions/5120/programming-languages-for-efficient-computation/5121#5121) and now I can better understand why so much time was spent teaching me typed lambda calculus.
Artem Kaznatcheev
CC BY-SA 2.5
2011-04-05T06:39:00.333Z
i see a `lo.logic` tag has been added.  probably a dumb question, but what exactly does that stand for?
jon_darkstar
CC BY-SA 3.0
2015-07-22T20:36:56.547Z
"When I attempt to research this i cant help but find myself sidetracked, opening up many browser tabs and branching in so many directions I never get into any of them with any depth!" <-- This is me, all the time! Thanks for asking what I've been thinking ...
agam
<lo.logic><type-theory><lambda-calculus>
Classification of Typed/Untyped Lambda Calculi
jon_darkstar
# Classification of Typed/Untyped Lambda Calculi

(Asked by: username_0 on 2011-04-02)

Can anyone explain briefly (if thats possible!) or refer me to a reference, summarizing the differences between untyped lambda calculus and the more common typed lambda calculi?

I'm particularly looking for statements of their expressive power, equivalences to logic/arithmetic systems or computation methods, and analogies to programming languages if applicable.

While I certainly intend to read, something like a reference table outlining the calculi and their equivalences/differences/place in the hierarchy would be a HUGE reference for helping me sort them out.

Not saying the below is correct, just trying to sketch together some of the impressions i have to see if they at least serve as a starting point (or something to correct!)

> Untyped lambda calculus - eq. to first order logic - cannot do X
>
> Simply typed lambda calculus - eq to ... logic, related to Lisp?
>
> 'Polymorphic' lambda calc -
> etc.
>
> Calculus of Constructions - intutionist logic?
>
> Combinatory Logic - comparable to ??? typed lambda calculus, related to APL/J kind of languages

If this ties into the lambda cube and its three axes all the better.

While I'm familiar with the basics of lambda calculus and programming with functional languages, I have never wrapped my head around, or made any significant connections to, the type systems involved and different flavors of lambda (and maybe pi?) calculi.

When I attempt to research this i cant help but find myself sidetracked, opening up many browser tabs and branching in so many directions I never get into any of them with any depth!

I'm not sure if what I'm asking for is reasonable, but hopefully at the very least I've painted enough of a picture to suggest some reading that can explain what im looking for?

**Tags:** lo.logic, type-theory, lambda-calculus

> **Comments:**
> **username_0**: a visualization of lambda cube, if perhaps referring to it can help with explanation http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm  
> **username_1**: A personal story: when I was first learning typed and untyped lambda calculus, I was always confused by why I should care about the typed non-Turing complete calculi. This often made me lose interest. On the other hand, I was never bothered by this when thinking about complexity and efficient computation. Eventually someone connected the two strands for me in [this answer](http://cstheory.stackexchange.com/questions/5120/programming-languages-for-efficient-computation/5121#5121) and now I can better understand why so much time was spent teaching me typed lambda calculus.  
> **username_0**: i see a `lo.logic` tag has been added.  probably a dumb question, but what exactly does that stand for?  
> **username_2**: "When I attempt to research this i cant help but find myself sidetracked, opening up many browser tabs and branching in so many directions I never get into any of them with any depth!" <-- This is me, all the time! Thanks for asking what I've been thinking ...  

---

## 3 answers

### Answer by username_6 on 2011-04-03. Score: 27 | Accepted answer

Your table is a bit confused; here's a better one.

* Untyped lambda calculus -- no logical interpretation, as Andrej notes
* Simply typed lambda calculus -- intuitionistic propositional logic
* Polymorphic lambda calculus -- pure second-order logic (ie, without first-order quantifiers)
* Dependent types -- generalization of first-order logic
* Calculus of constructions -- generalization of higher-order logic

Type dependency is more general than first-order quantification, since it turns proofs into objects you can quantify over. Lambda calculi corresponding to ordinary intuitionistic FOL exist, but are not widely used enough to have a special name -- people tend to go straight to dependent types.

You can also relate the syntactic form of a calculus to logical systems, as well.

* Combinator calculi (eg, SKI combinators) -- Hilbert-style systems
* A-normal form -- sequent calculus
* Ordinary typed lambda calculus -- natural deduction

> **Comments:**
> **username_0**: fantastic! thanks.  helps me realize the motivation/distinction for these different calculi, and will certainly help me keep a base understanding when i read more about it  
> **username_7**: I would also include typed lambda calculi with no logical interpretation, such as PCF.    Also, there are lots of cool lambda-calculi that correspond to other logic, such as the linear lambda calculus.  
> **username_6**: @Sam: Good point. "No logical interpretation" is really too strong, since it really means "unrestricted self-reference allowed", which *combined* with variable reuse leads to inconsistency. But some set theories based on linear logic support naive comprehension schemes without any inconsistency.  
> **username_7**: certainly, some ways you can add some things to lambda calculus without being inconsistent.  But there are many interesting, typed, lambda calculi with no logical interpretation in exactly the sense of the untyped lambda calculus.  

---

### Answer by username_3 on 2011-04-03. Score: 19

Pure untyped $\lambda$-calculus is Turing complete, i.e., a partial number-theoretic map is computable if, and only if, it is definable in the untyped $\lambda$-calculus. The computational power of typed $\lambda$-calculus is much smaller. For example, if we add a type of natural numbers `nat` to the typed $\lambda$-calculus, together with $0$, successor, and primitive recursion, we get what is commonly known as Gödel's $T$. It computes the primitive recursive functions only (and they are all total).

The untyped $\lambda$-calculus does not have a reasonable interpretation under the Curry-Howard correspondence, while the typed $\lambda$-calculus corresponds precisely to intuitionistic propositional calculus.

Models of typed $\lambda$-calculus are precisely the cartesian-closed categories. Models of the untyped $\lambda$-calculus are less well-behaved. While it is possible to talk about them, they are certainly not studied as widely as cartesian-closed categories.

We can also entertain ourselves by asking "Which is more general?" At face value the untyped $\lambda$-calculus seems more general because it is easy to embed the typed one into the untyped one (by forgetting types). But we can embed the untyped $\lambda$-calculus into the typed $\lambda$-calculus by positing a primitive type `U` together with isomorphisms `lambda : U -> (U -> U)` and `gamma : (U -> U) -> U`. On the semantic side this corresponds to Dana Scott's observation that every model of the untyped $\lambda$-calculus arises as a reflexive object in a cartesian closed category, i.e., given a model $\mathbb{U}$ of the untyped $\lambda$-calculus we can find a category $\mathcal{C}$ (if my memory serves me right, it is the idempotent splitting of $\mathbb{U}$), such that the $\mathbb{U}$ can be seen as an object of the presheaf category $[\mathcal{C}^{\mathrm{op}}, \mathsf{Set}]$ (via Yoneda embedding) satisfying the equation $\mathbb{U} \cong \mathbb{U}^{\mathbb{U}}$.

References:

* Dana S. Scott: "[Lambda Calculus: Some Models, Some Philosophy](http://dx.doi.org/10.1016/S0049-237X%2808%2971262-X)", Studies in Logic and the Foundations of Mathematics, Volume 101, 1980, Pages 223-265, The Kleene Symposium
* Hendrik Pieter Barendregt: "[The lambda calculus: its syntax and semantics](http://books.google.com/books?id=ZdydJZVue50C&lpg=PP1&dq=barendregt&pg=PP1#v=onepage&q&f=false)", Elsevier, 1984.

> **Comments:**
> **username_4**: "But we can embed the untyped λ-calculus into the typed λ-calculus by positing a primitive type U ..." I see this intuitively, but I can't reconcile it with the fact that only terminating computations can be expressed in the STLC whereas any Turing computation can be done in the ULC. Logically too, the ULC can express more than simple intuitionistic propositions  
> **username_3**: If you add stuff to a theory meta-theorems about the theory may become false. Case in point: STLC is strongly normalizing, but STLC with an additional type `U` isomorphic to `U → U` is not. Why would this be surprising?  
> **username_4**: When moving from the ULC to the STLC it seems many of the online articles I've looked at brush over the fact that its not just about giving the terms types. The ULC simply had computation steps that were carried out by \beta and \alpha rules. The STLC adds typing judgments and more importantly, inference rules. These have no analogue in the ULC  
> **username_3**: "Moving from ULC to STLC" is not a precise notion. We have at least two ways of doing it, both present in this discussion. The first is to take ULC, adjoint to it types and typing information, and restrict terms to the well-typed ones (thereby invalidating some terms). The second one is the embedding of ULC into STLC with a universal type $U$, as suggested above, in which *all* terms of ULC are translated to typeable terms (and all have type $U$). If we want to make progress in this discusssion, you'll have to be more precise about what you mean.  
> **username_4**: Sure, I can try and explain my concern a little better. If you take your 1st option, STLC = ULC + types/judgments + type inference rules. The inference rules in particular are a significant addition to the ULC which had nothing but term rewriting. From a pedagogical point of view, it seems to me at least that difference is really worth pointing out.  
> **username_3**: Or you can say that ULC is just like STLC, except that there is only one type $U$ and the typing rules are silly.  
> **username_4**: "If you add stuff to a theory meta-theorems about the theory may become false". I'm sure you're technically right, but it just seems bizarre to then claim that its still STLC. I mean when I call something X I would expect that the properties of X pertain to it, ie you can add properties but not remove them. To me its like saying I can characterize rectangles as squares by eliminating the property that all sides have the same length.  
> **username_3**: STLC can mean several things and you need to be careful. It might mean "pure STLC", or STLC + constants + equations, etc. And you can't seriously argue by using vague analogies, such as "squares and rectangles".  

---

### Answer by username_5 on 2011-04-03. Score: 7

A fairly comprehensive discussion of this stuff can be found in this book: [Lectures on the Curry-Howard Isomorphism](http://www.elsevier.com/wps/find/bookdescription.cws_home/706927/description#description). This is based on the freely available older version: [Lectures on the Curry-Howard Isomorphism](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385).


---

