# Classification of Typed/Untyped Lambda Calculi

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 heirarchy 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?

-
a visualization of lambda cube, if perhaps referring to it can help with explanation rbjones.com/rbjpub/logic/cl/tlc001.htm – jon_darkstar Apr 2 '11 at 23:14
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 and now I can better understand why so much time was spent teaching me typed lambda calculus. – Artem Kaznatcheev Apr 3 '11 at 18:00
i see a lo.logic tag has been added. probably a dumb question, but what exactly does that stand for? – jon_darkstar Apr 5 '11 at 6:39
"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 Jul 22 '15 at 20:36

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
-
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 Apr 4 '11 at 20:10
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 Apr 7 '11 at 19:46
@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 Apr 13 '11 at 14:55
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 Apr 21 '11 at 20:41

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:

-
definitely helpful, thank you! – jon_darkstar Apr 4 '11 at 20:11

A fairly comprehensive discussion of this stuff can be found in this book: Lectures on the Curry-Howard Isomorphism. This is based on the freely available older version: Lectures on the Curry-Howard Isomorphism.

-