Return to Answer

• 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 to 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.

• 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.

Simply type 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).

• 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 to 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.

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).

• 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 to 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.

Simply type 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).

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 type 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 to 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.