Today, we are going to present the pure simply-typed lambda calculus. PCF is extended from this system by adding natural numbers, booleans, and fixed-point operators.
In previous articles, we used PCF to describe the connections between typed lambda calculus and programming in some detail. Now we are more concerned with the mathematical properties of the system.
Church developed lambda calculus in the 1930’s as part of formal logic and as a formalism for defining computable functions. The original logic, which was untyped, was intended to serve a foundational role in the formalization of mathematics. Using lambda abstraction, logical quantifiers (such as universal, $\forall$, and existential, $\exists$, quantifiers) may be treated as constants, in much the same way that recursive function definitions may be treated using fixed-point constants.
In 1936, Kleene proved that the natural number functions definable in untyped lambda calculus are exactly the recursive functions. Turing, in 1937, then proved that the $\lambda$-definable numeric functions are exactly the functions computable by Turing machines. Together, these results, which are analogous to properties of PCF discussed in Easy Foundations for Programming Languages V — PCF Iteration and Recursion, establish connections between lambda calculus and other models of computation.
After the development of electronic computers, untyped lambda calculus clearly influenced the development of Lisp in the late 1950’s. General connections between lambda notation and other programming languages were elaborated throughout 1960’s by various researchers, leading to the view that the semantics of programming languages could be given using extensions of lambda calculus.
Types
We use the phrase “simply-typed lambda calculus” to refer to typed lambda calculus with only one type constructor ($\to$) that builds function types. It is the canonical and simplest example of a typed lambda calculus.
To define the types, a set of base types (like $bool$ and $nat$), $B$, must first be defined. These are called type constants. With this fixed, the syntax of types is given by the following grammar:
\[\sigma ::= b \mid \sigma \rightarrow \sigma\]where $b \in B$.
For example, \(B = \{a,b\}\) generates an infinite set of types starting with $a$, $b$, $a \to a$, $a \to b$, $b \to b$, $b \to a$, $a \to (a \to a)$, $…$.
When parentheses are omitted, we follow the convention that $\rightarrow$ associates to the right. For example, $a \rightarrow b \rightarrow c$ is read as $a \rightarrow (b \rightarrow c)$.
In addition, we give $\times$ higher precedence than $\rightarrow$, and $\rightarrow$ higher precedence than $+$, so that $a + b \times c \rightarrow d$ is read as $a + ((b \times c) \rightarrow d)$.
We name versions of typed lambda calculus by their types. The simplest langauge, called simply-typed lambda calculus with function types, will be indicated by the symbol $\lambda^\rightarrow$. With sums, products and functions, we have $\lambda^{+,\times,\rightarrow}$, and so on. A $\boldsymbol{\lambda^\rightarrow}$ type expression is a type expression containing only $\rightarrow$ and type constants.
Terms
Context-Sensitive Syntax
Programming languages are often defined using context-free grammar. However, a context-free description of a statically typed language only tells only half the story, since typing constraints are context-sensitive.
For example, the expression $x+3$ is well-typed only if the declaration of this $x$ specifies that $x$ is a numeric variable. In most languages, the declaration of $x$ may precede the expression $x+3$ by an arbitrary number of other declarations. It is not hard to prove that there is no context-free grammar generating precisely the well-typed terms of $\lambda^\rightarrow$.
We will define typed languages using a formalism based on logic. Specifically, we will define expressions and their types simultaneously using axioms and inference rules.
The atomic expressions of a language are given by typing axioms. Informally, a typing axiom $c:\tau$ means that the symbol $c$ has type $\tau$. Put another way, $c:\tau$ is an axiom that the type membership relation holds between $c$ and $\tau$. An example axiom for a language with natural numbers is $3:nat$, which specifies $3$ is a natural number.
The compound expressions and their types are defined using inference rules. There are rules that let us derive more complicated facts about the “$:$” relation. One form of the inference rule is
\[\frac{M_1:\sigma_1,...,M_k:\sigma_k}{N:\tau}.\]Intuitively, this rule says that if $M_1,…,M_k$ are well-formed terms of types $\sigma_1,…,\sigma_k$, respectively, then $N$ is a well-formed term of type $\tau$. Typically, $M_1,…,M_k$ are the subterms of $N$, since the type of a term will depend on the types of its subterms.
The inference rule above is not powerful enough to capture the context-sensitive syntax of expressions that declare the types of variables. To take the types of variables into account, we will work with typing assertions
\[\phantom{\stackrel{\text{def}}{=}} \Gamma \:\triangleright\: M:\tau ,\]where $\Gamma$ is a type assignment of the form
\[\Gamma = \{ x_1:\sigma_1,...,x_k:\sigma_k \},\]with no $x_i$ occurring twice.
Intuitively, the assertion \(\Gamma \:\triangleright\: M:\tau\) says that if variables $x_1,…,x_k$ have types $\sigma_1, …, \sigma_k$, respectively, then $M$ is a well-formed term of type $\tau$. A type assignment is also called a typing context so that \(\Gamma \:\triangleright\: M:\tau\) may be read, “in context $\Gamma$, the term $M$ has type $\tau$.”
In some presentations of typed languages and calculi, typing contexts are ordered sequences. Here, for simplicity, we consider type assignments unordered sets.
The general form of a typing rule with contexts is
\[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma_1\:\triangleright\: M_1:\sigma_1,...,\Gamma_k\:\triangleright\: M_k:\sigma_k}{\Gamma\:\triangleright\: N:\tau},\]which says that if each $M_i$ has type $\sigma_i$ in typing context $\Gamma_i$, then $N$ has type $\tau$ in context $\Gamma$. In all the typing rules we will use, the terms $M_1,…,M_k$ will be the subterms of $N$.
For any type assignment $\Gamma$, we write $\Gamma,x:\sigma$ for assigning a new variable $x$ into $\Gamma$. Namely,
\[\Gamma,x:\sigma \:\stackrel{\text{def}}{=}\: \Gamma \cup \{ x:\sigma \}.\]In doing so, we always assume that $x$ does not appear in $\Gamma$.
Syntax of $\lambda^\rightarrow$ Terms
The syntax of terms depends on the choice of type and term constants. A $\boldsymbol{\lambda^\rightarrow}$ signature $\Sigma = \langle B,C \rangle $ consists of
a set $B$ whose elements are called type constants or base types
and a collection $C$ of pairs of the form $\langle c,\sigma \rangle$, where $\sigma$ is a $\lambda^\rightarrow$ type expression over $B$ and no $c$ occurs in two distinct pairs.
A symbol $c$ occurring in some pair $\langle c,\sigma \rangle \in C$ is called a term constant of type $\sigma$. We generally write $c:\sigma$ if $\langle c,\sigma \rangle \in C$.
This definition of signature may seem too abstract to understand, so let’s directly look into an example. The $\lambda^\rightarrow$ signature, $\Sigma_\rightarrow$, is shown as below.
type constants: $nat, bool$
term constants:
- $0,1,2,3,4,…:nat$
- $true, false: bool$
- $plus: nat \rightarrow nat \rightarrow nat$
- $Eq?: nat \rightarrow nat \rightarrow bool$
- $cond_\sigma : bool \rightarrow \sigma \rightarrow \sigma \rightarrow \sigma \quad \text{ each type } \sigma$
- $fix_\sigma : (\sigma \rightarrow \sigma) \rightarrow \sigma \quad \text{ each type } \sigma$
We may write terms over this signature in the familiar form of PCF using the syntactic sugar
\[\begin{split} M + N &\:\stackrel{\text{def}}{=}\: plus \: M \: N\\ \text{if } M \text{ then } N \text{ else } P &\:\stackrel{\text{def}}{=}\: cond_\sigma \: M \: N \: P \end{split}\]where the type subscript on $cond$ is determined by the types of $N$ and $P$.
The $\lambda^\rightarrow$ terms over $\Sigma$ and their types are defined simultaneously using axioms and inference rules. For each term constant $c$ of type $\sigma$, we have the axiom
\[\emptyset \:\triangleright\: c:\sigma \tag*{($cst$)}\]The typing context here is empty, since the type of a constant is fixed, and therefore independent of the context in which it occurs.
We assume some countably infinite set $Var$ of variables \(\{ v_0, v_1,... \}\). Variables are given types by the axiom
\[x:\sigma \:\triangleright\: x:\sigma \tag*{($var$)}\]where $\sigma$ must be a $\lambda^\rightarrow$ type over $\Sigma$. This axiom simply says that a variable $x$ has whatever type it is declared to have.
Compound expressions and their types are specified using inference rules. A straightforward one is the following “add var” rule that applies to terms of any form. The rule
\[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma \:\triangleright\: M:\sigma}{\Gamma, x:\tau \:\triangleright\: M:\sigma} \tag*{($add \: var$)}\]allows us to add an additional hypothesis to the typing context. In other words, this axiom says that adding another variable into context will not affect the type of $M$. Recall that in writing $\Gamma, x:\tau$ we assume $x$ does not appear in $\Gamma$. Consequently, the type of $M$ could not have depended on the type of $x$.
In lambda calculus, lambda abstraction is used to identify the variable that is used as the function argument. This is made precise by the following term-formation rule.
\[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma, x:\sigma \:\triangleright\: M:\tau}{\Gamma \:\triangleright\: (\lambda x:\sigma. \:M):\sigma \rightarrow \tau} \tag*{($\rightarrow \: $Intro)}\]Intuitively, the rule says that if $M$ specifies a result of type $\tau$ for every $x:\sigma$, then the expression \(\lambda x:\sigma. \:M\) defines a function of type $\sigma \rightarrow \tau$. (Other free variables of $M$ are unaffected by lambda abstraction, and must be given types in $\Gamma$.) This rule is called ($\rightarrow$ Intro) because it “introduces” a term of functional type. As mentioned before, the variable $x$ is bound in \(\lambda x:\sigma. \:M\).
Similarly, function applications are written according to the rule
\[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma \:\triangleright\: M:\sigma \rightarrow \tau,\: \Gamma \:\triangleright\: N:\sigma}{\Gamma \:\triangleright\: M \: N:\tau} \tag*{($\rightarrow \: $Elim)}\]which says that we may apply any function with type $\sigma \rightarrow \tau$ to an argument of type $\sigma$ to produce a result of type $\tau$. Note that while $\rightarrow$ appears in the antecedent, this symbol has been “eliminated” in the consequent, hence the name ($\rightarrow$ Elim).
We say $M$ is a $\boldsymbol{\lambda^\rightarrow}$ term over signature $\boldsymbol{\Sigma}$ with type $\boldsymbol{\tau}$ in context $\boldsymbol{\Gamma}$ if \(\Gamma \:\triangleright\: M :\tau\) is either a typing axiom for $\Sigma$, or follows from axioms by rules (\(add\: var\)), ($\rightarrow$ Intro) and ($\rightarrow$ Elim).
As an expository convenience, we will often write \(\Gamma \:\triangleright\: M :\tau\) to mean that “\(\Gamma \:\triangleright\: M :\tau\) is derivable,” in much the same way as one often writes a formula \(\forall \: x.P(x)\), in logic, as a way of saying “\(\forall \: x.P(x)\) is true.” A proof of a typing assertion is called a typing derivation.
Lemmas
There are four lemmas which can be proved by a straightforward induction on typing derivations. All of them are easy to understand intuitively, so we omit the proofs for them.
(Lemma 1.) If \(\Gamma \:\triangleright\: M :\sigma\), then every free variable of $M$ appear in $\Gamma$.
(Lemma 2.) If \(\Gamma \:\triangleright\: M :\sigma\) and $\Gamma \cap \Gamma’$ contains all free variables of $M$, then \(\Gamma' \:\triangleright\: M :\sigma\).
(Lemma 3.) If \(\Gamma \:\triangleright\: M :\sigma\) and $y$ does not occur in $\Gamma$, then \([y/x]\Gamma \:\triangleright\: [y/x]M :\sigma\).
(Lemma 4.) If \(\Gamma_1 ,x:\sigma \:\triangleright\: M :\tau\) and \(\Gamma_2 \:\triangleright\: M :\sigma\) are terms of $\lambda^\rightarrow$, with $\Gamma_1 \cap \Gamma_2$ a well-formed type assignment, then the substitution instance \(\Gamma_1 \cap \Gamma_2\:\triangleright\: [N/x]M :\tau\).
These lemmas generalize to most type systems. Since all of the arguments are similar, we give only the proof of Lemma 4.
The proof is optional to read.
(Proof.) The proof of the lemma is by induction on the proof of typing assertion \(\Gamma_1 ,\: x:\sigma \:\triangleright\: M:\tau\). This is almost the same as induction on the structure of $M$, except that we have a stronger induction hypothesis for lambda abstractions, as noted below.
There are two base cases, one for the typing axiom for constants and one for the typing axiom for variables. However, the only axiom of the form \(\Gamma_1 ,\: x:\sigma \:\triangleright\: M:\tau\) is the variable axiom \(\Gamma_1 ,\: x:\tau \:\triangleright\: x:\tau\), with $\Gamma_1$ empty. We assume that \(\Gamma_2 \:\triangleright\: x:\tau\) is derivable. Since $[N/x]x$ is just $N$, the typing assertion \(\Gamma_1 \cap \Gamma_2\:\triangleright\: [N/x]x :\tau\) is just \(\Gamma_2 \:\triangleright\: x:\tau\) and therefore derivable. This proves the base case of the induction.
There are three induction steps, correponding to typing rules ($\to$ $\text{Intro}$),($\to$ $\text{Elim}$) and ($add$ $var$). A proof ending with ($\to$ $\text{Intro}$) concludes by deriving
\[\Gamma_1 ,\: x:\sigma \:\triangleright\: \lambda y:\tau'.\:M:\tau' \to \tau\]from
\[\Gamma_1 ,\: x:\sigma ,\: y:\tau' \:\triangleright\: M:\tau.\]Since \(\Gamma_1 ,\: x:\sigma ,\: y:\tau'\) is a well-formed type assignment, we know that $y$ does not appear in \(\Gamma_1 ,\: x:\sigma\). In particular, $y$ is different from $x$. (This would not be guaranteed if we tried to prove the lemma by induction on the structure of terms.)
By the inductive hypothesis,
\[\Gamma_1 \cup \Gamma_2,\: y:\tau' \:\triangleright\: [N/x]M:\tau\]is provable, and the lemma follows by rule ($\to$ $\text{Intro}$).
The induction step for a proof of \(\Gamma_1,\: x:\sigma \:\triangleright\: P:\tau' \to \tau\) and \(\Gamma_1,\: x:\sigma \:\triangleright\: Q:\tau'\) by rule ($\to$ $\text{Elim}$) is similar. By the induction hypothesis, both \(\Gamma_1 \cup \Gamma_2 \:\triangleright\: [N/x]P:\tau' \to \tau\) and \(\Gamma_1 \cup \Gamma_2 \:\triangleright\: [N/x]Q:\tau'\) are derivable and the lemma follows by rule ($\to$ $\text{Elim}$).
If the derivation of \(\Gamma_1,\: x:\sigma \:\triangleright\: M: \tau\) ends with ($add$ $var$), there are two cases to consider. The degenerate case is when ($add$ $var$) is used to add the hypothesis $x:\sigma$. In this case, $x$ does not appear in $M$ and so $[N/x]M \equiv M$. It follows from Lemma 2 that \(\Gamma_1 \cup \Gamma_2 \:\triangleright\: M:\tau\) is derivable. The final case is where ($add$ $var$) is used to add a hypothesis $y:\rho$, and \(\Gamma_1 \equiv \Gamma_1', y:\rho\). By the induction hypothesis, we know that since \(\Gamma_1' ,\: x:\sigma \:\triangleright\: M: \tau\) and \(\Gamma_2 \:\triangleright\: N: \sigma\) are derivable, so is \(\Gamma_1' \cup \Gamma_2 \:\triangleright\: [N/x]M:\tau\). The typing assertion \(\Gamma_1 \cup \Gamma_2 \:\triangleright\: [N/x]M:\tau\) follows by ($add$ $var$). This finishes the proof. $\blacksquare$
Terms with Product, Sum, and Related Types
The typing rules for the standard simply-typed extensions of $\lambda^\to$ are listed below.
For each version of simply-typed lambda calculus, the definition of signature and well-formed terms with respect to a given signature are analogous to the definitions for $\lambda^\to$. The definition of well-formed terms of $\lambda^{\to , \times}$ is stated below, to give an example, but the straightforward definitions for other variants are omitted.
Cartesian Product
Intuitively, a pair belongs to $\sigma \times \tau$ iff the first component belongs to $\sigma$, and the second component to $\tau$. One part of this “iff” is that if $M:\sigma$ and $N:\tau$, then the pair $\langle M,N \rangle$ has type $\sigma \times \tau$. This is written symbolically in the rule
\[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma \:\triangleright\: M:\sigma , \: \Gamma \:\triangleright\: N:\tau}{\Gamma \:\triangleright\: \langle M,N \rangle:\sigma \times \tau} \tag*{($\times \: $Intro)}\]which is called an introduction rule since it lets us “introduce” an element of product type. This rule implies that if $1:nat$ and $2:nat$, for example, then the pair $\langle 1,2 \rangle$ has type $nat \times nat$.
If $M$ is an element of type $\sigma \times \tau$, then $M$ consists of an element of $\sigma$ and an element of $\tau$. The rules
\[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma \:\triangleright\: M:\sigma \times \tau}{\Gamma \:\triangleright\: \mathbf{Proj}_1^{\sigma,\tau} M:\sigma} \tag*{($\times \: $Elim)$_1$}\] \[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma \:\triangleright\: M:\sigma \times \tau}{\Gamma \:\triangleright\: \mathbf{Proj}_2^{\sigma,\tau} M:\tau} \tag*{($\times \: $Elim)$_2$}\]describe the syntactic forms $\mathbf{Proj}_1^{\sigma,\tau} M$ and $\mathbf{Proj}_2^{\sigma,\tau} M$ which we use to obtain the first and second components of a pair $M:\sigma \times \tau$. These are called elimination rules since the $\times$ in the type of $M$ is “eliminated.” We often omit the type superscripts from $\mathbf{Proj}_1^{\sigma,\tau}$ and $\mathbf{Proj}_2^{\sigma,\tau}$.
We say \(\phantom{\stackrel{\text{def}}{=}} \Gamma \:\triangleright\: M:\sigma\) is a term of $\boldsymbol{\lambda^{\to , \times}}$ if \(\Gamma \:\triangleright\: M:\sigma\) is a typing axiom, or follows by rules ($add$ $var$), $(\times \text{ Intro})$, $(\times \text{ Elim})$, $(\to \text{ Intro})$, and $(\to \text{ Elim})$. All of the syntactic properties of $\lambda^\to$ terms mentioned in the last section extend easily to $\lambda^{\to , \times}$.
Sums
As we discussed in the last article, the term forms associated with sums are injection and case expressions. Terms of sum type are formed according to the following rules:
\[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma \:\triangleright\: M:\sigma}{\Gamma \:\triangleright\: \mathbf{Inleft}^{\sigma,\tau} M:\sigma + \tau} \tag*{($+ \: $Intro)$_1$}\] \[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma \:\triangleright\: M:\sigma}{\Gamma \:\triangleright\: \mathbf{Inright}^{\sigma,\tau} M:\sigma + \tau} \tag*{($+ \: $Intro)$_2$}\]These are called introduction rules since they introduce terms of sum type into the language. Intuitively, the injection functions map $\sigma$ or $\tau$ to $\sigma + \tau$ by “tagging” elements with $\mathbf{Inleft}$ or $\mathbf{Inright}$.
The elimination rule characterizes the type-correct use of case expressions.
\[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma \:\triangleright\: M:\sigma + \tau ,\: \Gamma \:\triangleright\: N:\sigma \to \rho ,\: \Gamma \:\triangleright\: P:\tau \to \rho}{\Gamma \:\triangleright\: \mathbf{Case}^{\sigma,\tau,\rho} M \: N \: P:\rho} \tag*{($+ \: $Elim)}\]Intuitively, \(\mathbf{Case}^{\sigma,\tau,\rho} M \: N \: P\) inspects the tag on $M$ and applies $N$ if $M$ is from $\sigma$ and $P$ if $M$ is from $\tau$.
Initial and Terminal Types
It is sometimes useful to have an initial (“empty”) type, $null$, or a terminal (“one-element”) type, $unit$. The only term form associated with $unit$ is the term constant
\[*:unit \tag*{($unit \: $Intro)}\]The term form associated with $null$ is that for each type $\sigma$, there is a term constant
\[\mathbf{Zero}^\sigma:null \to \sigma \tag*{($null \: $Elim)}\]Intuitively, $\mathbf{Zero}^\sigma$ is the empty function, “the function mapping nothing nowhere.” In the set-theoretic representation of functions as ordered pairs, $\mathbf{Zero}^\sigma$ is the empty set.
The constant $\ast$ is called an “Intro” form since it gives us a way of naming an element of type $unit$. The constant $\mathbf{Zero}^\sigma$ is called an “Elim” form since it gives us a way of using an element of type $null$ if we had one (which we generally do not).
Correspondence between Formulas and Types
This section is optional to read.
There is a correspondence between formulas of constructive logic and types in typed lambda calculus. The programming significance of this correspondence has been stressed by Martin-Löf and used as the basis for the Nuprl proof development system. we illustrate the main idea using implication logic.
For more about constructive logic, you may refer to this wiki page or the CMU textbook Constructive Logic, Frank Pfenning.
Logic formula is a type of syntactic formula that is well formed. If the values of all variables in a formula are given, it determines a unique truth value. You can check the boolean formula introduced in my blog Randomized Algorithm X — DNF & Monte Carlo Method for analogy.
Implicational propositional logic uses formulas that contain only propositional variables and implication, which we will write as $\rightarrow$. The formulas of implicational propositional logic are defined by the grammar
\[\sigma ::= b \mid \sigma \rightarrow \sigma\]where $b$ may be any propositional variable which can either be true or false.
Propositional logic applies natural deduction as the proof system, which is intended to mimic the common blackboard-style argument.
Assume $\sigma$.
By … we conclude $\tau$.
From this argument, we can see that $\sigma \to \tau$.
This argument begins by assuming some proposition $\sigma$, which is used to derive $\tau$. At this point, we have proved $\tau$ but the proof depends on the assumption of $\sigma$. In the third step of this argument, we observe that since $\sigma$ leads to a proof of $\tau$, the implication $\sigma \to \tau$ follows.
The natural deduction proof system for implicational propositional logic may be characterized using an axiom and three inference rules. Before giving them out directly, we first go through some notations we will use.
For technical reasons, we use labeled assumptions. Namely, if $x$ is a label and $\sigma$ a formula, then we write $x:\sigma$ for the assumption of $\sigma$ with label $x$.
Let $\Gamma$ be a finite set of labeled assumptions. We use the notation $\Gamma \vdash_M \sigma$ to mean that $M$ is a proof with consequence $\sigma$, relying on the set $\Gamma$ of labeled assumptions. For example, we may write $x:\sigma,y:\sigma \vdash_M \sigma$ to indicate that if $x$ and $y$ are assumptions of the formula $\sigma$, then $M$ is a proof of $\sigma$ that relies on assumptions $x$ and $y$.
Using these notations, the natural deduction proofs and their consequences are defined as follows: (The meaning of each is displayed in the Tip block.)
\[x:\sigma \vdash_x \sigma\]\[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma \vdash_M \sigma}{\Gamma,x:\tau \vdash_M \sigma} \quad x \text{ not in } \Gamma\]If $x$ is an assumption of $\sigma$, then $x$ is a proof of $\sigma$.
\[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma \vdash_M \sigma \to \tau, \: \Gamma \vdash_N \sigma}{\Gamma \vdash_{MN} \tau}\]If $M$ is a proof of $\sigma$ with assumptions $\Gamma$, then we may also consider $M$ a proof of $\sigma$ with assumptions $\Gamma, x:\tau$.
\[\frac{\phantom{\stackrel{\text{def}}{=}} \Gamma,x:\sigma \vdash_M \tau}{\Gamma \vdash_{\lambda x:\sigma.M} \sigma \to \tau}\]If $M$ is a proof of $\sigma \to \tau$ and $N$ is a proof of $\tau$, both with assumptions $\Gamma$, then $MN$ is a proof of $\tau$ with assumptions $\Gamma$.
If $M$ is a proof of $\tau$ with assumption $x$ of $\tau$, possibly among others, then $\lambda x:\sigma.M$ is a proof of $\sigma \to \tau$ with assumptions $x$ discharged.
A formula $\tau$ is provable if there is a proof $M$ with $\emptyset \vdash_M \sigma$.
Even when $\to$ is the only propositional connective, there are classical tautologies that are not intuitionistically provable. For example, it is easy to check that the formula $((a \to b) \to a) \to a$ is a classical tautology just by trying all possible assignments of $true$ and $false$ to $a$ and $b$. However, this formula is not intuitionistically provable.
In logic, a tautology is a formula that is true in every possible interpretation. An example is “$x=y$ or $x \neq y$”.
It is easy to see that we have just defined the typed lambda calculus: the terms of typed lambda calculus are precisely the proofs defined above and their types are exactly the formulas proved. Symbolically, \(\Gamma \vdash_M \sigma \: \text{ iff } \: \Gamma \:\triangleright\: M :\sigma\).
The correspondence is more than just a connection between terms and proofs. There are standard methods for simplifying proofs to normal forms that may be used to prove the consistency of various logics. This is one of the basic techniques of proof theory, discussed in Proofs and Types, JY Girard. For implicational logic, the proof simplifications are exactly the reduction rules on typed lambda terms. Thus, the formula-as-types correspondence has three parts:
\[\begin{split} \text{formula } \quad &\approx \quad \text{ type}\\ \text{proof } \quad &\approx \quad \text{ lambda term}\\ \text{proof normalization } \quad &\approx \quad \text{ reduction} \end{split}\]This correspondence is also called the Curry-Howard isomorphism. The correspondence extends to the other propositional connectives and quantifiers. The standard natural deduction proof rules for $\land$ and $\lor$ are precisely the formation rules given for product and sum types, respectively. The type constants $null$ and $unit$ correspond exactly to logical constants for $false$ and $true$. The quantifiers, which give us polymorphism and data abstraction, have more complicated correspondence and we will not discuss it here.
As a conclusion, we state the following lemma.
(Lemma 5.) Let $\Sigma$ be a $\lambda^\to$ signature with one type constant, $b$, and no term constants. Then for every type $\sigma$ over this signature, there is a closed term $M:\sigma$ iff $\sigma$ is a true formula of classical propositional logic, reading $\to$ as implication and $b$ as $false$.