the pure type system called λP

logical verification week 9 2004 11 10

recap

where we are in the course

propositional logic ↔ simple type theory

λ→

predicate logic ↔ type theory with dependent types

λP

2nd order propositional logic ↔ polymorphic type theory

λ2

the main difference between λ→ and λP

A → B

‘type of functions from A to B’

Πx : A. B

‘type of functions from A to B’ dependent product dependent function type

type of function value B now can depend on function argument x arrow type becomes a special case

λP

syntax

• two sorts ∗, □

• variables x, y, z, …

• function application MN

• function abstraction λx : A. M

• dependent product Πx : A. M

Coq syntax versus λP syntax

∗ ↔ Set
∗ ↔ Prop
□ ↔ Type

x ↔ x
M N ↔ M N

λx : A. M ↔ fun x:A => M
Πx : A. M ↔ forall x:A, M

λP does not make the distinction between Set and Prop

pseudo-terms versus terms

any expression according to the λP grammar is called a pseudo-term

(□ ∗)

λn : nat. λx : n. x
(λx : nat. x x) (λx : nat. x x)

if also all types are okay, then the expression is called a term

□

λn : nat. nat
(λf : (Πm : nat. nat). λx : nat. f x) (λn : nat. n)
(λf : nat → nat. λx : nat. f x) (λn : nat. n)

contexts and judgments

a judgment has the form Γ ⊢ M : N with Γ a context and M and N terms

a context Γ is a list of type declarations

a type declaration has the form x : M with x a variable name and M a term

A : ∗, P : (Πx : A. ∗), a : A ⊢ (Πw : P a. ∗) : □
A : ∗, P : A → ∗, a : A ⊢ (P a) → ∗ : □

the seven rules of λP

• one rule for each kind of term – axiom rule (for the sorts)

– variable rule

– product rule

– abstraction rule

– application rule

• two more rules – weakening rule (for the contexts)

– conversion rule

rule 1: axiom

\overline{⊢ ∗ : □}

gives the type of the sort ∗ the only rule with no premises!

rules 2 and 3: variable and weakening

in these rules s is either ∗ or □

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

gives the type of the variable x

if the variable is not the last in the context we need the weakening rule

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

rule 4: product

\frac{Γ ⊢ A : ∗ Γ ⊢ B : s}{Γ ⊢ A → B : s}

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

gives the type of a dependent product

rule 5: abstraction

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

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

gives the type of a function abstraction

rule 6: application

\frac{Γ ⊢ M : A → B Γ ⊢ N : A}{Γ ⊢ MN : B}

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

gives the type of a function application

rule 7: conversion

\frac{Γ ⊢ A : B  Γ ⊢ B′ : s}{Γ ⊢ A : B′}  with B =_{β} B′

is needed to make everything work

reduction and convertibility

• step

… ((λx : A. M)N) … →_{β} … (M[x := N]) …

• reduction → →_{β} zero or more steps

• convertibility =_{β} smallest equivalence relation

cheat sheet

axiom, application, abstraction, product

\overline{⊢ ∗ : □}

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

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

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

weakening, variable, conversion

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

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

\frac{Γ ⊢ A : B  Γ ⊢ B′ : s}{Γ ⊢ A : B′}  with B =_{β} B′

examples

example 1

X : ∗, x : X ⊢ x : X

example 2_{X : ∗ ⊢ (X → X) : ∗}

18

example 3_{A : ∗, P : A → ∗, a : A ⊢ (P a) → ∗ : □}

19

Curry-Howard-de Bruijn for minimal predicate logic

introduction rules versus abstraction rule

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

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

elimination rules versus application rule

\frac{⋮ ; A → B  ⋮ ; A}{B} E→  \frac{⋮ ; ∀x. B}{B[x := N]} E∀

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

examples

example 4

∀x. (P (x) → (∀y. P (y) → A) → A)

example 5_{(∀x. P (x) → Q(x)) → (∀x. P (x)) → ∀y. Q(y)}

23

logical framework

from automath to twelf

• automath 1968, de Bruijn start of proof checking of mathematics

• LF 1987, Harper & Honsell & Plotkin framework for defining logics the type of theory of LF is precisely λP

• twelf 1998, Pfenning & Schürmann current implementation of LF

logics in a logical framework

each logic has a λP context that contains syntax and rules of the logic

example: minimal propositional logic as a λP context

P : ∗ ,
⇒ : P → P → P ,
T : P → ∗ ,
I : Πp : P. Πq : P. (T p → T q) → T (p ⇒ q) ,
E : Πp : P. Πq : P. T (p ⇒ q) → T p → T q
⊢
…

logosphere

Schürmann, Pfenning, Kohlhase, Shankar, Owre making proof assistants talk to each other

approach:

• define contexts for the logics of the various proof assistants in twelf • import the libraries of the proof assistants in twelf

see:

                http://www.logosphere.org/

the Barendregt cube

pure type systems

Berardi & Terlouw:

framework for defining and studying typed λ-calculi PTS = pure type system

the PTS rules are exactly^{∗} the λP rules as presented here

(^{∗} except for one symbol, in the product rule)

variations on the product rule

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

λP s_{1} = ∗ , s_{2} ∈ {∗, □}

(s_{1}, s_{2}) ∈ {(∗, ∗), (∗, □)}

λ→ (s_{1}, s_{2}) ∈ {(∗, ∗)}
λC (s_{1}, s_{2}) ∈ {(∗, ∗), (∗, □), (□, ∗), (□, □)}

the Barendregt cube

[figure: λω; λC; λ2; (□, ∗); λP 2; λ\underline{ω}; λP \underline{ω}; λ→; (∗, □); (□, □); λP]

two schools of type theory

automath Netherlands

[figure]

[figure]

[figure]

[figure]

impredicative type theory

calculus of constructions France predicative type theory Martin-Löf’s type theory Sweden