λ2

logical verification week 12 2004 12 01

overview

the course

1st order propositional logic ↔ simple type theory

λ→

1st order predicate logic ↔ type theory with dependent types

λP

2nd order propositional logic ↔ polymorphic type theory

λ2

activities

logic  type theory
natural deduction  type derivations

on paper

↓  ↑

in Coq  →

minimal second order propositional logic

formulas

a b c … A → B ⊥ ⊤ ¬A A ∧ B A ∨ B ∀a. A ∃a. A

rules for →

→ introduction

\frac{[A^{x}] ; ⋮ ; B}{A → B} I[x]→

→ elimination

\frac{⋮ ; A → B  ⋮ ; A}{B} E→

rules for ∀

∀ introduction

\frac{⋮ ; B}{∀a. B} I∀

variable condition: a not a free variable in any open assumption

∀ elimination

\frac{⋮ ; ∀a. B}{B[a := A]} E∀

λ2

terms

∗, □

x, y, z, …

MN

λx : M. N

Πx : M. N

rules

\overline{⊢ ∗ : □} axiom

\frac{Γ ⊢ M : Πx : A. B  Γ ⊢ N : A}{Γ ⊢ MN : B[x := N]} application

\frac{Γ, x : A ⊢ M : B  Γ ⊢ Πx : A. B : s}{Γ ⊢ λx : A. M : Πx : A. B} abstraction

\frac{Γ ⊢ A : s  Γ, x : A ⊢ B : ∗}{Γ ⊢ Πx : A. B : ∗} product

rules (continued)

\frac{Γ ⊢ A : B  Γ ⊢ C : s}{Γ, x : C ⊢ A : B} weakening

\frac{Γ ⊢ A : s}{Γ, x : A ⊢ x : A} variable

\frac{Γ ⊢ A : B  Γ ⊢ B′ : s}{Γ ⊢ A : B′} conversion

with B =_{β} B′

the three product rules

all systems

\frac{Γ ⊢ A : ∗ Γ, x : A ⊢ B : ∗}{Γ ⊢ Πx : A. B : ∗}

only in λP

\frac{Γ ⊢ A : ∗ Γ, x : A ⊢ B : □}{Γ ⊢ Πx : A. B : □}

                          nat → ∗

only in λ2

\frac{Γ ⊢ A : □ Γ, x : A ⊢ B : ∗}{Γ ⊢ Πx : A. B : ∗}

Πa : ∗. a → a

Curry-Howard-de Bruijn

→ introduction versus abstraction rule

\frac{[A^{x}] ; ⋮ ; B}{A → B} I[x]→

\frac{Γ, x : A ⊢ M : B Γ ⊢ Πx : A. B : ∗}{Γ ⊢ λx : A. M : Πx : A. B}

→ elimination versus application rule

\frac{⋮ ; A → B  ⋮ ; A}{B} E→

\frac{Γ ⊢ M : Πx : A. B Γ ⊢ N : A}{Γ ⊢ MN : B[x := N]}

∀ introduction versus abstraction rule

\frac{⋮ ; B}{∀a. B} I∀

\frac{Γ, a : ∗ ⊢ M : B Γ ⊢ Πa : ∗. B : ∗}{Γ ⊢ λa : ∗. M : Πa : ∗. B}

∀ elimination versus application rule

\frac{⋮ ; ∀a. B}{B[a := A]} E∀

\frac{Γ ⊢ M : Πa : ∗. B Γ ⊢ A : ∗}{Γ ⊢ MA : B[a := A]}

example 1_{(∀b. b) → a}^{examples}

14

example 2

a → ∀b. (b → a)
a : ∗ ⊢ Πb : ∗. (b → a) : ∗

corresponds to

∏_{b∈Set} P(b) ∈ Set

week 10 → paradox

example 3_{a → ∀b. ((a → b) → b)}

16

detours and reduction

detour elimination for →

\frac{\frac{[A^{x}] ; ⋮ ; B}{A → B} I[x]→  ⋮ ; A}{B} E→ ⟶  ⋮ ; A ; ⋮ ; B

detour elimination for ∀

\frac{\frac{⋮ ; B}{∀a. B} I∀}{B[a := A]} E∀ ⟶  \begin{matrix}⋮ & ∗ \\ B[a := A] \end{matrix}

∗ replace a everywhere by A

typing the proof term of a detour

\frac{\frac{⋮ ; Γ, x : A ⊢ M : B  ⋮ ; Γ ⊢ Πx : A. B : s}{Γ ⊢ λx : A. M : Πx : A. B}  ⋮ ; Γ ⊢ N : A}{Γ ⊢ (λx : A. M)N : B[x := N]}

problems

type checking problem

input context Γ and terms M and N

Γ ⊢^{?} M : N

output true typing judgment is derivable false typing judgment is not derivable

generally decidable

type synthesis problem

input context Γ and term M

Γ ⊢ M : ?

output

true + term N

typing judgment is derivable with N substituted for ? false for no term substituted for ? is the judgment derivable

generally decidable

type inhabitation problem

input context Γ and term N

Γ ⊢ ? : N

output

true + term M

typing judgment is derivable with M substituted for ? false for no term substituted for ? is the judgment derivable

generally undecidable

proof checking problem

input formula A + possibly incorrect ‘proof’

correct?

output true the ‘proof’ is a correct proof of A false the ‘proof’ is not a correct proof of A

generally decidable corresponds to type checking problem

provability problem

input formula A

A?

output

true + proof of A

A is proved by the proof in the output false A is not provable

generally undecidable corresponds to type inhabitation problem

other notions

uniqueness of types

\begin{matrix}Γ ⊢ A : B \\ Γ ⊢ A : B′ \end{matrix} \} ⇒ B =_{β} B′

subject reduction

\begin{matrix}Γ ⊢ A : B \\ B → →_{β} B′ \end{matrix} \} ⇒ Γ ⊢ A : B′

Curry-Howard-de Bruijn isomorphism

isomorphism

between the set of proofs in a logic

and

the set of typed lambda terms in a type theory

formulas as types

proofs as terms Brouwer-Heyting-Kolmogorov interpretation

intuitive semantics of intuitionistic logic

explains

what it means to prove a formula

in terms of

what it means to prove its components

minimal versus intuitionistic versus classical logic

• minimal logic only → and ∀

• intuitionistic logic all connectives, just the intro and elim rules

• classical logic

… + one of the classical principles

excluded middle

A ∨ ¬A
∀a. a ∨ ¬a

Coq versus the other proof assistants

seven provers for mathematics

[figure: Mizar; most mathematical; LCF; HOL; Isabelle; most pure; Automath; Coq NuPRL; most logical; PVS; most popular; nqthm; ACL2; most computational]

foundations

• primitive recursive arithmetic ACL2

• type theory typed lambda calculus + inductive types, constructive Coq, NuPRL

• higher order logic typed lambda calculus + choice operator, classical HOL, Isabelle, PVS

• set theory Mizar

procedural versus declarative

0  ∞

• procedural

E E S E N E S S S W W W S E E E

HOL, PVS, Coq, NuPRL

• declarative

(0,0) (1,0) (2,0) (3,0) (3,1) (2,1) (1,1) (0,1) (0,2) (0,3) (0,4) (1,4) (1,3) (2,3) (2,4) (3,4) (4,4)

Mizar, Isabelle