simply typed λ-calculus

logical verification week 2 2004 09 15

newsflash

prime number theorem formalized

write π(n) for the number of primes below n, then

lim_{n→∞} \frac{π(n)}{n/ ln(n)} = 1

http://www.andrew.cmu.edu/user/avigad/isabelle/

• Jeremy Avigad

• Kevin Donelly

• David Gray

overview

last week

logic type theory
proofs  λ-terms

on paper

in Coq

why typed λ-calculus?

C program

#include <math.h>
double findzero(\underline{double (*f)(double)}, double z) \{
  double x, y;
  while (x = z, y = (*f)(x), z = x - y/((*f)(x + y) - y)*y,
    fabs(z/x - 1) >= 1e-15) ;
  return z;
}
double sqrminus2(double x) { return x*x - 2; }
main() {
  printf("%.15g\n", findzero(&sqrminus2, 1));
}

programming styles

• imperative programming C

• object-oriented programming C++ java

• logic programming prolog

• functional programming lisp ML ‘typed’

haskell  ‘lazy’  calculations with infinite data structures

functional programming

functional values become first class objects no need to name functions anymore

                findzero( &sqrminus2 , . . . )

↓

               findzero( λx . x*x - 2 , . . . )

functions also can return functional values ‘higher order’ functions

currying

f : A × B → C

partial evaluation

f(a, ·) : B → C

curried version of the function:

f : A → (B → C)
f : A → B → C

the type of findzero

(double → double) × double → double

curried:

(double → double) → double → double

↑ atomic type

↑

function type

simply typed λ-calculus

types

• atomic types A B C …

• function types A → B

terms

• variables x y z …

• lambda abstraction λx : A. t the function that maps the variable x of type A to t

• function application t u the result of applying the function t to the argument u

parentheses

• function types associate to the right

• application associates to the left these conventions are natural for curried functions:

f : A → (B → C) (f a) b

↓

f : A → B → C f a b

simplest example

identity function on A

term λx : A. x
type A → A

example in the real numbers

term λx : ℝ. x^{2} − 2
type ℝ → ℝ

(λx : ℝ. x^{2} − 2) 1 = 1^{2} − 2 = −1
(λx : ℝ. x^{2} − 2) 2 = 2^{2} − 2 = 2
↑
β-step

bigger example

term λx : (A → B) → C → D. λy : C. λz : B. x (λw : A. z) y
type ((A → B) → (C → D)) → C → B → D

type derivations

judgments

\underbrace{x_{1} : A_{1}, x_{2} : A_{2}, …, x_{n} : A_{n}}_{Γ context list of variable declarations} ⊢ t : A

the three typing rules

variable rule

Γ, x : A, Γ′ ⊢ x : A

x does not occur in Γ′

abstraction rule

\frac{Γ, x : A ⊢ t : B}{Γ ⊢ (λx : A. t) : (A → B)}

application rule

\frac{Γ ⊢ t : A → B Γ ⊢ u : A}{Γ ⊢ t u : B}

type derivation for the example

⊢ λx : (A → B) → C → D. λy : C. λz : B. x (λw : A. z) y : ((A → B) → (C → D)) → C → B → D

the Curry-Howard-de Bruijn isomorphism

recap minimal logic

• formulas propositional variables implication A → B

• rules implication introduction implication elimination

recap example natural deduction

((A → B) → (C → D)) → C → B → D

implication introduction & the abstraction rule

\frac{[A^{x}] ; ⋮ ; B}{A → B} I[x]→  \frac{Γ, x : A ⊢ t : B}{Γ ⊢ (λx : A. t) : (A → B)}

implication elimination & the application rule

\frac{⋮ ; A → B  ⋮ ; A}{B} E→  \frac{Γ ⊢ t : A → B  Γ ⊢ u : A}{Γ ⊢ t u : B}

isomorphism

propositional variable ∼ type variable
the connective → ∼ the type constructor →
formula ∼ type
assumption ∼ variable
implication introduction ∼ lambda abstraction
implication elimination ∼ function application
proof ∼ term
provability ∼ ‘inhabitation’
proof checking ∼ type checking

BHK-interpretation

Brouwer, Heyting, Kolmogorov intuitionistic logic

proof of A → B ∼ function that maps proofs of A to proofs B
proof of ⊥  does not exist
proof of A ∧ B ∼ pair of a proof of A and a proof of B
proof of A ∨ B ∼ either a proof of A or a proof of B

propositions as types

λx : A. x : A → A

the function type A → A represents a proposition the term λx : A. x represents a proof of that proposition

λ-terms are proof objects

Coq

term syntax

• x
• fun x : A => t
• t u

commands

• Check

prints a term with its type

• Print

print the term for a symbol with its type

example

                  fun x : A => x : A -> A

Coq as proof checker ‘->’ represents implication

Coq as functional programming language ‘->’ represents function type

proof objects

Lemma I : A -> A.
...
Qed.
Print I.

example

((A -> B) -> (C -> D)) -> C -> B -> D

summary

this week

logic type theory
proofs  terms

on paper

in Coq