Type Theory and Formal Proof

1. Untyped Lambda Calculus

Lambda calculus encapsulates a formation of the basic aspects of functions. Untyped lambda calculus means we do not consider the types in this chapter.

1.1. Constriction Principles

• Abstraction: From an expression \(M\) and a variable \(x\) we can construct a new expression \(\lambda x.M\). We call this the abstraction of \(x\) over \(M\).
• Application: From expressions \(M\) and \(N\) we can construct expression \(MN\). We call this application of \(M\) to \(N\).

1.2. Lambda Terms

Expressions in the lambda calculus are called lambda terms. We assume the existence of an infinite set \(V=\{x,y,z,\ldots\}\) of so-called variables while the below inductive definition establishes how the set \(\Lambda\) of all lambda terms are constructed:

1. Variable: If \(u\in V\), then \(u\in\Lambda\).
2. Application: If \(M\) and \(N\in\Lambda\), then \((MN)\in\Lambda\).
3. Abstraction: If \(u\in V\) and \(M\in\Lambda\), then \((\lambda u.M)\in\Lambda\).

An inductive definition of \(\Lambda\) means that the above definitions are the only ways to construct elements of \(\Lambda\). An alternative and shorter way is to define \(\Lambda\) via abstract syntax:

The syntactical identity of two lambda terms can be denoted with the symbol \(\equiv\).

The subterms of a given lambda term form a multiset:

1. Basis: \(\mathcal S(x)=x\), for each \(x\in V\).
2. Application: \(\mathcal S((MN))=\mathcal S(M)\cup\mathcal S(N)\cup\{(MN)\}\).
3. Abstraction: \(\mathcal S((\lambda x.M))=\mathcal S(M)\cup\{(\lambda x.M)\}\).

They follow reflexivity and transitivity. A proper subterm of \(M\) is \(L\) if \(L\not\equiv M\).

The expression have the following precedence and associativity:

• Parentheses in an outermost position may be omitted.
• Application is left-associative.
• Application takes precedence over abstraction.
• Successive abstractions may be combined in a right-associative way under one \(\lambda\).

1.3. Free and Bound Variables

Variable occurrences in a lambda term can be divided into three categories: free occurrences, bound occurrences and binding occurrences.

Binding variables are those occurred immediately after a \(\lambda\). In the construction of a lambda term, the single variable and the variables that aren’t bound by the binding variables are free variables. However, during the process of abstraction, an occurrence of \(x\) which is free in \(M\) becomes bound in \(\lambda x.M\); that is, abstraction of \(x\) over \(M\) binds all free occurrences of \(X\) in \(M\).

Then we have the following recursive rule, in which \(\mathcal F(L)\) denotes the set of free variables in the lambda term \(L\).

1. Variable: \(\mathcal F(x)=\{x\}\).
2. Application: \(\mathcal F(MN)=\mathcal F(M)\cup\mathcal F(N)\).
3. Abstract: \(\mathcal F(\lambda x.M)=\mathcal F(M)\setminus\{x\}\).

The lambda term is closed if \(\mathcal F(M)=\emptyset\). A closed set is also called a combinator. The set of all closed lambda terms is denoted by \(\Lambda^0\).

1.4. Alpha Conversation

Functions in the lambda notation have the property that the name of the binding variable is not essential; the name is only used to express the transformation or procedure from input to output. Thus the relation alpha conversation or alpha equivalence is defined to describe this process formally. It’s based on the possibility of renaming binding (and bound) variables.

\(M^{x\to y}\) denote the result of replacing every free occurrence of \(x\) in \(M\) by \(y\). The relation \(\lambda x.M=_\alpha\lambda y.M^{x\to y}\) is called renaming.

In the renaming of \(\lambda x.M\) to \(\lambda y.M^{x\to y}\), it is prevented that the new binding variable \(y\) binds old free \(y\)s; and that any old binding \(y\) binds a new \(y\).

Alpha conversation follows compatibility, reflectivity, symmetry and transitivity. If \(M\) and \(N\) are said to be alpha convertible or alpha equivalent, then \(M\) is called an alpha variant of \(N\).

We can abstract from the names of the bound (and binding) variables, by considering lambda terms modulo alpha equivalence.

1.5. Beta Reduction

1. Basis: \((\lambda x.M)N\to_\beta M[x:=N]\).
2. Compatibility: If \(M\to_\beta N\), then \(ML\to_\beta NL\), \(LM\to_\beta NL\) and \(\lambda x.M\to_\beta \lambda x.N\).

The suffix \([x:=N]\) not in lambda terms, are meant to be meta-notation called substitution, which follow:

• \(x[x:=N]\equiv N\), \(y[x:=N]\equiv y\) if \(x\not\equiv y\).
• \((PQ)[x:=N]\equiv(P[x:=N])(Q[x:=N])\).
• \((\lambda y.P)[x:=N]\equiv\lambda z.(P^{y\to z}[x:=N])\), if \(\lambda z.P^{y\to z}\) is an alpha variant of \(\lambda y.P\) such that \(z\notin\mathcal F(N)\).

The subterm of the form \((\lambda x.M)N\) is called a redex (from reducible expression) and subterm \(M[x:=N]\) is called the contractum (of the redex).

Note that in general, the substitutions \(M[x:=N][y:=L]\) does not describe the same lambda term as \(M[y:=L][x:=N]\) because of the left associativity (\(M[x:=N][y:=L]\equiv M[y:=L][x:=N[y:=L]]\land x\notin\mathcal F(L)\)).

We define the relation \(\to_\beta\) to be one-step beta reduction since one redex is replaced by its contractum. The further beta reduction performed after the one-step reduction can be defined using \(\twoheadrightarrow_\beta\) which generally take zero or more step. We can prove that \(\twoheadrightarrow_\beta\) is reflective and transitive.

Similar to alpha conversation, we can define beta conversation or beta equivalence. If \(M=_\beta N\) and there is an \(n\geq 0\) and there are terms \(M_0\) or \(M_n\) such that \(M_0\equiv M\), \(M_n\equiv N\) for all \(i\) such that \(0\leq i<n\):

\(\twoheadrightarrow_\beta\) extends \(\to_\beta\) to multi-steps, while \(=_\beta\) further extends \(\twoheadrightarrow_\beta\) in both directions. Thus \(=_\beta\) is reflective, symmetric and transitive.

• \(M\) is in beta normal form if \(M\) does not contain any redex.
• \(M\) is beta normalizing if there is an \(N\) in beta normal form such that \(M=_\beta N\).

A reduction path from \(M\) is an infinite or finite sequence \(N_0,N_1,N_2,\ldots\) that is connected using one-step beta reduction that starts from \(M\).

• \(M\) is weakly normalizing if there is an \(N\) in the beta normal form such that \(M\twoheadrightarrow_\beta N\). (One of the reduction path leads to an outcome.)
• \(M\) is strongly normalizing if there are no infinite reduction paths starting from \(M\). (Each reduction path leads to an outcome.)

Suppose that for a given lambda term \(M\), we have \(M\twoheadrightarrow_\beta N_i\) and \(M\twoheadrightarrow_\beta N_2\), then there is a lambda term \(N_3\) such that \(N_1\twoheadrightarrow_\beta N_3\) and \(N_2\twoheadrightarrow_\beta N_3\). This is the Church-Rosser Theorem.

1.6. Fixed Point Theorem

Every lambda term \(L\) has a fixed point, which can be constructed using a fixed point combinator. One instance is:

Then we have \(YL\) which is a fixed point of \(L\), since \(L(YL)=_\beta YL\), which can be shown as follows:

2. Simply Typed Lambda Calculus

In order to get a firmer hold on the desired behavior of functions, we introduce types. Functions are been classified to a certain collection, and certain restrictions on the input values are given.

The simple types introduced in this chapter prevents the anomalies but are also in several senses too restrictive. We will enlarge the expressivity of the system in subsequent chapters.

2.1. Simple Types

We first define an infinite set of type variables \(\mathbb{V}=\{\alpha,\beta,\gamma,\ldots\}\) and then define the set of simple types \(\mathbb{T}\):

1. Type variable: If \(\alpha\in\mathbb{V}\), then \(\alpha\in\mathbb{T}\).
2. Arrow type: If \(\sigma,\tau\in\mathbb{T}\), then \((\sigma\to\tau)\in\mathbb{T}\).

It can be expressed using abstract syntax as \(\mathbb{T}=\mathbb{V}\mid\mathbb{T}\to\mathbb{T}\).

The Greek letters \(\alpha,\beta,\gamma,\ldots\) and variants are used for type variables belonging to \(\mathbb{V}\). Arbitrary simple types are denoted using \(\sigma,\tau,\ldots\). Their outermost parentheses may be omitted and for arrow-types, they are right-associative.

Type variables are abstract representations of basic types, such as \(nat\) for natural numbers or \(list\) for lists. Arrow types represent function types, such as \(nat\to real\) which abstracts a function which input is a natural number and the returned result is a real number.

We also have statements which allow us to express something like term \(M\) has type \(\sigma\) in the form \(M:\sigma\). We assume we have infinitude of variables available for each type \(\sigma\), thus we assume that each variable \(x\) has a unique type: if \(x:\sigma\) and \(x:\tau\), then \(\sigma\equiv\tau\).

By adding typing to the basic construction principles of lambda calculus, we have:

1. Application: If \(M:\sigma\to\tau\) and \(N:\sigma\), then \(MN:\tau\).
2. Abstraction: If \(x:\sigma\) and \(M:\tau\), then \(\lambda x.M:\sigma\to\tau\).

There are two side conditions which have to be satisfied in the typing of an application \(MN\): the left-hand side \(M\) of the application must have a function type \(\sigma\to\tau\) while the right-hand side \(N\) of the application must match with the input type \(\sigma\); the output type will then be \(\tau\). For abstraction \(\lambda x.M\), we just need the types of \(x\) and \(M\).

A term \(M\) is called typable if there is a type \(\sigma\) such that \(M:\sigma\).

2.2. Church and Curry Typing

To type a lambda term, we should first type its variables. We can give types to variables in two ways:

1. Typing à la Church: also called explicit typing, that we prescribe a (unique) type for each variable upon its introduction.
2. Typing à la Curry: also called implicit typing, which type is left open to some extent. We find typable terms by a search process, which may involve guesses for the types of the variables.

We denote the types of bound variables immediately after their introduction following a \(\lambda\) while the types of free variables are given in a so-called context (basis):

2.3. Derivation Rules for Church’s \(\lambda_\to\)

The definition of lambda terms have to be modified to incorporate type information. This new set of pre-typed \(\Lambda_\mathbb{T}\) is defined by \(\Lambda_\mathbb{T}=V\mid(\Lambda_\mathbb{T}\Lambda_\mathbb{T})\mid(\lambda V:\mathbb{T}.\Lambda_\mathbb{T})\).

A judgment has the form \(\Gamma\vdash M:\sigma\), with \(\Gamma\) a context and \(M:\sigma\) a statement.

1. Statement: \(M:\sigma\), where \(M\in\Lambda_\mathbb{T}\) and \(\sigma\in\mathbb{T}\).
2. Declaration: a statement with a variable as subject.
3. Context: a list of declarations with different subjects.

Below we give three derivation rules to form a so-called derivation system for Church’s \(\lambda_\to\) in the premiss-conclusion format.

A pre-typed term \(\lambda_\to\) is called legal if there exist context \(\Gamma\) and type \(\rho\) such that \(\Gamma\vdash M:\rho\).

2.4. Well-Typedness in \(\lambda_\to\)

This is one of the three problems connected with judgments in type theory: to find an appropriate context and type if the term is indeed legal.

For example, we want to show \(M\equiv\lambda y:\alpha\to\beta.\lambda z:\alpha.yz\) is valid. Hence, our task is to find a type \(\rho\) such that \(\Gamma\vdash M:\rho\). First we determine the context \(\Gamma\) which \(\Gamma\equiv\emptyset\) suffices since there are no free variables in \(M\). Then we need to find \(\rho\).

Thus we can conclude that \(\lambda y.\alpha\to\beta.\lambda z:\alpha.yz\) is valid since we find \(\rho\) which is \((\alpha\to\beta)\to(\alpha\to\beta)\).

2.5. Type Checking in \(\lambda_\to\)

The name type checking is straightforward, it means to check the validity of a full judgment.

As an example, we can construct a derivation for \(x:\alpha\to\alpha,y:(\alpha\to\alpha)\to\beta \vdash(\lambda z:\beta.\lambda u:\gamma.z)(yz):\gamma\to\beta\).

Hence we have succeeded in giving a proper deviation of the judgment.

2.6. Term Finding in \(\lambda_\to\)

This section presents the third of the general problem in type theory, namely to find an appropriate term of a certain type, in a certain context. A term which belongs to a certain type is called an inhabitant of that type.

To find an inhabitant of a certain type, we can think of the type as proposition, while each inhabitant codes a proof of this proposition.

For instance, to find the term of \(A\to B\to A\), we can follow:

1. Assume that \(x\) is a proof of proposition \(A\).
2. Also assume that \(y\) is a proof of proposition \(B\).
3. Then \(x\) is still a proof of \(A\).
4. So the function mapping \(y\) to \(x\) sends a proof of \(B\) to a proof of \(A\), i.e., \(\lambda y:B.x\) proves the implication \(B\to A\).
5. Consequently, \(\lambda z:A.\lambda y:B.x\) proves \(A\to B\to A\).

The above process is generally called the PAT-interpretation, where PAT means both propositions-as-types and proofs-as-terms.

2.7. General Properties of \(\lambda_\to\)

We give a number of definitions about context below:

1. If \(\Gamma\equiv x_1:\sigma_1,\ldots,x_n:\sigma_n\), then the domain of \(\Gamma\) or \(\mathcal D(\Gamma)\) is the list \((x_1,\ldots,x_n)\).
2. Context \(\Gamma'\) is a subcontext of context \(\Gamma\), or \(\Gamma'\subseteq\Gamma\), if all declarations occurring in \(\Gamma'\) also occur in \(\Gamma\), in the same order.
3. Context \(\Gamma'\) is a permutation of context \(\Gamma\), if all declarations in \(\Gamma'\) also occur in \(\Gamma\), and vice versa.
4. If \(\Gamma\) is a context and \(\Phi\) is a set of variables, then the projection of \(\Gamma\) on \(\Phi\), or \(\Gamma\upharpoonright\Phi\), is the subcontext \(\Gamma'\) of \(\Gamma\) with \(\mathcal D(\Gamma')=\mathcal D(\Gamma)\cap\Phi\).

An important property concerning the free variables occurring in a judgment is that if \(\Gamma\vdash L:\sigma\), then \(\mathcal F(L)\subseteq\mathcal D(\Gamma)\). This can be proved by induction on the deviation of the judgment \(\mathcal J\equiv\Gamma\vdash L:\sigma\).

We continue with three other properties which are trivial and can also be proved by induction.

1. Thinning: Let \(\Gamma'\) and \(\Gamma''\) be contexts such that \(\Gamma'\subseteq\Gamma''\). If \(\Gamma'\vdash M:\sigma\), then also \(\Gamma''\vdash M:\sigma\).
2. Condensing: If \(\Gamma\vdash M:\sigma\), then also \(\Gamma\upharpoonright\mathcal F(M)\vdash M:\sigma\).
3. Permutation: If \(\Gamma\vdash M:\sigma\), and \(\Gamma'\) is a permutation of \(\Gamma\), then \(\Gamma'\) is also a context and moreover, \(\Gamma'\vdash M:\sigma\).

The Generation Lemma, which says precisely how a certain judgment can be generated, is shown below:

1. If \(\Gamma\vdash x:\sigma\), then \(x:\sigma\in\Gamma\).
2. If \(\Gamma\vdash MN:\tau\), then there is a type \(\sigma\) such that \(\Gamma\vdash M:\sigma\to\tau\) and \(\Gamma\vdash N:\sigma\).
3. If \(\Gamma\vdash\lambda x:\sigma.M:\rho\), then there is \(\tau\) such that \(\Gamma,x:\sigma\vdash M:\tau\) and \(\rho\equiv\sigma\to\tau\).

It’s obvious that, in order to build a legal term, its subterms should be legal too. This is the Subterm Lemma.

Another important property which applies for Church’s \(\lambda_\to\) is that, a term may have at most one type. This ensures that the type, if exists, must be unique. Therefore we also have the uniqueness of types.

2.8. Reduction and \(\lambda_\to\)

In order to be able to treat substitution, an operation at the heart of beta reduction, in \(\lambda_\to\), we have to append type information. We then have the Substitution Lemma: assume \(\Gamma',x:\sigma,\Gamma''\vdash M:\tau\) and \(\Gamma'\vdash N:\sigma\); then \(\Gamma',\Gamma''\vdash M[x:=N]:\tau\). This means that if we substitute all occurrences of context variable by a term of the same type, the result type is unchanged which is intuitively understandable.

We also have to adjust the definition for beta reduction to the (pre-typed) terms of \(\Lambda_\mathbb{T}\):

1. Basis: \((\lambda x:\sigma.M)N\to_\beta M[x:=N]\).
2. Compatibility: If \(M\to_\beta N\), then \(ML\to_\beta NL\), \(LM\to_\beta NL\) and \(\lambda x:\tau.M\to_\beta \lambda x:\tau.N\).

The Church-Rosser Theorem is still valid as types clearly play no role in the reduction process.

The Subject Reduction states that beta reduction does not affect typability, and even does not change the term’s type: if \(\Gamma\vdash L:\rho\) and if \(L\twoheadrightarrow_\beta L'\), then \(\Gamma\vdash L':\rho\). Proof can be done by inducting the one basic and three compatibility cases of beta reduction.

Finally, one can prove that there are no infinite reduction sequences in \(\lambda_\to\), or every legal term is strongly normalization. This is the String Normalization Theorem or Termination Theorem.

3. Second Order Typed Lambda Calculus

In Church’s \(\lambda_\to\), we only encounter abstraction and application on the term level, which is first order, as abstraction and application are over terms. In the present chapter, second order operations, or terms depending on types, are introduced.

This is called the second order lambda calculus, written as \(\lambda2\) for short.

3.1. \(\Pi\) Types

To construct a function that can handle terms of different types, we can consider an arbitrary type, and use this type as another abstraction for our function \(\lambda\alpha:*.\lambda x:\alpha.x\).

This function receives a type variable \(\alpha\), while the \(*\) symbol denotes the type of all types. The function acts as a term depending on a type, thus is second ordered or polymorphic.

To type this polymorphic term, we introduce a new binder, the \(\Pi\) binder. We can then express the type of the polymorphic function created earlier as \(\Pi\alpha:*.\alpha\to\alpha\).

By an obvious extension of the alpha conversation, we obtain:

3.2. Second Order Abstraction and Application Rules

Since we allow second order abstraction, second order application and \(\Pi\) types, our derivation system for \(\lambda_\to\) has to be extended.

The second order application rule is intuitive, that two types of arbitrary type can be interchanged. This abstraction rule also corresponds to our expectations, as presented in the previous section where the \(\Pi\) types are introduced.

3.3. The System \(\lambda2\)

To describe the complete system, we have to first extend our definition of types. The abstract syntax for \(\lambda2\) types is \(\mathbb{T}2=\mathbb{V}\mid(\mathbb{T}2\to\mathbb{T}2)\mid(\Pi\mathbb{V}:*.\mathbb{T}2)\) while \(\mathbb{V}\) is the set of type variables.

Then we extend our set of pre-typed lambda terms so that second order abstraction and application are allowed:

Note that now we have two classes of variables: object variables \(V\) and type variables \(\mathbb{V}\). We also have first order application \((\Lambda_{\mathbb{T}2}\Lambda_{\mathbb{T}2})\) and second order application \((\Lambda_{\mathbb{T}2}\mathbb{T}2)\) as well as first order abstraction \((\lambda V:\mathbb{T}2.\Lambda_{\mathbb{T}2})\) from object variables and second order abstraction \((\lambda\mathbb{V}:*.\Lambda_{\mathbb{T}2})\).

The convention is similar to that in untyped and simply typed lambda calculus:

• Outer parentheses may be omitted.
• Application is left-associative.
• Application and \(\to\) takes precedence over both \(\lambda\) and \(\Pi\) abstraction.
• Successive \(\lambda\) or \(\Pi\) abstractions concerning the same types may be combined in a right-associative way.
• Arrow types are denoted in a right-associative way.

The notation of declaration should as well be extended to allow second order declarations:

1. Statement: Either of the form \(M:\sigma\), where \(M\in\Lambda_{\mathbb{T}2}\) and \(\sigma\in\mathbb{T}2\), or of the form \(\sigma:*\), where \(\sigma\in\mathbb{T}2\).
2. Declaration: A statement with a term variable or a type variable as subject.

The rule that all variables must be declared before they can be used motivates the following recursive definition of the \(\lambda2\) context, which the new definition of the domain of a context is combined:

1. \(\emptyset\) is a \(\lambda2\) context. Its domain is the empty list.
2. If \(\Gamma\) is a \(\lambda2\) context, \(\alpha\in\mathbb{V}\) and \(\alpha\notin\mathcal D(\Gamma)\), then \(\Gamma,\alpha:*\) is a \(\lambda2\) context. And \(\mathcal D(\Gamma,\alpha:*)=(\mathcal D(\Gamma),\alpha)\).
3. If \(\Gamma\) is a \(\lambda2\) context, if \(\rho\in\mathbb{T}2\) such that \(\alpha\in\mathcal D(\Gamma)\) for all free type variants \(\alpha\) occurring in \(\rho\) and if \(x\notin\mathcal D(\Gamma)\), then \(\Gamma,x:\rho\) is a \(\lambda2\) context. And \(\mathcal D(\Gamma,x:\rho)=(\mathcal D(\Gamma),x)\).

Conforming with the new notion of context, we adapt the variable rule and define the formation rule which defines a properly formed \(\lambda2\) type. We assume \(\Gamma\) is a \(\lambda2\) context.

Finally, we define the legality of \(\lambda2\): a term \(M\) in \(\Lambda_{\mathbb{T}2}\) is called legal if there exists a \(\lambda2\) context \(\Gamma\) and a type \(\rho\) in \(\mathbb{T}2\) such that \(\Gamma\vdash m:\rho\).

3.4. Properties of \(\lambda2\)

The definition of alpha conversion is adapted and extended accommodating \(\Pi\) types:

1. Renaming of term variable: \(\lambda x:\sigma.M=_\alpha\lambda y:\sigma.M^{x\to y}\) if \(y\notin \mathcal F(M)\) and \(y\) does not occur as a binding variable in \(M\).
2. Renaming of type variable: \(\lambda\alpha:*.M=_\alpha\lambda\beta:*.M[\alpha:=\beta]\) if \(\beta\) does not occur in \(M\) or \(\Pi\alpha:*.M=_\alpha\Pi\beta:*.M[\alpha:=\beta]\) if \(\beta\) does not occur in \(M\).

We also extend the beta reduction in an obvious way matching the extensions of alpha conversation:

1. Basis for first order: \((\lambda m:\sigma.M)N\to_\beta M[x:=N]\).
2. Basis for second order: \((\lambda\alpha:*.M)T\to_\beta M[\alpha:=T]\).

Most properties for \(\lambda_\to\) defined in the previous chapter still applies, except the Permutation Lemma, which holds only if the permuted context is a \(\lambda2\) context.

4. Types Dependent on Types

In this chapter, we discuss the way to construct generalized types, by abstracting types. This results in the system \(\lambda\underline{\omega\!}\,\).

4.1. Type Constructors

We can handle the abstraction of types of terms similar to the way we handle arbitrary types: types like \(\beta\to\beta\), \(\gamma\to\gamma\), \((\beta\to\gamma)\to(\beta\to\gamma)\) can be generalized using a function \(\lambda\alpha:*.\alpha\to\alpha\) with type as value. This is a so-called type constructor, with type \(*\to*\) itself. Proper constructor are the type constructors which are not types.

We name the type of the type constructors consisting of \(*\) alone and of \(*\) symbols with arrows in between kind. They belong to set \(\mathbb{K}\) with abstract syntax \(\mathbb{K}=*\mid(\mathbb{K}\to\mathbb{K})\). Outermost parentheses may be omitted, and the kinds are right-associative. For the type of all kinds, a new symbol \(\square\) is introduced.

We use the word sort or symbol \(s\) for either \(*\) or \(\square\); by definition, the set of sorts is \(\{*,\square\}\).

So now there are four levels in our syntax:

1. The terms.
2. The constructors (types plus the proper constructors).
3. The kinds.
4. Solely of type of kinds.

4.2. Sort and Variable in \(\lambda\underline{\omega\!}\,\)

First, we formalize the fact that the super-type \(*\) is of type \(\square\) using the sort rule.

The variable rule is used to establish that all declarations occurring in a context is derivable in that context. In \(\lambda_\to\), the set of permissible types was given beforehand. In \(\lambda2\), we restrict the types of the variables to the recursively defined \(\lambda2\) context. For the more complicated \(\lambda\underline{\omega\!}\,\), we combine it with the construction of the context proper.

The new approach is that we only extend a context with a declaration \(x:A\) only when the type \(A\) is permissible, which is either a type or a kind.

This rule plays a double role due to the two possibilities of \(s\).

4.3. Weakening Rule in \(\lambda\underline{\omega\!}\,\)

When defining the variable rule, the type of the derivable term is restricted to level 2 and 3, since one prerequisite is that the type of the derivable term must be of type sort, which is level 4. The solution to this limitation is the addition of the weakening rule, which states the fact that the context of a judgment can be weakened by adding new declarations provided that the types of the new declarations are well-formed.

Assuming that we have derived the judgment \(\Gamma\vdash A:B\), then we may weaken the context by adding an arbitrary declaration which type is well-formed at the end. In fact, the Thinning Lemma still applies for \(\lambda\underline{\omega\!}\,\), which means insertion of new declaration is allowed at an arbitrary place, however the weakening rule is easy to express and turns out to be sufficient.

Now that we are able to derive for example \(\alpha:*,\beta:*\vdash\alpha:*\) by proof tree.

4.4. Formation Rule in \(\lambda\underline{\omega\!}\,\)

For the construction of typing statements in a context, we have the formation rule. In \(\lambda2\), the rule was based on a set \(\mathbb{T}2\) of \(\lambda2\) types. While types are more complex in \(\lambda\underline{\omega\!}\,\), the possibility of double roles makes things become easier.

4.5. Application and Abstraction Rules in \(\lambda\underline{\omega\!}\,\)

The application and abstraction rules differ from the ones in the previous section because of the extended type in \(\lambda\underline{\omega\!}\,\) and the lack of \(\Pi\) types. Thus the type identifier is changed and a second premiss which the term must be well-formed is added.

The two rules both have a double role again, since \(s\in\{*,\square\}\).

4.6. Conversion Rule

We have applied beta reduction and conversation only on terms before. While the type becomes more complex in \(\lambda\underline{\omega\!}\,\), one will want an other derivation rule which acts on the types.

This rule is called the conversion rule, similar to the subject reduction but is intended for types.

4.7. Properties of \(\lambda\underline{\omega\!}\,\)

The system \(\lambda\underline{\omega\!}\,\) satisfies the majority of the nice properties from the previous systems, while only the conversion rule requires a slight modification of the Uniqueness of Type Lemma, that types need no longer be literally unique, but they are unique up to conversation.

5. Type Dependent on Terms

In the previous three chapters, we have met \(\lambda_\to\), the basic system which terms depending on terms; \(\lambda2\), terms depending on types; and \(\lambda\underline{\omega\!}\,\), types depending on types. In this chapter, we will treat the last extension \(\lambda P\) which types are dependent on terms.

A type depending on a term has general format \(\lambda x:A.M\), where \(M\) is a type, \(x\) is a term variable, and \(A\) is a type. This abstraction then depends on \(x\), and is often called type-valued function or simply type constructor.

For instance, let \(V_n=\{\langle v_1,\ldots,v_n\rangle\mid v_i\in\mathbb{N}\}\), a set of all natural number vectors of length \(n\), then \(\lambda n:nat.V_n\) maps \(n\) to the set of all vectors of length \(n\). It has type \(nat\to*\).

Furthermore, we can turn this type-valued function into a predicate. Take \(P_n\) to be the proposition \(n\) is a prime number, then \(\lambda n:nat.P_n\) is the logical predicate to be a prime. This is the PAT-interpretation introduced with \(\lambda_\to\), the first step to a fruitful treatment of proof in formal logic and mathematics.

5.1. Derivation Rules of \(\lambda P\)

The derivation rules of \(\lambda P\) has a great resemblance to the rules of \(\lambda\underline{\omega\!}\,\), so we present them directly.

The main differences with respect to \(\lambda\underline{\omega\!}\,\) are:

1. The appearance of \(\Pi\) types instead of the \(\to\) types, which means \(B\) is generalized so that \(x\) can appear as a free variable, thus a dependent product, which the output type depends on the input value.
2. The input type can not be dependent on types anymore, so that it can only have type \(*\).

The formation rule is also called the product rule, since it enables the construction and typing of a \(\Pi\) type. Martin-Löf calls a \(\Pi\) type the cartesian product of a family of types. So \(\Pi\) types can both be seen as a generalization of the cartesian product (consider \(A=\{a_1,a_2\}\), then \(\Pi x:A.B\) is the same as \(B[x:=a_1]\times B[x:=a_2]\)) and as a generalization of the function space (if \(x\notin\mathcal F(B)\), then \(\Pi x:A.B\) is just \(A\to B\)).

5.2. Minimal Predicate Logic

We can code minimal predicate logic which only has implication and universal qualification as logic operations with basic entities propositions, sets and predicates over sets in \(\lambda P\).

We first investigate the coding of the basic entities of minimal predicate logic and apply the full PAT interpretation in the appropriate cases.

1. We code a set \(S\) as a type, so \(S:*\). Then, the elements of the sets are terms.
2. Propositions are coded as types. Let \(A\) be a proposition, then \(A:*\). A term \(p\) inhabiting such \(A\) codes a proof of \(A\).
3. A predicate \(P\) is a function from a set \(S\) to set of all propositions. Therefore \(P:S\to*\). If this function with a term applied is inhabited, then the predicate hold, and vice versa.
4. The implication \(A\Rightarrow B\) is coded as the function type \(A\to B\) in type theory. Note that propositions are independent from each other, so there is no need to consider \(\Pi\) types here.
5. We code the universal qualification \(\forall_{x\in S}(P(x))\) as the \(\Pi\) type \(\Pi x:S.Px\). And it turns out that the elimination and introduction rules are a special case of the abstraction and application rules of \(\lambda P\).

An example of minimal predication logic is given. Let \(S\) be a set and \(Q\) a binary predicate over \(S\), what we want to prove is \(\forall_{x\in S}\forall_{y\in S}(Q(x,y))\Rightarrow\forall_{u\in S}(Q(u,u))\). We define a local environment \(\Delta=\{S:*,Q:S\to S\to*\}\) for this.

This is identical to a term finding process, and the proposition is proved since we succeeded in finding an inhabitant for the type representing the proposition.