Introduction

These are study notes for my comprehensive. My reading list includes Girard's book: "proofs and types" (see link on right hand top inset for online version). Note that math notation based on Peter Jipsen's ASCIIMathML.js works in Netscape7.1/Mozilla/Firefox only. I still need to get it to work on other browsers. In the other browser(s), you should see mathematical formulas as $ delimited garbage $.

The simply-typed $\lambda$-calculus

The simply-typed $\lambda$-calculus is introduced on:

• page 34 of Selinger's notes (chapter 5)
• page 33 of Barendregt and Barendsen (chapter 5)

It is sometimes necessary to know the domain/codomain of a function ahead of time. Types are syntactic objects. They can be thought of as names for sets.

---

Introduction

There are only two rules for creating types from atomic types:

• $T_1,\cdots,T_n$ are Atomic Types.
• If $U$ and $V$ are types, then
  • $U\rarr V$ and
  • $U\xx V$
  are types.

Typing The Terms

• The variables $x_0^T,\cdots,x_n^T$ are terms of type $T$
  (also written $x_i : T$).
• $(:u,v:)$ is a term of type $U\xx V$ where $u:U$ and $v:V$ respectively.
• $\pi^1 t$ and $\pi^2 t$ are terms of type $U$ and $V$ respectively where $t:U\xx V$
• $\lambda x.v$ is a term of type $U\rarr V$ where $x : U$ is a variable and $v:V$ is a term
• $tu$ is a term of type $V$ where $t:U\rarr V$ and $u:U$

Denotational Semantics

• $[[x:U]] =$
• $[[(:u,v:) : U\xx V]] = $
• $[[\lambda x.v : U\rarr V]]=$
• $[[tu : V]] = $

Consistence

Decidability

Consistence and decibility are a consequence of the Church-Rosser Theorem and of the Normalisation Theorem (see below)

The Curry-Howard Isomorphism

The Curry-Howard isomorphism establishes a connection between propositional logic and the simply-typed $\lambda$-calculus. Using this connection, it is possible to view types as propositions and terms as proofs of propositions.

Important: Note here that (Girard's 1.2.2, page 5) the logic that is connected to the calculus is Brouwer's intuitionistic logic which corresponds to Heyting semantics (as opposed to classical logic). This is also described on page 37 of Selinger's notes.

The isomorphism is defined below (section 3.5 page 19 in Girard's):

• Hypothesis:

  ---

  $A$

  ---

• Introduction Rules:

  ---

  ---

  ${{:(.),(A):}{:text"   ":}{:(.),(B):}}/{A^^^B}$ $^^^I$

  corresponds to $(:u^A, v^B:)$, where $u$ corresponds to the deduction of $A$, while $v$ corresponds to the deduction of $B$.

  ---

  ${{:([A]),(.),(B):}}/{A\rArr B}$ $\rArr I$

  corresponds to $\lambda x^A.v^B$

  ---

  ---

• Elimination Rules:

  ---

  ${{:(.),(A^^^B):}}/{A}$$^^^E1$        ${{:(.),(A^^^B):}}/{{:(B),():}}$$^^^E2$ Correspond respectively to $\pi^1(:u^A, v^B:)$ and $\pi^2(:u^A, v^B:)$

  ---

  ${{:(.),(A):}{:text"   ":}{:(.),(A\rArr B):}}/{{:(B),():}}$ $\rArr E$

  Corresponds to the application $tu$ where $t:A\rarr B$ and $u:A$.

  ---

  ---

Conversion

(3.4. page 24 in Girards's Proof and Types)

Conversion

Below, term $t$ (the redex) converts to $t'$ (the contractum)

• $t=\pi^1(:u,v:)$ and $t'=u$
• $t=\pi^2(:u,v:)$ and $t'=v$
• $t=(\lambda x^U.v)u$ and $t'= v[u//x]$

Reduction

A term $u$ reduces to a term $v$ when there is a sequence of conversions from $u$ to $v$, that is a sequence $u = t_0, t_1,\cdots, t_{n-1}, t_n = v$ such that for $i = 0, 1,\cdots, n-1$, $t_{i+1}$ is obtained from $t_i$ by replacing a redex by its contractum. “u reduces to v” is written $u\lred v$

Normal forms

Definition: A term is normal if none of its subterms is of the form:

• $\pi^1 (:u,v:)$
• $\pi^2 (:u,v:)$
• $(\lambda x^U.v)u$

A normal form for a term $t$ is a term $u$ such that $t\lred u$ and $u$ is normal. Normal forms exist and are unique (Chapter 4 in Girards's Proof and Types).

The Church-Rosser property

if $t\lred u$ and $t\lred v$ then , there is a $w$ s.t. $u\lred w$ and $v\lred w$ (proof sketch around pg 21 of Selinger's notes)

As a corollary (pg 23 in Girard's notes), if $t\lred u$ and $t\lred v$ and both $u$ and $v$ are normal, then $u = v$. This is obvious since neither $u$ nor $v$ can be reduced any further.

The Weak Normalisation Theorem

Girard (section 4.2 pg 24)

All term have a normal form (which is unique). Note that this doesn't mean that all reduction procedures will reach the normal form.

The proof (for which I am responsible) looks vaguely like:

• Define the degree of a type as:
  • $\vartheta(T)=1$ if $T$ is atomic
  • $\vartheta(U\xx V) = \vartheta(U\rarr V)=max(\vartheta(U), \vartheta(V))+1$
• Define the degree of a redex as:
  • $\vartheta(\pi^1(:u^U,v^V:))= \vartheta(\pi^2(:u^U,v^V:)) = \vartheta(U\xx V)$
  • $\vartheta((\lambda x^U.v^V)u^U) = \vartheta(U\rarr V)$
• Define the degree of a term $d(t)$ as the sup of the degrees of the redexes it contains. A normal term has degree $0$

The Strong Normalisation Theorem

(Chapter 6 in Girard's)

Strong Normalisation

Definition: A term $t$ is strongly normalisable iff there is no infinite reduction sequence beginning with $t$.

Lemma:
$t$ is strongly normalisable iff there is a number $\nu(t)$ which bounds the length of any normalisation sequence that begins with $t$.

Theorem (The strong normalisation theorem):
All terms are strongly normalisable.

In order to prove the theorem, the notion of reducibility and neutralility are defined as follows:

Reducibility

Definition: A term $t:T$ is a reducible term of type $T$, written $t\in RED_T$ if, by induction on the type $T$:

• if $T$ is an atomic type , $t$ is reducible if it is strongly normalisable
• For $t$ of type $U\xx V$, $t$ is reducible if both $\pi^1t$ and $\pi^2t$ are reducible
• For $t$ of type $U\rarr V$, $t$ is reducible if, for all reducible $u$ of type $U$, $tu$ is reducible of type $V$

Neutrality

Definition: A term $t:T$ is neutral if it isn't in the form $(:u,v:)$ or $\lambda x.v$

Girard then proves the following 4 conditions:

• CR1:if $t\in RED_T$, then $t$ is strongly normalisable
• CR2:if $t\in RED_T$ and $t\lred t'$ then $t'\in RED_T$
• CR3:if $t$ is neutral, and $\forall t'$ s.t. $t\lred t'$, $t'\in RED_T$ then $t\in RED_T$
• CR4: (special case of CR3) if $t$ is neutral and normal, then $t\in RED_T$

The principal type property

Every typeable lambda term has a most general type.