This article introduces the axiomatic semantics of typed lambda calculus. Recall that “axiomatic semantics consists of a proof system for deducing properties of programs and their parts.” The equational proof system of typed lambda calculus may be used to derive equations that hold in all models, and to derive equations that follow from equational hypothesis.
Equations
A typed equation has the form
\[\phantom{\stackrel{\text{def}}{=}} \Gamma \:\triangleright\: M = N:\tau\]where we assume that $M$ and $N$ have type $\tau$ in context $\Gamma$.
Intuitively, the equation \(\{ x_1:\sigma_1 ,..., x_k:\sigma_k \} \:\triangleright\: M = N:\tau\) means that for all type-correct values of the variables $x_1:\sigma_1 ,…, x_k:\sigma_k$, expressions $M$ and $N$ denote the same element of type $\tau$. Another way of writing this equation might be
\[\forall x_1:\sigma_1 ...\forall x_k:\sigma_k \: .\: M = N:\tau.\]Because the variables listed in the type assignment are universally quantified, an equation may hold vacuously if some type is empty.
For example, if $\sigma$ is empty, then the equation \(\forall x:\sigma . \forall y:\rho . M = N:\tau\) is true simply because there is no possible value for $x$.
Since we include type assignments in equations, we have an equational version of the typing rule that adds variables to type assignments,
\[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma \:\triangleright\: M = N:\sigma}{\Gamma , x:\tau \:\triangleright\: M = N:\sigma} \tag*{($add \: var$)}\]The next group of axioms and inference rules make provable equality an equivalence relation.
\[\Gamma \:\triangleright\: M = M:\sigma \tag*{($ref$)}\] \[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma \:\triangleright\: M = N:\sigma}{\Gamma \:\triangleright\: N = M:\sigma} \tag*{($sym$)}\] \[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma \:\triangleright\: M = N:\sigma ,\: \Gamma \:\triangleright\: N = P:\sigma}{\Gamma \:\triangleright\: M = P:\sigma} \tag*{($trans$)}\]An equivalence relation is a binary relation that is reflexive, symmetric and transitive. More to see this wiki page.
The two term-formation operations of $\lambda^\to$ are abstraction and application, both of which preserve equality. The rule
\[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma,x:\sigma \:\triangleright\: M = N:\tau}{\Gamma \:\triangleright\: \lambda x :\sigma.M = \lambda x :\sigma.N:\sigma \to \tau} \tag*{($\xi$)}\]says that if $M$ and $N$ are equal for all values of $x$, then the two functions $\lambda x :\sigma.M$ and $\lambda x :\sigma.N$ are equal.
For application, we have the rule
\[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma\:\triangleright\: M_1 = M_2:\sigma \to \tau,\: \Gamma \:\triangleright\: N_1 = N_2:\sigma}{\Gamma \:\triangleright\:M_1\: N_1 = M_2\:N_2:\tau} \tag*{($\nu$)}\]saying that equals applied to equals yield equals.
It is interesting to note that these two rules have the same form as the introduction and elimination rules for $\to$.
For $\lambda^\to$, three axioms remain. The first describes the renaming of bound variables, while the other two specify that the introduction and elimination rules are “inverses” of each other. These axioms are already illustrated in previous articles, so we just list them below and will not discuss them in detail here.
\[\Gamma \:\triangleright\: \lambda x:\sigma.M = \lambda y:\sigma.[y/x]M : \sigma \to \tau \text{, provided } y \notin FV(M)\tag*{($\alpha$)}\] \[\Gamma \:\triangleright\: (\lambda x:\sigma.M)\:N = [N/x]M : \tau \tag*{($\beta$)}\] \[\Gamma \:\triangleright\: \lambda x:\sigma.(M\:x) = M : \sigma \to \tau \text{, provided } x \notin FV(M)\tag*{($\eta$)}\]$FV(M)$ represents the set of free variables in $M$, i.e., the variables appearing in $M$ that are not bound by $\lambda$.
Theories
A typed lambda theory (or $\boldsymbol{\lambda^\to}$ theory) over signature $\Sigma$ is a set of well-typed equations between $\Sigma$-terms that includes all instances of the axioms and is closed under the inference rule. We use the word “closed” here to mean that any equation deduced from inference rules will not go outside of this set.
If $\mathcal{E}$ is any set of well-typed equations, we write \(\mathcal{E} \vdash \Gamma\:\triangleright\: M= N:\sigma\) to mean that the equation \(\Gamma\:\triangleright\: M= N:\sigma\) is provable from the axioms and equations of $\mathcal{E}$. We write \(\vdash \Gamma\:\triangleright\: M= N:\sigma\) when $\mathcal{E}$ is an empty set.
If you have read the Correspondence between Formulas and Types section in the last article, the symbol $\vdash$ is already familiar to you. We put a further explanation of this symbol at the end of this article.
The theory of $\boldsymbol{\mathcal{E}}$, written $Th(\mathcal{E})$, is the set of equations provable from the axioms and equations of $\mathcal{E}$.
Exercises
In this section, we try to prove some properties using the above typed lambda theory.
(Lemma 1.) If \(\vdash \Gamma\:\triangleright\: M = N:\sigma\) and $\Gamma \cap \Gamma’$ contains all free variables of $M$ and $N$, then \(\vdash \Gamma'\:\triangleright\: M = N:\sigma\).
(Proof.) This lemma can be easily proved by induction on equational proofs.
Let $\Gamma_M$ be the set of type assumptions $x:\sigma$ with $x \in FV(M)$. The induction base case is that $\Gamma$ only contains all free variables of $M$, i.e., $\Gamma = \Gamma_M \subseteq \Gamma’$. In this case, we may get $\Gamma’$ by adding variables into $\Gamma$. According to the ($add$ $var$) rule, this process will not affect the equation $M=N:\sigma$, so the lemma holds.
When $\Gamma$ contains some variable not appearing in $M$ or bound by $\lambda$, we need to induce on each equational rule to show the lemma still holds. We take a proof ending with ($\to$ $\text{Intro}$) as an example, where we need to derive
\[\phantom{\stackrel{\text{def}}{=}} \vdash \Gamma_M\:\triangleright\: \lambda x:\sigma.\:M = N:\sigma \to \tau\]from
\[\phantom{\stackrel{\text{def}}{=}} \vdash \Gamma_M,\: x:\sigma\:\triangleright\: \lambda x:\sigma.\:M = N:\sigma \to \tau.\]Since $x$ is bound in \(\lambda x:\sigma.\:M\), it is safe to remove $x:\sigma$ from type assumptions without affecting the equation. So the lemma follows by rule ($\to$ $\text{Intro}$). Other rules can be proved similarly. $\blacksquare$
(Lemma 2.) The substitution rule
\[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma,\:x:\sigma\:\triangleright\: M=N : \sigma,\: \Gamma \:\triangleright\: P=Q : \sigma}{\Gamma \:\triangleright\: [P/x]M=[Q/x]N : \tau} \tag*{($subst$)}\]is a provable proof rule of $\lambda^\to$.
(Proof.) From \(\Gamma,\:x:\sigma\:\triangleright\: M=N : \sigma\), we can prove
\[\phantom{\stackrel{\text{def}}{=}} \Gamma\:\triangleright\: \lambda x:\sigma.\:M=\lambda x:\sigma.\:N : \sigma \to \tau\]by rule ($\xi$). Then by rule ($\nu$), we have
\[\phantom{\stackrel{\text{def}}{=}} \Gamma\:\triangleright\: (\lambda x:\sigma.\:M)\:P=(\lambda x:\sigma.\:N)\:Q : \tau.\]The lemma follows by ($\beta$) and transitivity. $\blacksquare$
(Proposition.) There is a typed lambda theory $\mathcal{E}$ and terms $M$ and $N$ without $x$ free such that \(\mathcal{E} \vdash \Gamma,\:x:\sigma\:\triangleright\: M=N : \tau \:\) but \(\:\mathcal{E} \not\vdash \Gamma \:\triangleright\: M=N : \tau\).
(Proof.) Let us consider three lambda terms $f:\sigma \to \tau$, $a:\tau$, and $b:\tau$. Let $\mathcal{E}$ be a set of two equations \(x:\sigma\:\triangleright\: f \: x = a\) and \(x:\sigma\:\triangleright\: f \: x = b\). Then $Th(\mathcal{E})$ represents the theory consisting of all equations provable from them. Following from the transitivity we have the equation \(x:\sigma\:\triangleright\: a=b:\tau\) in $Th(\mathcal{E})$. However, we can see that \(\emptyset \:\triangleright\:a=b:\tau\) is not provable from $\mathcal{E}$, by the following semantic argument.
When $\sigma$ is an empty type, the equations \(f \: x = a:\tau\) and \(f \: x = b:\tau\) are true, since there is no possible value for $x:\sigma$. However, \(a=b:\tau\) does not hold in this case; they can be different values. As a result, we have \(\mathcal{E} \vdash x:\sigma \:\triangleright\: a=b : \tau\:\) but \(\:\mathcal{E} \not\vdash \emptyset \:\triangleright\: a=b : \tau\). $\blacksquare$
This proposition shows that an equation is not provable from some set of equations. Specifically, if we can find a theory satisfying $\mathcal{E}$ but not satisfying an equation $E$, then there cannot be a proof of $E$ from $\mathcal{E}$.
In cases where we do not know if an equation $E$ follows from a set of equations $\mathcal{E}$, we generally try both to prove $E$ from $\mathcal{E}$ and find a theory satisfying $\mathcal{E}$ but not $E$. In principle, one of these is possible. However, it is important to realize that there is a significant difference between searching for a proof and searching for a theory that demonstrates that there is no proof. The difference is that there is an effective and routine method for enumerating all proofs. Therefore, if there is a proof of $E$ from $\mathcal{E}$, a routine method will eventually find it. However, there is no routine method for finding a theory to show that there is no proof.
What is the Exact Meaning of $\vdash$ ?
In mathematical logic and computer science, the symbol $\vdash$ takes the name turnstile, because it resembles to a typical turnstile if viewed from above. It is often read as “yields”, “proves”, “satisfies” or “entails”.
In programming language theory literatures, $\vdash$ is heavily used, but it is not the programming language researchers who invent this symbol. In fact, it was originally used by logicians in proof calculus, or called proof system. To date, there are three most widely known proof calculus:
The class of Hilbert systems, of which the most famous example is the 1928 Hilbert–Ackermann system of first-order logic. We introduced this one in Easy Foundations for Programming Languages II — Notation and mathematical Conventions;
Gerhard Gentzen’s calculus of natural deduction, which is the first formalism of structural proof theory, and which is the cornerstone of the formulae-as-types correspondence relating logic to functional programming we discussed in Easy Foundations for Programming Languages VII — Simply-Typed Lambda Calculus;
Gentzen’s sequent calculus, which is the most studied formalism of structural proof theory.
There is another very famous but no longer widely used proof calculus — Aristotle’s syllogistic calculus, presented in his 350 BC book Prior Analytics. This book represents the first time in history when Logic is scientifically investigated.
The Aristotelian syllogism dominated Western philosophical thought for many centuries. Syllogistic arguments are usually represented in a simple three-line form:
All men are mortal.
Socrates is a man.
Therefore, Socrates is mortal.
Check this wiki page to see more about Syllogism.
In these proof calculus, suppose $\Gamma$ is a set of formulas, considered as hypotheses or assumptions. For example, $\Gamma$ could be a set of axioms for group theory or set theory.
The notation $\Gamma \vdash \phi$ means that there is a deduction that ends with $\phi$ using as axioms only logical axioms and elements of $\Gamma$. Thus, informally, $\Gamma \vdash \phi$ means that $\phi$ is provable assuming all the formulas in $\Gamma$. We write $\vdash \phi$ to mean that $\phi$ is provable without assumption.
Suppose we have three formulas $\psi$, $\omega$, and $\phi$. To express “$\phi$ is provable when $\psi$ and $\omega$ hold,” we have the following four kinds of style to write this inference rule.
\[\psi, \omega \vdash \phi\] \[\frac{\:}{\psi, \omega \vdash \phi}\] \[\frac{\psi, \omega}{\phi}\] \[\frac{\vdash \psi, \omega}{\vdash \phi}\]These four rules share the same meaning in logic. In essence, you may use whichever you like.
In many literature on type systems, natural deduction or sequent calculus are used. In these sources, it is common to use $\Gamma \vdash M:\sigma$ to indicate that the typing assertion $M:\sigma$ is provable from the set $\Gamma$ of typing assumptions. In our series, however, we use the symbol $\triangleright$ in type assertions instead of $\vdash$, because we want to differentiate the type system from the equational proof system introduced in this article.