Formalizing Bishop Style

Constructive Mathematics with Martin-Löf’s Type Theory

Frank Rosemeier FernUniversität Hagen D-58084 Hagen

e-mail: frank.rosemeier@fernuni-hagen.de

Motivation

Theory  | Implementation

( \begin{matrix}Bishop Style \\ Constr. Math. \end{matrix} ⟶ ? )

↓

\begin{matrix}Martin-Löf’s \\ Type Theory \end{matrix}  \} \begin{matrix}Alf \\ Alfa/Agda \end{matrix}

↓

\begin{matrix}Barendregt’s \\ λ-cube \end{matrix}  \} \begin{matrix}Coq \\ Lego \end{matrix}

↓

(Pure Type Systems ⟶ Yarrow )

Barendregt’s λ-cube

[figure: λω; λC; λ2; λP2; λ\underline{ω}; λP\underline{ω}; λ→; λP]

[Barendregt 1992]

λ→ simply typed λ-calculus [Church 1932–41]
λ2 second order λ-calculus [Girard 1972, Reynolds 1974]
λω higher order λ-calculus [Girard 1972]
λC calculus of constructions [Coquand, Huet 1985–88]

λ-cube terms

Term  Meaning/Interpretation
x_{1}, x_{2}, … variables
(fa)  function application
(λx:A.b)  function abstraction
(Πx:A.B) (dependent) function type
∗  sort of all types
□  sort of all kinds
(fa)  f(a)
(λx:A.b)  function x ↦ b for all x in A
(Πx:A.B) { f |f(x) in B for all x in A }
∗  { α |α is a type }
□  {∗, ∗→∗, …}

β-conversion

Notation M[x := N] denotes substitution of N for all free occurrences of x in M.

Definition Let β-conversion =_{β} be the smallest equivalence relation on λ-cube terms such that

((λx:M.N)L) =_{β} M[x := L],

M =_{β} M′ ⟹ (LM) =_{β} (LM′),
M =_{β} M′ ⟹ (MN) =_{β} (M′N),
M =_{β} M′ ⟹ (λx:L.M) =_{β} (λx:L.M′),
M =_{β} M′ ⟹ (λx:M.N) =_{β} (λx:M′.N),
M =_{β} M′ ⟹ (Πx:L.M) =_{β} (Πx:L.M′),
M =_{β} M′ ⟹ (Πx:M.N) =_{β} (Πx:M′.N).

General λ-cube rules

Γ context x_{1}:A_{1}, …, x_{n}:A_{n} (n ≧ 0)

(Start)  \frac{Γ ⊢ A: s}{Γ, x:A ⊢ x: A}  (s ∈ \{∗, □\})

(Weaken) \frac{Γ ⊢ A: s Γ ⊢ b: B}{Γ, x:A ⊢ b: B}

(Conv) \frac{Γ ⊢ a: A Γ ⊢ A′: s}{Γ ⊢ a: A′} if A =_{β} A′

(Π-intro) \frac{Γ ⊢ (Πx:A.B) : s Γ, x:A ⊢ b: B}{Γ ⊢ (λx:A.b) : (Πx:A.B)}

(Π-elim) \frac{Γ ⊢ f : (Πx:A.B) Γ ⊢ a: A}{Γ ⊢ (fa) : B[x := a]}

(x fresh for Γ and for A)

Axiom (Ax) ⊢ ∗: □ Specific rules (s_{1}, s_{2} ∈ {∗, □})

(Π-form) \frac{Γ ⊢ A: s_{1} Γ, x:A ⊢ B : s_{2}}{Γ ⊢ (Πx:A.B) : s_{2}}

(x fresh for Γ and for A) λ-cube calculi

Calculus Specific (s_{1}, s_{2})-rules available
λ→ (∗,∗)
λP (∗,∗) (∗,□)
λ2 (∗,∗)  (□,∗)
λ\underline{ω} (∗,∗)  (□,□)
λP2 (∗,∗) (∗,□) (□,∗)
λP\underline{ω} (∗,∗) (∗,□)  (□,□)
λω (∗,∗)  (□,∗) (□,□)
λC = λPω (∗,∗) (∗,□) (□,∗) (□,□)

Notation (A→B) ≡ (Πx:A.B) with x fresh for A, B

Derived rules (s, s_{1}, s_{2} ∈ {∗, □})

(→-intro) \frac{Γ ⊢ (A→B) : s Γ, x:A ⊢ b: B}{Γ ⊢ (λx:A.b) : (A→B)}

(x fresh for Γ and A)

(→-elim) \frac{Γ ⊢ f : (A→B) Γ ⊢ a: A}{Γ ⊢ (fa) : B}
(→-form) \frac{Γ ⊢ A: s_{1} Γ ⊢ B : s_{2}}{Γ ⊢ (A→B) : s_{2}}

Rule  Dependency
(∗, ∗)  objects depending on objects
(∗, □) types depending on objects
(□, ∗) objects depending on types
(□, □) types depending on types

Examples

In λ→: \begin{aligned}α:∗, β:∗ & ⊢ & (α→β) : ∗ \\ α:∗ & ⊢ & (λx:α.x) : (α→α) \end{aligned}

In λ2: \begin{matrix}⊢ & (Πα:∗.(α→α)) : ∗ \\ ⊢ & (λα:∗.(λx:α.x)) : (Πα:∗.(α→α)) \end{matrix}

In λ\underline{ω}: \begin{matrix}⊢ & (∗→∗) : □ \\ ⊢ & (λα:∗.(α→α)) : (∗→∗) \end{matrix}

In λP: \begin{aligned}α:∗ & ⊢ & (α→∗) : □ \\ α:∗, P:(α→∗), x:α & ⊢ & (P x) : ∗ \end{aligned}

Impredicativity

In λ2: ⊢ (Πα:∗.α) : ∗

Martin-Löf’s type theory

Judgements Representation
A set  A : Set
A = B  (SetEQ A B) true
a ∈ A  a : (El A)
a = b ∈ A  (ElEQ A a b) true

where

Set : ∗
SetEQ : Set→Set→∗
El : Set→∗
ElEQ : ΠA:Set.((El A)→(El A)→∗)

(A type α:∗ is called true if it is inhabited, i. e. if c: α for some c.)

Judgements as Types Interpretation