6
$\begingroup$

It is well-known that the simply typed lambda calculus is strongly normalizing (for instance, Wikipedia). Hence, it is not strong enough to be Turing-complete, as also mentioned on the Wikipedia page for Turing-completeness. Its strength is usually compared to propositional logic (I think intuitionistic), and one way to show this is the Curry-Howard Correspondence.

However, it also seems to be well known that the simply typed lambda calculus is equivalent to "simple type theory," which is equivalent to higher order logic and hence has no sound, complete, effective proof system. For example, see the article "Seven Virtues of Simple Type Theory", which cites Godel's theorem and explicitly addresses the "virtue" that STT can create categorical theories (such as second-order PA).

How can these two things possibly both be true? What is the correct way of understanding this?


EDIT: people have asked for some references on the equivalence between the terms "Simply Typed Lambda Calculus" and "Simple Type Theory." When I said that, I didn't mean they were two different systems that admit some technical "equivalence," but rather that I have generally seen the two terms used interchangeably to mean the same thing, which is the thing defined in Alonzo Church's 1940 paper.

To be clear, this paper describes a simply typed lambda calculus with two base types - that of propositions and that of "individuals" (not the same as a primitive "integer" type, but more general and without any particular description of the inhabitants of that type). He also defines as primitives negation, logical OR, universal quantification, and a definite description operation, from which he further derives existential quantifiers, an implication relation, a propositional bidirectional implication, an equality relation on "individuals," an encoding of numerals with a "successor relation," and so on.

Church also gives an inference system as a list of additional axioms. His axioms 1-4 are sufficient to derive the law of excluded middle, adding his axioms 5-6 are sufficient for the "logical functional calculus" (which I believe is his term for first-order logic, given that these axioms define how quantifiers work), axioms 7-9 describe the universe of individuals and yield that there are infinitely many, 10-11 give axioms of extension and choice. Church describes which axioms are required to prove different theories; axioms 1-4 are sufficient for "propositional calculus," 1-6 are sufficient for "logical functional calculus" (FOL?), 1-9 are sufficient for "elementary number theory," 1-11 are sufficient for "classical real analysis."

Church then goes onto derive the Peano axioms from the above, including the Peano induction axiom. I am not sure how strong the induction axiom is.

There are a few other papers describing ways to simplify Church's system: for instance, you can derive quantifiers from lambda plus definite description (Quine 1956, Henkin 1963). A good reference for these is Stanford's Encyclopedia page on Church's Type Theory.

Here are a few examples in which the terms "Simply Typed Lambda Calculus" and "Simple Type Theory" are used to describe the same system from Church's paper:

Referring to Church's System as "Simply Typed Lambda Calculus"

  • Wikipedia's page on the Simply Typed Lambda Calculus states in the first paragraph "The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical uses of the untyped lambda calculus, and it exhibits many desirable and interesting properties."
  • In general, Wikipedia is fairly uniform in defining the "simply typed lambda calculus" as the typed lambda calculus without polymorphic types, dependent types, etc, and explicitly citing Church's version.
  • Thierry Coquand's course notes on Type Theory says: "Church formulated then an elegant formulation of higher-order logic, using simply typed λ-calculus 5, which can be seen as a simplification of the type system used in Principia Mathematica, but also is in some sense a return to Frege."
  • In general, an arXiv search for "Simply Typed Lambda Calculus" "Higher Order Logic" yields plenty of results. For instance, see the paper "An overview of type theories" by Nino Guallart, which says "Simply typed lambda calculus. Simply typed lambda calculus was also originally developed by Church (1940,1941). It is a higher order logic system based on lambda calculus and it uses the same syntax."

Referring to Church's System as Simple Type Theory

  • The article Seven Virtues of Simple Type Theory refers to Church's system instead as "Simple Type Theory," and says "In 1940 A. Church presented an elegant formulation of simple type theory, known as Church's type theory..." They claim that the abstract "simple type theory" that Church's version is "a formulation of" is equivalent to Russell's "ramified theory of types plus the Axiom of Reducibility."
    • The same article writes "Simple type theory, also known as higher-order logic, is a natural extension of first-order logic. It is based on the same principles as first-order logic but differs from first-order logic in two principal ways. First, terms can be higher-order, i.e., they can denote higher-order values such as sets, relations, and functions. Predicates and functions can be applied to higher-order terms, and quantification can be applied to higher-order variables in formulas."
    • Seven Virtues gives an explicit formulation of "a version" of "Simple Type Theory" which is claimed to be "a version of" Church's theory and equivalent to it. Their derivation seems to be equivalent to the one on Stanford's page, which shows that some of Church's primitives (such as universal quantification) are redundant and can be derived from lambda plus equality.
    • The "Seven Virtues" paper proves as a theorem that any nth-order logic can be embedded in their STT, which they prove in Theorem 2.
  • The Stanford Encyclopedia of Philosophy has an article on "Church's Type Theory," for which they make clear that they consider Church's theory "a formulation of" type theory, and also state "Type theories are also called higher-order logics, since they allow quantification not only over individual variables (as in first-order logic), but also over function, predicate, and even higher order variables."
  • All such examples above referring to "Simple Type Theory" or "Church's Type Theory" do not incorporate any notion of polymorphic types, dependent types, etc.
  • In general it is also not difficult to find references citing Church's paper and using the term "Simple Type Theory" for it. Here is an arXiv paper called Formalising Mathematics In Simple Type Theory that says "Higher-order logic is based on the work of Church 10, which can be seen as a simplified version of the type theory of Whitehead and Russell."

So that was my point. I have seen the terms "STLC" and "STT" used interchangeably to describe the same system, which is Church's typed system, or various equivalent formulations of it. The terminology seems messy and I am not sure exactly in what sense Church's system is or isn't stronger than FOL.

$\endgroup$
  • 1
    $\begingroup$ @user40276: You wrote this comment as I was editing my post for clarification. The point is that the simply typed lambda calculus is typically considered to be equivalent in expressive power to propositional logic (i.e. it is not strong enough to be Turing complete). I don't understand how this is possible, given that it is also stronger than first-order logic. $\endgroup$ – Mike Battaglia Jan 30 at 3:43
  • 5
    $\begingroup$ @MikeBattaglia: Andrej’s answer lays out a lot of the relevant situation quite well, but for resolving the apparent contradiction you outline, I recommend just (1) expand the beliefs you’ve stated briefly (like “STLC is equivalent to STT”) into fully precise and unambiguous statements of what you believe to hold; (2) try to make precise your argument for how they’re contradictory. The trouble in logic is that terminology is not very well standardised, especially in comparing different kinds of logical systems, [cont’d] $\endgroup$ – Peter LeFanu Lumsdaine Jan 30 at 11:46
  • 4
    $\begingroup$ so something like “system ABC is equivalent to system XYZ” may mean several reasonable but different things to different people, and it’s very easy to read a paper that summarises its results as “ABC is equivalent to XYZ”, remember the summary not the precise results, and end up with the belief that ABC is equivalent to XYZ in some stronger (or just different) form from what the paper actually showed. $\endgroup$ – Peter LeFanu Lumsdaine Jan 30 at 11:49
  • 2
    $\begingroup$ I think that one source of confusion is that the same paper of Church "introduced" both STLC and STT, but nowadays they are used to mean different things. I think most of your sources for "Referring to Church's System as STLC" are actually intending to say that Church's theory was the first STLC, not that what we nowadays mean by "STLC" is identical to Church's system. $\endgroup$ – Mike Shulman Jan 31 at 0:41
  • 1
    $\begingroup$ Nowadays STLC refers to a general class of theories, as Andrej says in his answer (and if you read the rest of the Wikipedia page you'll see that), whereas Church's theory (nowadays STT or HOL) is built on top of a particular STLC but augments it with extra power such as propositions and connectives and deduction rules. But when Church wrote his original paper (I think), the general framework of STLC did not exist yet, so in defining STT he was implicitly also defining STLC as the foundation for it. Nowadays we disentangle the two, but we still credit Church with inventing both of them. $\endgroup$ – Mike Shulman Jan 31 at 0:42
19
$\begingroup$

The simply-typed $\lambda$-calculus is not stronger than second-order logic.

The simply-typed $\lambda$-calculus has:

  • product types $A \times B$, with corresponding term formers (pairing and projections)
  • function types $A \to B$, with corresponding term formers (abstraction and application)
  • equations governing the term formers and subtitution

The simply-typed $\lambda$-calculus does not postulate the existence of any types. Sometimes we postulate the unit type $1$, and often we postulate the existence of a collection of basic types, but without any assumptions about them being inhabited. This is akin to using a collection of propositional symbols in the propositional calculus, where we make no claims as to their truth value.

Simple type theory is simply-typed $\lambda$-calculus and additionally at least:

  • the type of truth values $o$, with the corresponding term formers (constants $\bot$ and $\top$, connectives, quantifiers at every type)
  • the type of natural numbers $\iota$, with the corresponding term formers (zero, succcesor, primitive recursion into arbitrary types)
  • equations governing the term formers and substitution

There are several variations:

  • we may postulate excluded middle for truth values
  • we may include a definite description operator
  • we may include the axiom of choice
  • we may vary the extensionality principles

We quickly obtain a formal system that expresses Heyting (or Peano) arithmetic and more, which suffices for incompleteness phenomena to kick in.

What I think is confusing you is the fact that there are two ways to relate logic to type theory:

  1. The Curry-Howard correspondence relates the propositional calculus to the simply-typed $\lambda$-calculus by an interpreation of propositional formulas as types.

  2. Higher-order logic embeds into simple type theory by an interpretation of logical formulas as terms of the type $o$ of truth values.

There is a difference of levels, which makes all the difference.

To illustrate, consider the propositional formula $$p \land q \Rightarrow (r \Rightarrow p \land r).$$ In the simply typed $\lambda$-calculus it is interpreted as the type $$P \times Q \to (R \to P \times R).$$ To prove the formula amounts to giving a term of the type. In constrast, in simple type theory it is interpreted as the term $$p \land q \Rightarrow (r \Rightarrow p \land r) : o$$ (with parameters $p, q, r$ of type $o$). Now proving the formula amounts to proving the equation $(p \land q \Rightarrow (r \Rightarrow p \land r)) =_o \top$ in the simple type theory.

A higher-order formula, such as $(\forall r : \mathsf{Prop} . r \Rightarrow p) \Rightarrow p$ cannot be encoded in the simply-typed $\lambda$-calculus, whereas in the simple type theory it is again just a term of type $o$ (just replace the sort of propositions $\mathsf{Prop}$ with the type $o$).

Also note that the pure simply-typed $\lambda$-calculus does not postulate the natural numbers. If we add the natural numbers to the simply-typed $\lambda$-calculus we get a fragment of simple type theory known as Gödel's System T (or a version of it, depending on minutiae of how equality is treated), which suffers from – or enjoys, depending on your point of view – the incompleteness phenomena already.

$\endgroup$
  • $\begingroup$ To my knowledge, System T has product types but simply typed lambda calculus does not (at least according to Church: "A Formulation of the Simple Theory of Types" and Benzmüller, Miller: "Automation of Higher-Order Logic", which are my standard sources regarding STT). $\endgroup$ – lambda.xy.x Jan 30 at 17:28
  • $\begingroup$ Andrej - as per request, I just edited my original post to try to clarify. I am somewhat confused about the distinction between STLC and STT, since in the sources I had read, those terms have both been used to describe Church's paper (and papers describing related/equivalent systems simplifying it). In Church's system there is a basic propositional type and a basic type of individuals (which seems to be more general than the naturals). Is the term "STLC" used in some settings to exclude things like Church's system? I would appreciate some reading material if you have some. $\endgroup$ – Mike Battaglia Jan 30 at 18:32
  • 1
    $\begingroup$ The product types are inessential as far as expressive power is concerned. $\endgroup$ – Andrej Bauer Jan 30 at 19:12
  • 3
    $\begingroup$ I recommend taking heed of Peter Lumsdaine's advice: the terminology is not standard, and there are many variants of everything. Products or no products? Is equality up to $\beta$ or up to $\beta\eta$-equivalence? Do we assume any basic types, and how many? And so on, and so on. The only safe way is to always make precise references to precisely given formal systems, and not to assume anything. $\endgroup$ – Andrej Bauer Jan 30 at 19:14
  • 1
    $\begingroup$ What I tried to convey in my answer is a possible source of confusion. I believe my use of terminology is broadly standard. But please keep in mind that STLC and STT are not exactly defined. Even things like "first-order logic" and "set theory" are not precisely defined, and there are many versions of everything. Fortunately, mathematics is robust with respect to foundations. $\endgroup$ – Andrej Bauer Jan 30 at 19:17
4
$\begingroup$

Simply typed lambda calculus and simple type theory are not equivalent. The former only has rules for alpha- and beta-reduction, the latter also has rules for Modus Ponens, extensionality and the Introduction of the quantification constant $\Pi$. The normalization results for lambda calculus only refer to rewriting modulo alpha- and beta reduction (there are also variants including eta, an extensionality rule for lambda terms). I will give a common set of rules below (following: Benzmüller, Miller: Automation of Higher-order Logic).

What is a little confusing is that lambda calculus can encode proofs in simple type theory. This is usually done via the Curry-Howard isomorphism but Farmer uses a different encoding. In both cases, we can verify a proof term by normalization but we can not find these terms by reduction.

  • Simply typed LC (Church style)

    The types $o$ and $\iota$ are basic types. Every basic type is a (complex) type. Let $\tau_1, \tau_2$ be (complex) types, then the type application $\tau_1 \rightarrow \tau_2$ is a complex type.

    Terms are inductively defined:

    • A variable $x$ of type $\tau$ is a term of type $\tau$
    • Let $s$ be a term of type $\tau_1 \rightarrow \tau_2$ and $t$ be a term of type $\tau_1$. Then the application $s t$ is a term of type $\tau_2$
    • Let $x$ be variable of type $\tau_1$ and $t$ be a term of type $\tau_2$, then $\lambda x.t$ is a term of type $\tau_1 \rightarrow \tau_2$.

    We define the following inferences on lambda terms:

    • $\alpha$-equivalence: $(\lambda x.t[x]) = (\lambda y.t[y])$ when $x,y$ do not appear in t otherwise.
    • $\beta$-equivalence: $(\lambda x.s[x])t = s[t]$ when $x$ does not appear in $t$. Rewriting the equation left to right is called a $\beta$-reduction; rewriting right to left is called $\beta$-expansion.

    Remark: I made the containment requirements stricter than necessary to simplify the presentation. The main issue is overbinding, iotw. that $(\lambda x \lambda y.f x y) y$ $\beta$-reduces to $\lambda z.f y z$ but not to $\lambda y. f y y$.

    The decidability result you mentioned is that continued $\beta$-reduction of a term modulo $\alpha$-equivalence terminates and results in a normal form. There is also an upper bound ($O(2\uparrow\uparrow$n)) to the growth in size during this process such that we cannot express any function that grows faster than that.

  • Elementary type theory: We assume the existence of variables for the logical connectives ($¬,∨,\Pi)$ of types $o\rightarrow o$, $o\rightarrow o \rightarrow o$ and $(\alpha \rightarrow o) \rightarrow o$. The connectives $\land,⊃$ can be derived the same way as in FOL. $\Pi$ represents universal quantification; $\forall x.f$ is defined as $\Pi \lambda x.f$ and $\exists x.f = \neg \forall x.\neg f$.

    We also add the following inference rules to typed LC:

    • Substitution: given the term $f x$ where $x$ is not free (*), infer the term $f a$ (under the condition that $x$ and $a$ have the same type)
    • Modus Ponens: from $f$ and $f ⊃ g$ infer $g$
    • Generalization: from $f x$ infer $\Pi f$ if $x$ is not free in $f$

    We also assume some Hilbert-style axioms describing the logical connectives.

  • Simple type theory: We add even more axioms to elementary type theory: extensionality, Leibniz equality, number theory, description and choice.

It should be intuitive that applying inferences cannot terminate even for elementary type theory: after all, it allows to derive logical consequences for which $\beta$-reduction is not sufficient. LC is still a quite expressive language which even allows to encode proofs - it's just not strong enough to express the proof search.

Remark: the logical connectives can be defined in multiple ways, e.g. Andrews builds up the whole theory based on an equality predicate.

(*) a variable $x$ is bound in a term if it occurs inside an abstraction $\lambda x.t$ over $x$. All occurrences of a variable that are not bound are free occurrences.

$\endgroup$
  • 1
    $\begingroup$ Hello lambda.xy.x - since you wrote this, I have since edited my original post to further clarify what I am trying to ask. Basically, though, I am very confused on how STLC and STT differ - all resources I can find using either of those terms cite Church's paper as having introduced "STLC" or "STT" or whatever. $\endgroup$ – Mike Battaglia Jan 30 at 18:37
  • 1
    $\begingroup$ For example, in your comment to Andrej above, you say "STLC" doesn't have product types, citing Church's paper. But if Church's paper is an example of "STLC," then Church's paper also has universal quantification $\Pi$ as a primitive symbol, for example, but in this answer you say that "STLC" doesn't have quantification. Church's paper also had a set of axioms that could be used for inference (including extensionality and so on), but the quantification constant is defined before any of those and is a primitive symbol of his theory, whether it's "STT" or "STLC" or something else. $\endgroup$ – Mike Battaglia Jan 30 at 18:39
  • $\begingroup$ I updated the text that it becomes clearer - Church did not make a difference between the lambda calculus as a term language and his Hilbert system. Since LC by itself is already pretty useful, the two were disentangled at some point. $\endgroup$ – lambda.xy.x Jan 31 at 16:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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