14
$\begingroup$

A simple question here, which likely demands a somewhat complex answer... Or rather, a set of related questions.

  • What are the advantages of typed lambda calculus over untyped lambda calculus in terms of proof theory?
  • Specifically, Church's original Lambda Calculus was untyped and allows arbitrarily high-order functions. What are the limitations with respect to constructing a proof calculus from it?
  • Are not untyped and typed lambda calculi inherently higher-order formal systems?
  • What are the reasons for using complex (e.g. polymorphic/dependent) type theories over the simple type theory in lambda calculus? Are they more 'powerful' in some sense; if so, how exactly?
  • Do semantics (interpretation) have anything to say here, with respect to typed and untyped theories, especially in terms of soundness and completeness?
  • The well-known proof verifier Coq, which (I believe) uses a language of higher-order complex-typed lambda calculus to represent proofs in constructive (intuistionistic) mathematics. I have read that the theory behind it (the Calculus of Constructions) is essentially an extension of the Curry-Howard isomorphism to higher-order logic. Are there any elaborations/clarifications I should be aware of here?
$\endgroup$

1 Answer 1

Reset to default
9
$\begingroup$
  1. What are the advantages of typed lambda calculus over untyped lambda calculus in terms of proof theory? and also
  2. Specifically, Church's original Lambda Calculus was untyped and allows arbitrarily high-order functions. What are the limitations with respect to constructing a proof calculus from it?
    • Simply, typed lambda calculus has a proof theory, and untyped lambda calculus doesn't because it lacks a normal-form theorem.
  3. Are not untyped and typed lambda calculi inherently higher-order formal systems?
    • This is tricky, because there are two ways of looking at higher-orderness. They are higher-order when you look at the terms, since the definition of higher order is abstraction over higher-order entities like functions, and lambda abstraction is abstraction. But note, under the formulae-as-types correspondence, the proposaitions in logic are associated with the types of the lambda terms, and in, say, the simply-typed lambda calculus, there is no abstraction over anything. This point confused me when I first studied Church's simple theory of types, because it is a higher-order calculus based on simply-typed lambda calculus, where the propositions are formed using the lambda terms, rather than, as with the formulae-as-types corespondence, being the types.
  4. What are the reasons for using complex (e.g. polymorphic/dependent) type theories over the simple type theory in lambda calculus? Are they more 'powerful' in some sense; if so, how exactly?
    • They do add power. Under the formulae-as-types correspondence, the simply-typed lambda calculus has as its matching logic propositional calculus, adding dependent types adds universal and existential quantification at higher finite types to its logic. Polymorphic types allow types allowing all usual mathematical entities to be constructed (although without the usual theory of provability) and has high proof-theoretic consistency: Strong normalisation of system F has (over a base theory such as RCL0) the same strength as consistency second order arithmetic, even though it lacks an induction principle.
  5. Do semantics (interpretation) have anything to say here, with respect to typed and untyped theories, especially in terms of soundness and completeness?
    • They are much less useful with these sorts of theories than model theory is with classical logic, although there are good applications of category theory to the semantics of type theory.
  6. The well-known proof verifier Coq, which (I believe) uses a language of higher-order complex-typed lambda calculus to represent proofs in constructive (intuistionistic) mathematics. I have read that the theory behind it (the Calculus of Constructions) is essentially an extension of the Curry-Howard isomorphism to higher-order logic. Are there any elaborations/clarifications I should be aware of here?
    • Yes, that polymorphic types are tricky, and non-conservative over the base theory. I'd recommend sarting an exploration of formulae-as-types with Martin-Löf's dependent type theory. If you want to work with a proof assistant, there is Agda, which is a functional programming language whose type system is Martin-Löf's type theory.
$\endgroup$
9
  • $\begingroup$ Thanks Charles. Your expertise on formal logic and proof theory is a valuable resource around here! I'm just going to wait and see if anyone else has something more to offer here, but this is pretty thorough. I'll read it over properly tomorrow morning and reply with any queries, since it's a bit late now. No need to post on cstheory now however, it seems. $\endgroup$
    – Noldorin
    Sep 28, 2010 at 18:25
  • $\begingroup$ @Noldorin: It's a bit sketchy, what I wrote, and rather simplified. I could qualify several things I wrote, e.g., you can give type systems to untyped lambda calculus, such as intersection types, but it's tricky to argue these give a proof theory. $\endgroup$
    – Charles Stewart
    Sep 29, 2010 at 7:16
  • $\begingroup$ Ok, a few follow up questions... 1) What specifically is the consequence of lacking a normal-form theorem? i.e. In terms of soundness/completeness/decidability? 2) What are the proof-theoretical restrictions of Church's simple theory of types? 3) What sort of type system admits the most power proof calculus. 4) Why do most/all proof verification systems today use a functional (higher-order lambda calculus) approach rather than an imperative (Turing machine) approach? I guess I'm looking for an overview again here mainly, though details could always help. $\endgroup$
    – Noldorin
    Sep 30, 2010 at 19:44
  • 2
    $\begingroup$ @Noldorin: (1) The normal form theorem is the foundation for the proof theory of natural deduction. A system of natural deduction might have soundness/completeness/decidability, but you are not going to be able to prove those results in the proof theory of natural deduction. (2) It's basically multi-sorted first-order logic. (3) Polymorphic ones. (4) I'm not really sure. The lambda calculus is a very convenient syntax. I should think that another approach is viable, but you'd need to show the alternative has an important edge on the current approach to gain acceptance. $\endgroup$
    – Charles Stewart
    Oct 1, 2010 at 12:55
  • 1
    $\begingroup$ @Noldorin: (1b) Proof theory is well suited to proving consistency and decidability; with soundness one has to ask, soundness with respect to what? You can construct models proof theoretically: this is the key to Gödel's completeness theorem. The point is, if you can't prove these results, the problem might not lie in your incompetence or bad properties of the logical consequence relation, but in the unsuitability of the proof calculus for the task. (2) Yes. (3) Coq uses both polymorphic and dependent, and an induction schema, because polymorphism gives you recursion but not induction. $\endgroup$
    – Charles Stewart
    Oct 2, 2010 at 9:27

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .