19
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ a visualization of lambda cube, if perhaps referring to it can help with explanation rbjones.com/rbjpub/logic/cl/tlc001.htm $\endgroup$
    – jon_darkstar
    Apr 2, 2011 at 23:14
  • 3
    $\begingroup$ 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. $\endgroup$
    – Artem Kaznatcheev ♦
    Apr 3, 2011 at 18:00
  • $\begingroup$ i see a lo.logic tag has been added. probably a dumb question, but what exactly does that stand for? $\endgroup$
    – jon_darkstar
    Apr 5, 2011 at 6:39
  • $\begingroup$ "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 ... $\endgroup$
    – agam
    Jul 22, 2015 at 20:36

3 Answers 3

Reset to default
27
$\begingroup$

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
Improve this answer
$\endgroup$
4
  • $\begingroup$ 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 $\endgroup$
    – jon_darkstar
    Apr 4, 2011 at 20:10
  • $\begingroup$ 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. $\endgroup$
    – Sam Tobin-Hochstadt
    Apr 7, 2011 at 19:46
  • $\begingroup$ @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. $\endgroup$
    – Neel Krishnaswami
    Apr 13, 2011 at 14:55
  • $\begingroup$ 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. $\endgroup$
    – Sam Tobin-Hochstadt
    Apr 21, 2011 at 20:41
20
$\begingroup$

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:

Improve this answer
$\endgroup$
8
  • $\begingroup$ "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 $\endgroup$
    – Motorhead
    Jul 4 at 18:17
  • $\begingroup$ 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? $\endgroup$
    – Andrej Bauer
    Jul 5 at 10:36
  • $\begingroup$ 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 $\endgroup$
    – Motorhead
    Jul 6 at 0:36
  • $\begingroup$ "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. $\endgroup$
    – Andrej Bauer
    Jul 6 at 10:11
  • $\begingroup$ 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. $\endgroup$
    – Motorhead
    Jul 6 at 17:01
7
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.