Inductive Definitions

Christine Paulin-Mohring Université Paris Sud, Orsay, France

June 2003 Introduction : what is an inductive definition ?

Informal definition

An inductive definition introduces a new concept by :

• specifying a set of rules of constructions

• the assumption that we are considering the smallest notion closed under the rules of constructions

• different rules of constructions give different objects Inductive definitions are everywhere !

• programming – data structures : records, lists, trees …

– predicate definitions as clauses in logic programming • semantics of programming languages

– abstract syntax trees

– static, operational semantics as inference rules

• logic – representation of terms, formulas

– semantics, deduction relation

– constructive interpretation of connectors Two different views

Mathematics

• Make sure the notion is well-defined

• Implicit justification in main cases

• Extensional view of functions, equational reasoning Programming language or proof assistant

• Explicit construction

• Intensional view, computation

• Reasoning How to provide inductive definitions ?

in proof-assistant (HOL, type theory)

• Representation – primitive notion / encoded

• Which class of inductive definitions ? – strictly positive, positive, no restriction – polymorphic, dependent types

• Which rules ?

– primitive rules / derived rules What we expect from an inductive definition ?

• Termination of computations

• Consistency of the underlying logic

• Representation theorems

– Correspondance between terms in an inductive type and the

values to be represented

• Provability of properties of inductive definitions inside the proof assistant Contents of the course

1. Different sorts of inductive types

2. Inductive relations

3. Inductive definitions in different systems

4. Applications Different sorts of inductive types

• Examples of inductive types – Algebraic structures, ML concrete types and others.

• Non-recursive concrete types and logic

• Recursive definitions

C. Paulin-Oregon-June 2003 8

Algebraic Types

Introduce sorts, constants, operators with signature Natural numbers nat

constant 0,

operator S: (nat) → nat Finite sets color

constants red, black Lists of natural numbers list

constant nil,

   operator cons (nat,list) → list.

Expected properties : Free (initial) algebra

Injectivity Cons(n_{1}, l_{1}) = Cons(n_{2}, l_{2}) ⇒ n_{1} = n_{2} ∧ l_{1} = l_{2} Non-confusion Nil ≠ Cons(n, l) Finite terms any object of sort list is finitely built with

constant Nil and operator Cons. Induction

\frac{P (Nil) ∀n : nat.∀l : list.P (l) ⇒ P (Cons(a, l))}{∀l : list.P (l)}

Associated functions

Testing isNil ,isCons : list→bool
      (isNil Nil) ⟶ true (isNil Cons(n, l)) ⟶ false

Projections partial functions on non-nil lists

           hd : list^{∗} → int     tl : list^{∗} → list
           (hd Nil) ⟶ ⊥  (tl Nil) ⟶ ⊥

(hd Cons(n, l)) ⟶ n (tl Cons(n, l)) ⟶ l

C. Paulin-Oregon-June 2003 11

Inductive types in functional programming languages

OCAML notations

type list = Nil | Cons of int * list
type color = Red | Black

Parameterized types

type 'a option = None | Some of 'a
type 'a list = Nil | Cons of 'a * 'a list
type 'a tree = Leaf | Node of 'a * 'a tree * 'a tree

Expected Properties

Any value of type list evaluates to :

                     Nil or Cons(n, l)

with n of type int and l of type list Non confusion

                     Nil ≠ Cons(n, l)

Injectivity Cons(n_{1}, l_{1}) = Cons(n_{2}, l_{2}) ⇔ n_{1} = n_{2} and l_{1} = l_{2} Pattern-matching

Properties

match x with Nil → f | Cons(n,l) → g Equivalent to testing and projections functions : let isNil x = match x with Nil → true | Cons(n,l) → false let hd x = match x with Nil → failwith "hd" | Cons(n,l) → n let tl x = match x with Nil → failwith "tl" | Cons(n,l) → l Compiling pattern-matching match x with Nil → f | Cons(n,l) → g ≡ if isNil x then f else let n = hd x and l = tl x in g Assume equality is substitutive (Leibniz)

\frac{x = y  P (x)}{P (y)}  \frac{x = y}{f(x) = f(y)}

The pattern-matching construction (or test and projection functions) allows to derive :

  • Nil=Cons(a,l) ⇒ true=false

• Cons(a, l) = Cons(b, m) ⇔ a = b ∧ l = m Tree with finite (unbounded) branching

type tree = Node of tree list

• No explicit constant but still a basic element Node(Nil)

• Recursive argument as a parameter of another inductive type • Could also be seen as mutual inductive definitions :

  tree and tree list

Non-algebraic inductive types

Trees with infinite (denumerable) branching

type itree = Leaf | Node of (nat → itree)

               \overline{Leaf : itree}

                            f : nat → itree
                            Node(f) : itree

f:nat →itree is an infinite family of trees indexed by a natural number i. Node(f) is a tree with a root and a denumerable set of subtrees f_{0}, f_{1}, …, f_{n}, … represented by f. Remark : Node(f) = Node(g) ⇔ f = g ⇎ ∀n : nat.(f n) = (g n)

Non-positive types

type lambda = Lam of lambda → lambda     \frac{f : lambda → lambda}{Lam(f) : lambda}

λ-term representation

lambda  λ − term

Lam(fun x → x)  λx.x
Lam(fun x → (Lam(fun y → x))) λx.λy.x

C. Paulin-Oregon-June 2003 18

Lambda-term representation : application Application is defined by pattern-matching

app : lambda → lambda → lambda
let app (Lam f) x = f x

\frac{λf.λg.λx.(f (g x))}{Lam(fun f → Lam(fun g → Lam(fun x → (app f (app g x)))))}

Substitution for free

C. Paulin-Oregon-June 2003 19

Non Recursive types

Basic constructions

():unit

inl: α → sum_{α,β}, inr: β → sum_{α,β}

Derived notions

 bool   sum_{unit,unit}
 true   inl(())
 false  inr(())

C. Paulin-Oregon-June 2003 20

Product

Primitive notion in CAML Can also be seen as an inductive definition (curryfication of constructor)

pair: α → β → prod_{α,β}

Any non-recursive concrete data-type in ML can be encoded

                 using prod, sum and unit

Logic : introduction Proofs as Programs paradigm

Constructors

Introduction rules

     () : unit                       \overline{⊤}

inl : α → sum_{α,β}, inr : β → sum_{α,β} \frac{A}{A ∨ B} \frac{B}{A ∨ B}
pair : α → β → prod_{α,β}  \frac{A B}{A ∧ B}

Other logical constructions : ⊥ ∃ Elimination rules, reduction.

C. Paulin-Oregon-June 2003 22

Logic : elimination pattern-matching/projections

Elimination rules

\frac{x : prod_{α,β}}{fst(x) : α} \frac{x : prod_{α,β}}{snd(x) : β}  \frac{A ∧ B}{A} \frac{A ∧ B}{B}

\frac{x : sum_{α,β} a : α ⊢ f : γ b : β ⊢ g : γ}{match x with inl(a) → f|inr(b) → g : γ} \frac{A ∨ B A ⊢ C B ⊢ C}{C}

\frac{x : prod_{α,β} a : α, b : β ⊢ p : γ}{let (a, b) = x in p : γ} \frac{A ∧ B A, B ⊢ C}{C}

isleft : sum_{α,β} → bool
pleft : sum_{α,β} → A
pright : sum_{α,β} → B

A ∨ B ≡

                                       ∃b : bool,
                                          b = true ⇒ A
                                       ∧ b = false ⇒ B

C. Paulin-Oregon-June 2003 23

Logic : cut elimination Reductions correspond to cut-elimination :

\frac{\frac{A}{A ∨ B} A ⊢ C B ⊢ C}{C} ⟶ \frac{A ; // ; ⋮}{C}

match inl(a) with inl(x) → f | inr(y) → g ⟶

f[x := a]

C. Paulin-Oregon-June 2003 24

Absurd proposition

⊥ corresponds to an empty type

• No introduction rule

• Elimination provides an element in any type

\frac{⊥}{C}

Recursive types and logic

Specify type E with one constructor C: E → E There is no finite object in that type. f : E → ⊥ can be built for any type ⊥ (by recursion)

f (C x) = (f x)

Specify property A with one constructor neg: (A → ⊥) → A Then ⊥ is inhabited. Build a term p of type A → ⊥, (neg p) has type A, (p (neg p)) has type ⊥.

(p x) ≡ match x with neg f → (f x)

Dependent types

Types (or propositions) may depend on variables.

• object variable x of type s

• second-order type variables α Dependent functions have type ∀x : s.p(x), ∀α.p(α).

\frac{f : ∀x : s.p(x) t : s}{f t : p(t)}  \frac{f : ∀α.p(α)}{f : p(A)}

Notational remark In the proposition as type paradigm, one may identify the products

∀x : P.Q ≡ P ⇒ Q ∀α : Prop.P ≡ ∀α.P Existential quantifiers ∃x : s.p(x) can also be seen as an inductive definition sig_{p}

dpair : ∀x : s.p(x) → sig_{p}

Dependent pair or disjoint union with constructors indexed by t : s

                    dpair_{t} : p(t) → sig_{p}

Introduction rule/constructor :

\frac{t : s u : p(t)}{dpair t u : sig_{p}}  \frac{p(t)}{∃x : s.p(x)}

Elimination (x is a fresh variable) :

\frac{u : sig_{p} x : s, y : p(x) ⊢ f : C}{let (x, y) = u in f : C} \frac{∃x : s.p(x) p(x) ⊢ C}{C}

C. Paulin-Oregon-June 2003 28

Second order existential quantification Second order type p(α) depending on type variable α. ∃α.p(α) can also be seen as an inductive definition sig_{p} :

Eintro : ∀α.p(α) → sig_{p}

Introduction rule/constructor :

\frac{u : p(A)}{Eintro A u : sig_{p}}  \frac{p(A)}{∃α.p(α)}

Elimination (α is a fresh type variable) :

\frac{u : sig_{p} y : p(α) ⊢ f : C}{let (α, y) = u in f : C}  \frac{∃α.p(α) p(α) ⊢ C}{C}

C. Paulin-Oregon-June 2003 29

Constructive interpretation of disjonction

Any value of type sum_{α,β} is either inl(a) or inr(b). If p is a program of type sum_{α,β} without free variables, then it evaluates to a value of type sum_{α,β}. Logical interpretation : any proof without hypotheses of A ∨ B can be reduced by cut-elimination to a proof which ends by

\frac{A}{A ∨ B} or \frac{B}{A ∨ B}

So either A or B are also provable.

Constructive interpretation of existential quantifier

A value in sig_{p} is (dpair t u) with u : p(t).

Any proof without hypothesis of ∃x.p(x) can be normalized to a proof ending with an introduction rule.

\frac{p(t)}{∃x : s.p(x)}

Constructive property : If ∃x : s.p(x) is provable, then one can find a term t such that p(t) is provable.

Categorical view Sum and product

\begin{matrix}A & C \\ A + B & B \end{matrix}  \begin{matrix}A & C \\ A ∗ B & B \end{matrix}

Recursion : monotonic functor X ↦ F (X)

c : F (I)  I F (recf)  recf f : F (C)  C recf(c p) = f(F recf) p

Dual notion : co-inductive types Primitive recursion

g : nat^{k} → nat, h : nat^{k+2} → nat

define a unique function f : nat^{k+1} → nat s.t.

\{ \begin{matrix}f(0, x_{1}, …, x_{k}) & = g(x_{1}, …, x_{k}) \\ f(n + 1, x_{1}, …, x_{k}) & = h(n, f(n, x_{1}, …, x_{k}), x_{1}, …, x_{k}) \end{matrix}

Remark Categorical construction gives a weaker (but equivalent) iterative scheme

\{ \begin{matrix}f(0, x_{1}, …, x_{k}) & = g(x_{1}, …, x_{k}) \\ f(n + 1, x_{1}, …, x_{k}) & = h(f(n, x_{1}, …, x_{k}), x_{1}, …, x_{k}) \end{matrix}

Recursive definitions

Algebraic view (rewriting)

length (Nil)=0
length (Cons(n,l))=1+length (l)

Testing and projecting

let rec length x = if isNil x then 0 else 1+length (tl x)

Pattern-matching

let rec length x = match x with

    Nil → 0

| Cons(n,l) → 1+(length l)

Primitive recursive functionals

Generalisation g : α, h : nat → α → α define a unique function f : nat → α s.t.

\{ \begin{matrix}f(0) & = g \\ f(n + 1) & = h(n, f(n)) \end{matrix}

Gödel system T, a combinator R_{α} : α → (nat → α → α) → nat → α s.t.

\{ \begin{matrix}R_{α} g h 0 & ⟶ g \\ R_{α} g h (n + 1) & ⟶ h n (R_{α} g h n) \end{matrix}

Functional definition of min min is a primitive recursive function. Easy definition as a primitive recursive functional.

    min  : nat → (nat → nat)

min 0 m  = 0
min n + 1 m = if m = 0 then 0 else (min n (m − 1)) + 1

C. Paulin-Oregon-June 2003 36

Ackermann function

ack(0, m)  = m + 1
ack(n + 1, 0)  = ack(n, 1)
ack(n + 1, m + 1) = ack(n, ack(n + 1, m))

Primitive recursive functional

 ack  : nat → (nat → nat)

ack 0 m  = m + 1

 ack n + 1 m = ack aux m n (ack n)
ack aux  : nat → nat → (nat → nat) → nat

ack aux 0 n f  = (f 1)
ack aux (m + 1) n f = (f (ack aux m n f))

Uniform tree of height n

                  uniform : nat → itree

let rec uniform x = match x with

     0 → Leaf | S(n) → Node(fun p →uniform n)
uniform 3 ≡
                             Node(.)
             Node(.)
    Node(.)  Node(.)
Leaf Leaf .. Leaf Leaf .. Leaf Leaf .. Leaf Leaf ..

..

                                        Node(.)
                              Node(.)  Node(.)

..

..

Tree of infinite height

let inft = Node(uniform )
inft ≡ Node(.) Leaf  Node(.) {Leaf \atop ..} Node(.) _{Node(.) {Leaf \atop ..} ..}  Node(.) _{Node(.) _{Node(.) {Leaf \atop ..} ..} ..} ..

Unbounded height Tree of infinite height (2)

Each branch is finite Length of a path : [p_{0}; p_{1}; ..; p_{n}; ..] Path represented as a function p : nat → nat

lgpath : (nat → nat) → itree → nat

let rec lgpath p x = match x with

   Leaf → 0

| Node(f) → 1+(lgpath (shift p) (f (p 0)))

               ∀p.(lgpath p (uniform n)) = n

∀p.(lgpath p inft) = 1 + (p 0)

Non terminating computations

let gcd a b = if a = b then a else if a < b then gcd a (b-a) else gcd (a-b) b

(gcd a b) loops when b ≤ 0 or a ≤ 0

Unbounded search p :nat→ bool let search n = if p n then n else search (n+1) (search n) loops unless ∃k ≥ n.(p k) = true

Strong normalisation is lost !

Other recursive schemes

let gcd n a b = if n=0 then fail else if a = b then a else if a < b then gcd (n-1) a (b-a) else gcd (n-1) (a-b) b

Structural recursion Computes gcd with the extra assumption that a + b < n Assuming a + b < n, show a + (b − a) < n − 1 and (a − b) + b < n − 1 requires a > 0 and a > 0 Bounded search

Assume p :nat→ bool

let search k n = if k=0 then fail else if p n then n else search (k-1) (n+1)

(search k n) correct when ∃l.n ≤ l < n + k.(p l) = true Extra argument protects unwanted reduction and bounds the number of reductions. Additional cost.

Theoretical result

Any recursive function, provably total in higher-order arithmetic can be represented using (higher-order) primitive recursive scheme.

• Take a recursive function f

• Kleene T ,U (primitive recursive) : natural number n which represents f : f(x) = y ⇔ ∃k.T(n, x, k) ∧ U(k) = y

• f is provably total if there is a proof of : ∀x.∃k.T(n, x, k)

• From this proof, one can extract a (higher-order) primitive recursive representation.

Maybe not the appropriate algorithm !

Recursive definition of (infinite) values

let rec one = Cons(1,one)
          (lengthone) ⟶ 1 + (lengthone) ⟶ · · ·

C. Paulin-Oregon-June 2003 45

Non recursive but non terminating term

type lambda = Lam of lambda → lambda
let delta = Lam (fun x → app x x)
let omega = app delta delta

Reduction

 omega ≡ app (Lam (fun x →app x x)) delta

⟶ (fun x →app x x) delta

        ⟶ app delta delta
        ≡ omega

C. Paulin-Oregon-June 2003 46

Recursion

• Limited scheme for structural recursion – covers pattern-matching and fixpoint – logical point of view

– classical proofs of normalisation

• Fixpoint – requires additional pattern-matching – computational point of view

– criteria for termination Induction principles

Let I be an inductive definition with rules of constructions c_{1},…,c_{n} How do I prove ∀x : I.P (x) ?

Case analysis

Any value of type I can be reduced to c_{i}(a_{1}, …, a_{k})

\frac{(∀a_{1}, … a_{k}.x = c_{i}(a_{1}, …, a_{k}) ⇒ P (x)) i ∈ \{1 … n\}}{∀x : I.P (x)}

\frac{(∀a_{1}, … a_{k}.P (c_{i}(a_{1}, …, a_{k}))) i ∈ \{1 … n\}}{∀x : I.P (x)}

C. Paulin-Oregon-June 2003 48

Dependent type for match

\frac{x : sum_{α,β} a : α ⊢ f : P (inl(a)) b : β ⊢ g : P (inr(b))}{match x with inl(a) → f|inr(b) → g : P (x)}

\frac{x : prod_{α,β} a : α, b : β ⊢ p : P (pair a b)}{let (a, b) = x in p : P (x)}

General case

\frac{x : I (a_{1}, … a_{k} ⊢ f_{i} : P (c_{i}(a_{1}, …, a_{k}))) i ∈ \{1 … n\}}{match x with … |c_{i}(a_{1}, …, a_{k}) → f_{i}| …: P (x)}

C. Paulin-Oregon-June 2003 49

Properties Types are preserved by reduction

match inl(t) with inl(a) → f|inr(b) → g : P (inl(t))
↓
f[a := t]  : P (inl(t))

C. Paulin-Oregon-June 2003 50

Consequence on disjonction

Assume

classic : ∀ A. A ∨ ¬ A
diff : true ≠ false

Define

witness A = match classic A with
    inl a → true |  inr na → false

Prove ∀A.(witness A) = true ⇔ A by case analysis on the proof of (classic A)

Building a paradox

bool : Prop
witness : Prop → bool
T : bool → Prop := [b]b=true

∀ A. (T (witness A)) ⇔ A)

leads to a paradox (Girard) : J. Hurkens adapted by H. Geuvers

look at coq/theories/Logic/Hurkens.v

Deduce (∀A.A ∨ ¬A) ⇒ true = false Classical logic implies proof-irrelevance Consequences on existential type sig_{p} admits two projections

π_{1} : sig_{p} → s
π_{1} t = let (x, y) = t in x

Dependent case analysis :

\frac{u : sig_{p} x : s, y : p(x) ⊢ f : P (dpair x y)}{let (x, y) = u in f : P (u)}

Defines P (u) ≡ p(π_{1}(u)) P (dpair x y) is equivalent (up to computation) to p(x).

\frac{u : sig_{p} x : s, y : p(x) ⊢ y : P (dpair x y)}{let (x, y) = u in y : P (π_{1} u)}

C. Paulin-Oregon-June 2003 53

Induction

Captures the fact that we consider the smallest set of objects built with constructors. Consider only strictly positive inductive definitions I. If a rule of construction has type A_{1} → ⋯ → A_{k} → I then

• either I doest not occur in A_{i}

• or A_{i} ≡ C_{1} → ⋯ → C_{l} → I and I doest not occur in C_{j}

\frac{(∀a_{1}, … a_{k}. · · · (∀y_{1} … y_{l}.(P (a_{i} y_{1}, … y_{l}))) → ⋯ (P (c_{i}(a_{1}, …, a_{k})))_{i∈\{1...n\}}}{∀x : I.P (x)}

Induction with more general definitions

Dependent types : Rule of construction has type : ∀a_{1} : A_{1} … ∀a_{k} : A_{k}.I Recursive argument : A_{i} ≡ ∀y_{1} : C_{1} … ∀y_{l} : C_{l}.I Same rule applies. Multiple inductive definition : Node : treelist → tree

\frac{∀f : treelist.all list(P, f) → P (Node(f))}{∀x : tree.P (x)}

         all list(P, Nil)

                           \frac{P (a) all list(P, l)}{all list(P, Cons(a, l))}

C. Paulin-Oregon-June 2003 55

Exemple : infinitely branching trees

\frac{P (Leaf) ∀f : nat → itree.(∀n : nat.P (f n)) ⇒ P (Node(f))}{∀x : itree.P (x)}

We can associate to this rule, an operator for structural recursion on the type.

\frac{b : P (Leaf) r : ∀f : nat → itree.(∀n : nat.P (f n)) ⇒ P (Node(f))}{itree rec : ∀x : itree.P (x)}

with \{ \begin{matrix}itree rec(Leaf) & = b \\ itree rec(Node(f)) & = r f (λ n.itree rec(f n)) \end{matrix}

Basic rules of Martin-Löf’s Type Theory/ Strong normalisation.

Definition of types/properties by induction We often define a type or property by induction on a term.

\begin{aligned}P (0) & ⇔ G \\ P (n + 1) & ⇔ H(n, P (n)) \end{aligned}

Examples

arr(0) ⇔ A arr(n + 1) ⇔ A → arr(n)
even(0) ⇔ ⊤ even(n + 1) ⇔ ¬even(n)

C. Paulin-Oregon-June 2003 57

Definition of properties by induction Non monotonic constructions Kripke semantics : W ⊢ P

W ⊢ (P ⇒ Q) ⇔ ∀W′.W ⊆ W′ ⇒ (W′ ⊢ P) ⇒ (W′ ⊢ Q) Reducibility candidate : t ∈ [T]_{ρ}

\begin{aligned}t ∈ [P ⇒ Q]_{ρ} & ⇔ ∀x.x ∈ [P]_{ρ} ⇒ (t x) ∈ [Q]_{ρ} \\ t ∈ [∀α.P]_{ρ} & ⇔ ∀C.t ∈ [P]_{ρ,α↦C} \end{aligned}

More with inductive relations

C. Paulin-Oregon-June 2003 58

Strong elimination scheme Replace equivalence by definitional equality

Proposition definition

P (0)  = G
P (n + 1) = H(n, P (n))

Proof/object definition

f(0)  = g
f(n + 1) = h(n, P (n))

A general scheme

\frac{T (n) type g : T (0) h : ∀x.T (x) ⇒ T (x + 1)}{f : ∀x.T (x)}

with f the unique function such that \{ \begin{matrix}f(0) & = g \\ f(n + 1) & = h(n, f(n)) \end{matrix} Strong elimination : consequences

C. Paulin-Oregon-June 2003 59

• Computation on propositions/types

• Strong elimination for bool gives a proof of true ≠ false (otherwise, proof-irrelevance model)

   \{ \begin{matrix}T & : bool → Prop \\ T(true) & = ⊤ \\ T(false) & = ⊥ \end{matrix}

                                   true = false
                                T(true) = T(false)

⊤ = ⊥ () : ⊤

⊥

C. Paulin-Oregon-June 2003 60

Strong elimination and second-order existential

\frac{C type u : sig_{p} y : p(α) ⊢ f : C}{let (α, y) = u in f : C}

Take p(α) = ⊤ (∃α.⊤) and C = Prop Define B = sig_{p} : Prop Define π : B → Prop = [u]let (α, y) = u in α Define ϵ : Prop → B = [α]Eintro(α, ())

π(ϵα) = α

Leads to a paradox! Strong elimination is only acceptable for small types (arguments of constructors are specific propositions or sets not the universe of all propositions or sets)

Strong elimination and programming Non ML-typable program

\frac{b : bool 0 : T(true) (0, 0) : T(false)}{match b with true → 0 | false → (0, 0) : T(b)}

T  : bool → type

                  T(true) = nat
                  T(false) = nat∗ nat

No value in T(b) when b does not start with a constructor. First eliminate b!

C. Paulin-Oregon-June 2003 62

Inductive types : summary

• Algebraic types, ML data types

• Dependent pair, second-order existential

• Non positive inductive definitions have unwanted behavior • Strong relation between computation and deduction

• Primitive recursive definitions

• Other recursive definitions may be problematic More on that, when studying properties Inductive relations

• Logic programming

• Semantics

• Equality

• Well-founded relations

• Recursive definitions of types

• Dependent types Logic programming inf(a, l) when a is less than any element of the list l

inf(a,Nil) :-
inf(a,Cons(b,l)) :- a ≤ b, inf(a,l)

sorted(l) when l is a sorted list

sorted(Nil) :-
sorted(Cons(a,l)) :- inf(a,l),sorted(l)

insert(a, l, m) when the list m is obtained by insertion of a in l

insert(a,Nil,Cons(a,Nil)) :-
insert(a,Cons(b,l),Cons(a,Cons(b,l))) :- a ≤ b
insert(a,Cons(b,l),Cons(b,m)) :- b < a,insert(a,l,m)

• Well-defined notion

• Executable specification

  insert(2, Cons(1, Cons(3, Nil)),?)

Find m such that insert(2, Cons(1, Cons(3, Nil)), m) holds

• Establish properties

  sorted(l) ⇒ (insert(a, l, m) ⇒ sorted(m))

Inductive definitions in logical systems Inference rules for minimal logic

\frac{P ∈ Γ}{Γ ⊢ P} \frac{Γ, P ⊢ Q}{Γ ⊢ P ⇒ Q} \frac{Γ ⊢ P ⇒ Q Γ ⊢ P}{Γ ⊢ Q}

Reflexive-transitive closure of a property

\overline{R^{∗}(x, x)} \frac{R(x, y)}{R^{∗}(x, y)} \frac{R^{∗}(x, y) R^{∗}(y, z)}{R^{∗}(x, z)}

More operational definition (one proof for one path)

\overline{R^{∗}(x, x)}  \frac{R^{∗}(x, y) R(y, z)}{R^{∗}(x, z)}

C. Paulin-Oregon-June 2003 67

Operational semantics Expressions :

e := x|e.f| …

Static typing γ ⊢ e : τ

\frac{x : τ ∈ γ}{γ ⊢ x : τ} \frac{γ ⊢ e : Class(C) isfield(f, C, τ)}{γ ⊢ e.f : τ}

Operational semantics m, e ↦ m′, v

\frac{access(m, x, v)}{m, x ↦ m, v} \frac{m, e ↦ m′, a access field(m, a, f, v)}{m, e.f ↦ m′, v}

C. Paulin-Oregon-June 2003 68

General scheme of inductive relations

• Precise the arity of the definition I(x_{1}, …, x_{n})

• Gives rules of constructions :

\frac{A_{1} … A_{n}}{I(t_{1}, …, t_{n})}

Implicit quantification over free variables :

∀x_{1}, …, x_{k}.A_{1} ⇒ ⋯ A_{n} ⇒ I(t_{1}, …, t_{n})

A_{i} may contain recursive occurrences of I.

C. Paulin-Oregon-June 2003 69

Rules In case of positive occurrences of I in A_{i}. Introduction rules associated to each rule of construction :

∀x_{1}, …, x_{k}.A_{1} ⇒ ⋯ A_{n} ⇒ I(t_{1}, …, t_{n})

Minimality property : let P (z_{1}, …, z_{n}) be a property of same arity

\frac{(∀x_{1}, …, x_{k}.A_{1}[I := P] ⇒ ⋯ A_{n}[I := P] ⇒ P (t_{1}, …, t_{n})) for all rules}{∀z_{1}, …, z_{n}.I(z_{1}, …, z_{n}) ⇒ P (z_{1}, …, z_{n})}

C. Paulin-Oregon-June 2003 70

Generalized scheme Dependent functions in introduction rules

∀x_{1} : A_{1}, …, x_{k} : A_{k}.I(t_{1}, …, t_{n})

Recursion instead of iteration scheme

\frac{(∀x⃗ : A⃗.A_{i_{1}}[I := P] ⇒ ⋯ A_{i_{l}}[I := P] ⇒ P (t_{1}, …, t_{n})) for all rules}{∀z_{1}, …, z_{n}.I(z_{1}, …, z_{n}) ⇒ P (z_{1}, …, z_{n})}

C. Paulin-Oregon-June 2003 71

Example : transitive closure

Iteration, first definition

\frac{∀x.P (x, x) ∀x, y.R(x, y) ⇒ P (x, y) ∀x, y, z.P (x, y) ⇒ P (y, z) ⇒ P (x, z)}{∀x, y.R^{∗}(x, y) ⇒ P (x, y)}

Iteration, second definition

\frac{∀x.P (x, x) ∀x, y, z.P (x, y) ⇒ R(y, z) ⇒ P (x, z)}{∀x, y.R^{∗}(x, y) ⇒ P (x, y)}

Example : transitive closure, other eliminations Generalized elimination Q(x, y) = R^{∗}(x, y) ∧ P (x, y)

\frac{∀x.P (x, x) ∀x, y, z.R^{∗}(x, y) ⇒ P (x, y) ⇒ R(y, z) ⇒ P (x, z)}{∀x, y.R^{∗}(x, y) ⇒ P (x, y)}

Case analysis

\frac{∀x.P (x, x) ∀x, y, z.R^{∗}(x, y) ⇒ R(y, z) ⇒ P (x, z)}{∀x, y.R^{∗}(x, y) ⇒ P (x, y)}

Parameterized version (fix x the basic element)

\frac{P (x) ∀y, z.R^{∗}(x, y) ⇒ P (y) ⇒ R(y, z) ⇒ P (z)}{∀y.R^{∗}(x, y) ⇒ P (y)}

Q(x, y) = P (x) ⇒ (∀y, z.R^{∗}(x, y) ⇒ P (y) ⇒ R(y, z) ⇒ P (z)) ⇒ P (y)

C. Paulin-Oregon-June 2003 73

Equality

Smallest reflexive binary relation x = y Rule for construction : ∀x.x = x Minimality :

\frac{∀x.P (x, x)}{∀x, y.x = y ⇒ P (x, y)}

Fix t, define a unary predicate t = y of terms equal to t (eq_{t}(y)) Rule for construction : t = t (eq_{t}(t)) Minimality (Leibniz rule)

\frac{P (t)}{∀y.t = y ⇒ P (y)} \frac{t = u P (t)}{P (u)}

C. Paulin-Oregon-June 2003 74

Equality as an essential notion The rule of constructor :

∀x_{1} : A_{1}, …, x_{k} : A_{k}.I(t_{1}, …, t_{n})

Can be reformulated as :

\begin{matrix}∀x_{1} : A_{1}, …, x_{k} : A_{k}.x = (t_{1}, …, t_{n}) ⇒ I(x) \\ (∃x_{1} : A_{1}, …, x_{k} : A_{k}.x = (t_{1}, …, t_{n})) ⇒ I(x) \end{matrix}

Fixpoint

I(x) ⇔ ⋁(∃x_{1} : A_{1}, …, x_{k} : A_{k}.x = (t_{1}, …, t_{n}))

Inductive relations = equality + smallest fixpoint

C. Paulin-Oregon-June 2003 75

R^{∗}(p) ⇔ \begin{matrix}∃x : A.p = (x, x) \\ ∨ ∃x, y, z : A.R^{∗}(x, y) ∧ R(y, z) ∧ p = (x, z) \end{matrix}

Alternative caracterisation

R^{∗}(x, t) ⇔ \begin{matrix}t = x \\ ∨ ∃y, z : A.R^{∗}(x, y) ∧ R(y, z) ∧ t = z \end{matrix}

Well-founded relation

A binary relation R of type A is well-founded if there is no infinite decreasing sequence : (f : nat → A)(∀n.R(f(n + 1), f(n))) → ⊥ Constructive definition for an element x of A, to be well-founded.

\frac{∀y.R(y, x) ⇒ wf(y)}{wf(x)}

Branching on x parameterized by {y : A|R(y, x)} Associated minimality (generalized elimination) principle

\frac{∀x.(∀y.R(y, x) ⇒ wf(y)) ⇒(∀y.R(y, x) ⇒ P (y)) ⇒ P (x)}{∀x.wf(x) ⇒ P (x)}

Associating terms to proofs Follows the same pattern as for inductive types:

• Give a name to each rule of construction, seen as a constructor • Associate a combinator to the elimination scheme Example R*refl : ∀x.R^{∗}(x, x) R*add : ∀x, y, z.R^{∗}(x, y) ⇒ R(y, z) ⇒ R^{∗}(x, z)

\frac{f : ∀x.P (x, x) g : ∀x, y, z.R^{∗}(x, y) ⇒ P (x, y) ⇒ R(y, z) ⇒ P (x, z)}{R*ind_{f,g} : ∀x, y.R^{∗}(x, y) ⇒ P (x, y)}

(R*ind_{f,g} x x R*refl(x))  ⟶ f
(R*ind_{f,g} x z R*add(x, y, z, p, r)) ⟶ (g x y z p (R*ind_{f,g} x y p) r)

C. Paulin-Oregon-June 2003 78

Well-founded induction The relation is well-founded if all the elements are well-founded

wfR : ∀x.wf(x) \frac{∀x.(∀y.R(y, x) ⇒ P (y)) ⇒ P (x)}{∀x.P (x)}

Associated proof-terms Introduction rule : wf intro : ∀x.(∀y.R(y, x) ⇒ wf(y)) ⇒ wf(x) Elimination rule :

\frac{F : ∀x.(∀y.R(y, x) ⇒ wf(y)) ⇒ (∀y.R(y, x) ⇒ P (y)) ⇒ P (x)}{wfind_{F} : ∀x.wf(x) ⇒ P (x)}

(wfind_{F} x (wf intro x f)) ⟶ (F x f λy.λr.(wfind_{F} y (f y r)))

C. Paulin-Oregon-June 2003 79

Well-founded recursion

Associated proof-term :

\frac{F : ∀x.(∀y.R(y, x) ⇒ P (y)) ⇒ P (x)}{(fix F) = λx.(wfind_{λx,a,r.(F x r)} x (wfR x)) : ∀x.P (x)}

Well-founded recursion corresponds to structural recursion on a proof of wf(x). The fixpoint reduction is guarded by the proof (wfR x) of (wf x) which should start with a constructor. When (wfR x) = (wf intro x f), (fix F x) ≃ (F x λy.λr.(fix F y))

Inversion scheme Elimination schemes proves universally quantified properties

∀x_{1}, …, x_{l}.I(x_{1}, …, x_{l}) ⇒ P (x_{1}, …, x_{l})

No quantification over parameters

• What to do with I(t_{1}, …, t_{l}) ⇒ P (t_{1}, …, t_{l}) when t_{i} are not variables ?

• Generalize to ∀x_{1}, …, x_{l}.I(x_{1}, …, x_{l}) ⇒ P (x_{1}, …, x_{l})

• What to do if the generalization does not hold ?

• Find another one which works :

∀x_{1}, …, x_{l}.I(x_{1}, …, x_{l}) ⇒ (x_{1}, …, x_{l}) = (t_{1}, …, t_{l}) ⇒ P (t_{1}, …, t_{l}) Use non-recursive elimination on I

C. Paulin-Oregon-June 2003 81

Inversion : example Le(n, m)

Constructors :

Le0 : ∀m.Le(0, m) LeS : ∀n, m.Le(n, m) ⇒ Le(n + 1, m + 1)

Elimination :

\frac{∀m.P (0, m) ∀n, m.Le(n, m) ⇒ P (n, m) ⇒ P (n + 1, m + 1)}{∀n, m.Le(n, m) ⇒ P (n, m)}

How to prove ∀p, q.Le(p + 1, q + 1) ⇒ Le(p, q) ? Take P (n, m) = n = p + 1 ⇒ m = q + 1 ⇒ Le(p, q) Each case either eliminated by contradiction 0 ≠ q + 1 or simplified n + 1 = p + 1 ⇒ n = p Exercise : Prove ∀k.Le(k + 1, 0) ⇒ ⊥ ?

Proofs as objects

Consider proofs of inductive relations as objects

• Size of a derivation

• Path associated to the transitive closure Define recursive functions : path : ∀x, y : A.(R^{∗} x y) → (list A)

path x x R*refl(x) = Nil

path x z R*add(x, y, p, r) = Cons(y, path x y p) Reasoning on this function requires a dependent elimination scheme Dependent elimination scheme for inductive relations P (x, y, p) with p : R^{∗}(x, y)

\frac{f : ∀x.P (x, x, R*refl(x)) g : \begin{matrix}∀x, y, z. \\ ∀p : R^{∗}(x, y).P (x, y, p) ⇒ ∀r : R(y, z).P (x, z, R*add(x, y, z, p, r)) \end{matrix}}{(R*ind f g) : ∀x, y.∀p : R^{∗}(x, y).P (x, y, p)}

Same reduction rules

C. Paulin-Oregon-June 2003 84

Constructive interpretation of inductive relations

A relation may be defined inductively in many different ways Example

sorted(Nil)

∀a, l, m.sorted(l) ⇒ sorted(m)

    ⇒ inflist(a, m) ⇒ suplist(a, l)
    ⇒ sorted(app l Cons(a, m))

Proving equivalence may be difficult Each definition carry out a specific induction principle A proof corresponds to a concrete representation (prove transitivity of LE!)

Dependent types

Use inductive relations to represent more precise types.

• Lists of length n

• Terms of sort s

Example

Nil : (list 0)

Cons : ∀n : nat.A → (list n) → (list n + 1) No interest as a predicate on nat

map_{f} : ∀n : nat.(list n) → (list n)
map_{f} 0 Nil = Nil

map_{f} (n + 1) Cons(n, a, l) = Cons(n, f(a), map_{f} n l) app : ∀n, m : nat.(list n) → (list m) → (list n + m)

Dependent types : difficulties

Extra arguments of Cons, map , app for typing the real arguments ... Propositional equality between terms with the same type (app n 0 l Nil) = l not well-formed because (app n 0 l Nil) : (list (n + 0)) and l : (list n) not convertible Requires more sophisticated equalities (dependent, John Major ...) Cannot always replace a sub-term with a variable of the same type Example 0 : nat in (app n 0 l Nil). Expect instance elimination scheme / partial pattern-matching

\frac{x : (list 0) f : P (Nil)}{match x with Nil → f : P (x)}

C. Paulin-Oregon-June 2003 87

Mutual Inductive definition

A mutually inductive definition can be encoded as a single inductive family. An argument serves as an index.

I_{1}(a_{1} : A_{1}) … I_{n}(a_{n} : A_{n}) c : ∀x_{1} : B_{1} … ∀x_{l} : B_{l}.I_{i}(t_{i})

Introduce a set of indexes X

inl_{i} : A_{i} → X I(x : X) Replace in the constructors, I_{i}(a_{i}) by I(inl_{i}(a_{i}))

Recursive definition of properties

Define a property F n by induction on n

F 0 ⇔ G F (n + 1) ⇔ H(n, (F n))

H is stable with respect to equivalence : (P ⇔ Q) ⇒ (H(n, P) ⇔ H(n, Q)) Inductive definition of “ϕ is a partial solution up to n”

\frac{ϕ 0 ⇔ G}{(partial ϕ 0)} \frac{(partial ϕ n) ϕ (n + 1) ⇔ H(n, (ϕ n))}{(partial ϕ n + 1)}

Main property (induction on n):

(partial ϕ n) ⇒ (partial ψ n) ⇒ (ϕ n ⇔ ψ n)

Building the solution Takes the union of all partial solutions (higher-order quantification)

sol n ≡ ∃ϕ.(partial ϕ n) ∧ ϕ n

Check

∀ϕ.(partial ϕ n) ⇒ ((ϕ n) ⇔ (sol n))

Show (partialsol n) by induction on n.

C. Paulin-Oregon-June 2003 90

Inductive relations : summary

• A natural extension of the inductive type case

• Includes propositional equality

• Inversion schemes, partial pattern-matching are not primitive • Even interpreted logically, carry a strong computational content Inductive definitions in different systems

• Rules à la Martin-Löf

• Representation in second-order type theory

• Representation in higher-order logic

• Recursive definitions Martin-Löf’s Type Theory

Intensional Type Theory

• Constructive logic

• Propositions as type paradigm

• Logical connectives represented as inductive definitions

• Dependent elimination scheme

• Associated recursion operator

• Extension with universes, inductive-recursive schemes, records … Rules for primitive inductive definitions t, T := prop|x|λx : T.t|∀x : T.T | Ind(I : T){c_{1} : T_{1}| … |c_{n} : T_{n}}|Constr(i, T)|Elim(T)(t_{1}, …, t_{n}) Formation rule

\frac{(I : T ⊢ T_{1} : prop)_{i=1...n} positivity condition}{Ind(I : T)\{c_{1} : T_{1}| … |c_{n} : T_{n}\} : T}

Introduction rules

\frac{I ≡ Ind(I : T)\{c_{1} : T_{1}| … |c_{n} : T_{n}\} I : T 1 ≤ i ≤ n}{Constr(i, I) : T_{i}}

C. Paulin-Oregon-June 2003 94

Elimination

Elimination rule

\frac{I ≡ Ind(I : T)\{c_{1} : T_{1}| … |c_{n} : T_{n}\} I : T (f_{i} : Φ(T_{i}))_{i=1...n}}{Elim(I)(f_{1}, …, f_{n}) : ∀x⃗.∀p : (I x⃗).P (x⃗, p)}

• Dependent/ Non dependent

• Weak/Strong

• One for both recursion and pattern-matching or one for pattern-matching and a fixpoint

Reduction rule (Elim(I)(f_{1}, …, f_{n}) t⃗ (Constr(i, I) a⃗))

⟶ (f_{i} ϕ(T_{i}, Elim(I)(f_{1}, …, f_{n}), a⃗))

C. Paulin-Oregon-June 2003 95

Martin-Löf’s Type Theory

Related Implementations

• Nuprl, Cornell University – Extensional type theory

– Partial terms

– Subtyping …

• ALF, Göteborg – Pattern-matching with dependent types + fixpoint

• Agda, Göteborg – Non-recursive inductive types (Case)

– Fixpoint on proofs and types

– No inductive relations (only fixpoints, ad-hoc equality)

Second-order encoding

System F (Girards, Reynolds) Second order typed λ-calculus (minimal propositional logic) Types T := α | ∀α.T | T → T Terms t := x | Λα.t | λx.t | (t T) | (t t)

Typing \frac{x : T ∈ Γ}{Γ ⊢ x : T}

\frac{Γ ⊢ t : T α not free in Γ}{Γ ⊢ Λα.t : ∀α.T} \frac{Γ ⊢ t : ∀α.T}{Γ ⊢ (t U) : T [α := U]}
\frac{Γ, x : T ⊢ t : U}{Γ ⊢ λx : T.t : T → U} \frac{Γ ⊢ f : T → U  Γ ⊢ t : T}{Γ ⊢ (f t) : U}

C. Paulin-Oregon-June 2003 97

Encoding inductive types in system F

Type : I Rules of construction : c_{1} : C_{1}, … c_{n} : C_{n} c_{i} : ∀α_{1}…. ∀α_{l}.T_{1} → ⋯ → T_{m} → I Definition : I ≡ ∀α.C_{1}[I := α] → ⋯ → C_{n}[I := α] → α Examples

⊥  ∀α.α
⊤  () : ⊤  ∀α.α → α

bool     true, false : bool  ∀α.α → α → α

nat  0 : nat, S : nat → nat ∀α.α → (α → α) → α
β ∗ γ  P : β → γ → β ∗ γ  ∀α.(β → γ → α) → α
β + γ  inl : β → β + γ  ∀α.(β → α) → (γ → α) → α
inr : γ → β + γ
∃β.T (β) E : ∀β.(T (β) → ∃β.T) ∀α.(∀β.(T (β) → α)) → α

C. Paulin-Oregon-June 2003 98

Deriving constructors and elimination

The non-recursive case We have I ≡ ∀α.C_{1}[I := α] → ⋯ → C_{n}[I := α] → α We want c_{i} : C_{i} ≡ ∀α_{1}…. ∀α_{l}.T_{1} → ⋯ → T_{m} → I C_{i}[I := α] ≡ ∀α_{1}…. ∀α_{l}.T_{1} → ⋯ → T_{m} → α

Definition c_{i} = \begin{matrix}Λα_{1}…. Λα_{l}.λx_{1} : T_{1}…. λx_{m} : T_{m}. \\ Λα.λf_{1} : C_{1}[I := α]…. λf_{n} : C_{n}[I := α] \\ (f_{i} α_{1} ⋯ α_{l} x_{1} ⋯ x_{m}) \end{matrix}

Elimination I ≡ ∀α.C_{1}[I := α] → ⋯ → C_{n}[I := α] → α Elimination just application, non-dependent

\frac{Γ ⊢ p : I Γ ⊢ f_{1} : C_{1}[I := C] … Γ ⊢ f_{n} : C_{n}[I := C]}{Γ ⊢ (p C f_{1} ⋯ f_{n}) : C}

Reduction

c_{i} = \begin{matrix}Λα_{1}…. Λα_{l}.λx_{1} : T_{1}…. λx_{m} : T_{m}. \\ Λα.λf_{1}, …, f_{n}.(f_{i} α_{1} ⋯ α_{l} x_{1} ⋯ x_{m}) \end{matrix}

(c_{i} A_{1} … A_{l} t_{1} … t_{m} C f_{1} ⋯ f_{n}) ⟶ (f_{i} A_{1} … A_{l} t_{1} … t_{m})

C. Paulin-Oregon-June 2003 100

Examples

• Booleans bool = ∀α.α → α → α

– Constructors : true = Λα.λx, y : α.x false = Λα.λx, y : α.y

– Conditional : if : ∀α.α → α → bool = Λα.λf, g : α.λb : bool.(b α f g)

• β ∗ γ = ∀α.(β → γ → α) → α

– Constructor : P = λx : β.λy : γ.ΛC.λf : β → γ → α.(f x y) : β ∗ γ.

– Projections : fst : β ∗ γ → β = λp.(p β λx : β.λy : γ.x) snd : β ∗ γ → γ = λp.(p β λx : β.λy : γ.y)

Recursive case

Condition Each recursive argument T_{i}(I) should be monotonic :

\frac{f : X → Y}{T_{i}[f] : T_{i}(X) → T_{i}(Y)} Allows c : ((I → T) → U) → I

Typical case c : F (I) → I Definition I = ∀α.(F (α) → α) → α Constructor

c = λa : F (I).Λα.λf : F (α) → α.(f (F [λx : I.(x α f)] a))

Typing \begin{matrix}λx : I.(x α f) : I → α \\ F [λx : I.(x α f)] : F (I) → F (α) a : F (I) \\ (F [λx : I.(x α f)] a) : F (α) \end{matrix}

C. Paulin-Oregon-June 2003 102

Recursive case, elimination Iterative non-dependent scheme

\frac{p : I f : f(T) → T}{(p T f) : T}

Example : natural numbers

• nat = ∀α.α → (α → α) → α

• Constructors : 0 = Λα.λx : α.λf : α → α.x S = λn : nat.Λα.λx : α.λf : α → α.x

• Iterator : it = Λα.λx : α.λf : α → α.λn : nat.(n α x f)

\{ \begin{matrix}(it T g h 0) & = g \\ (it T g h (S n)) & = (h (it T g h n)) \end{matrix}

C. Paulin-Oregon-June 2003 103

Impredicative encodings : problems

• true ≠ false not provable (proof-irrelevance model) but true ≠ false implies non-confusion c_{i}(x⃗) ≠ c_{j}(y⃗)

• How to write the predecessor function ?

Fixpoint theorem (nat → 1 + nat) or standard trick to derive recursion from iteration :

(f it 0)  = g

(f it (S n)) = (h (f it n))

(f rec 0)  = g

(f rec (S n)) = (h n (f rec n))

(f' rec 0)  = (0, g)

(f' rec (S n)) = let (n, x) = (f' rec n) in ((S n), (h n x))

Predecessor function Specification pred 0 = 0 pred (n + 1) = n

Definition \{ \begin{matrix}pred′ 0 & = (0, 0) \\ pred′ n + 1 & = let (m, x) = pred′ n in (m + 1, m) \\ pred n & = let (m, x) = pred′ n in x \end{matrix}

Reduction

pred 3 ⟶ let (m, x) = pred′ 3 in x  ⟶ 2
pred′ 3 ⟶ let (m, x) = pred′ 2 in (m + 1, m) ⟶ (3, 2)
pred′ 2 ⟶ let (m, x) = pred′ 1 in (m + 1, m) ⟶ (2, 1)
pred′ 1 ⟶ let (m, x) = pred′ 0 in (m + 1, m) ⟶ (1, 0)
pred′ 0 ⟶ (0, 0)

Representation problems

• pred n requires n steps of computation

• pred (n + 1) and n are in general non equivalent on open terms

• there are closed normal terms in β ∗ γ which are not of the form (P b c) = Λα.λf : β → γ → α.(f b c) Assume β = γ = ⊥ → ⊥ (negative universal quantification, ⊤ → ⊤ works as well) We have id = (λx : ⊥.x) : β Λα.λf : β → γ → α.(f (λx : ⊥.(x α → ⊥ (f id id))) id)

Extensions with fixpoints

• Add fixpoint combinator to improve intensional behavior

– Parigot, Krivine, Audebaud … μα.F (α) = F (μα.F (α)) nat = ∀α.α → (nat → α → α) → α

– Mendler : μ = μα.F (α) c : F (μ) → μ

\frac{ϕ : ∀β.(β → μ) → (β → γ) → F (β) → γ}{rec ϕ : μ → γ} F (μ ∗ γ) → γ

rec ϕ (c p) ⟶ (f μ id (rec ϕ) p) Example nat = μα.(1 + nat) = μα.(∀β.β → (α → β) → β)

\{ \begin{matrix}f 0 & = g \\ f(n + 1) & = h(n, f(n)) \\ (ϕ β p r n) & = (n γ g λx : β.h((p x), (r x))) \end{matrix}

Extensions with dependent types

Extends system F with higher-order type schemes (F_{ω}) or dependent types (Calculus of Constructions). The same scheme applies.

• I : κ with κ an arity (∀z_{1} : s_{1}…. ∀z_{k} : s_{k}.Prop) Examples : Prop → Prop or nat → Prop …

• rules of constructions c_{1} : C_{1}, …, c_{n} : C_{n} C_{i} ≡ ∀x_{1} : T_{1}…. ∀x_{m} : T_{m}.(I t_{1} … t_{k}) Definition I:

\begin{matrix}λz_{1} : s_{1} … λz_{k} : s_{k}. \\ ∀α : κ.C_{1}[I := α] → ⋯ → C_{n}[I := α] → (α z_{1} ⋯ z_{k}) \end{matrix}

Good representation for inductive relations but not for types.

Higher-order logic

HOL, Isabelle/HOL, PVS …

• Objects : simply typed λ-calculus with a type of propositions o, an (infinite) type of individuals ι. Any type is inhabited.

• Higher-order logic ∀x : τ.p(x)

covers quantification on objects ∀x : ι.p(x), ∀x : ι → ι.p(x) and higher-order quantification on propositions ∀x : o.p(x), ∀x : ι → ι → o.p(x)

• Classical logic o = bool, functions as relations.

Representation in higher-order logic

• Description operator ϵx.P (x).

From a relational function F : α → β → o to a term λx.ϵy.F (x, y) : α → β

• Type restriction : from predicates to new types.

τ \begin{matrix}rep \\ ⟶ \\ ⟵ \\ abs \end{matrix} \{x : σ|P (x)\}

Properties of HOL

• The object language cannot be extended with polymorphic quantification.

• The object language can be extended with (primitive) (strictly positive) inductive definitions (ECC, Luo, Goguen).

• Logical connectives, inductive relations can be defined with higher-order quantification.

Product definition : α ∗ β

• Take the type of binary relations X = α → β → o

• Define the pair (a, b) = λx : α.λy : β.x = a ∧ y = b

• Define the set of relations which represents pairs Pair(P) :

\begin{matrix}∃a : α.∃b : β.P (a, b) \\ ∧ ∀a_{1}, a_{2} : α.∀b_{1}, b_{2} : β.P (a_{1}, b_{1}) ⇒ P (a_{2}, b_{2}) ⇒ a_{1} = a_{2} ∧ b_{1} = b_{2} \end{matrix}

• Takes α ∗ β be the type of predicates P which satisfies

  Pair(P).

• Check (a, b) satisfies Pair .

• First projection fst :α ∗ β → α defined as a relation : Fst(p, x) = ∃y : β.rep(p)(x, y).

C. Paulin-Oregon-June 2003 112

Inductive types in HOL

T. Melham, E. Gunter, L. Paulson, J. Harrison… The key steps :

• Build a type X, such that one can build injective functions for the constructors. z : X s : X → X s(x) = s(y) → x = y s(x) ≠ 0

• Define by induction the smallest subset I(x) of X closed by the rules of construction. N(x) = ∀P : X → o.P (z) → (∀y.P (y) → P (s(y))) → P (x)

• Define I as the restriction of X to objects which satisfy I. abs : X → I rep : I → X abs(rep(n)) = n I(x) ⇒ rep(abs(x)) = x I(rep(n))

Properties of the inductive type

• Define constructors with the apropriate type using abs and rep. O = abs(z) S(n) = abs(s(rep(n)))

• S(n) = S(m) s(rep(n)) = s(rep(m)) rep(n) = rep(m) n = m
• S(n) = O s(rep(n)) = z ⊥

• Derive induction principle for I using property I .

\frac{P (0) ∀n : N.P (n) ⇒ P (S(n))}{∀n : N.P (n)}

Show ∀x.N(x) → P (abs(x)) and use Recursion scheme

C. Paulin-Oregon-June 2003 114

Prove the existence of a general recursor

\begin{matrix}∀g : α.∀h : N → α → α. \\ ∃!f : N → α.f(0) = g ∧ ∀n.f(S(n)) = h(n, f(n)) \end{matrix}

Define F : N → α → o inductively :

\overline{F (0, g)} \frac{F (n, a)}{F (S(n), h(n, a))}

Prove ∀n : N.∃a : α.F (n, a) and ∀n : N.∀a, b : α.F (n, a) ⇒ F (n, b) ⇒ a = b and Take f(n) be ϵa.F (n, a). Computation done by equational reasoning.

Building the apropriate support

• A large enough tree set, built from ι,o and function space.

• Existence of injection, using cardinality.

• Monotonic (non strictly) positive inductive types are not legal.

(B → o) ⟶^{λp,q.p=q} ((B → o) → o) \begin{matrix}in \\ ⟶ \\ ⟵ \\ out \end{matrix} B

Injective function f : (B → o) → B

P_{0}(x) = ∃P.f(P) = x ∧ ¬P (x) i_{0} = f(P_{0})

P_{0}(i_{0}) ⇔ ¬P_{0}(i_{0})

Classical technics

• Primitive recursive scheme

• Well-founded recursion

• Compile other schemes to one of these

p 117-1

Recursive definitions

More specific solutions

• Syntactic criteria for termination (Coq)

• Capture structural fixpoint by typing Mendler, Giménez, Barthe, Amadio, Altenkirch …

\frac{f : nat^{x} → α ⊢ t : nat^{s(x)} → α}{let rec f x = t : nat → α}

• Introduce rewriting in conversion – General scheme (Blanqui, Jouannaud, Okada)

– RPO (Walukiewicz, Jouannaud, Rubio)

Normalisation, confluence, consistency, completeness, efficiency of reduction Other extensions

• Record

• Induction-recursion

• Quotient types

• Universes Applications

• Deep embedding of programming languages

• Shallow embedding of programs

• Proof of cryptographic protocols

• Proof by reflexion Deep embedding

Objectives :

• Study the properties of a programming language

• Tools working on this programming language Examples :

• Properties of the Java(Card) Virtual Machine – Byte-code verifier

– Offensive versus defensive machine

– Firewall Deep-embedding : principles

Introduce an inductive type to represent the syntax of programs.

• Abstract syntax tree

• Representation of bounded variables/substitution Different solutions

– De Bruijn indexes

– Explicit substitution

– Higher-order abstract syntax (lambda → lambda)

• Functions on terms

• Semantics as inductive relations or functions Current experiments (Java(Card) programs)

• BALI project in Munich (T. Nipkow,

http://isabelle.in.tum.de/Bali/) - Isabelle/HOL

Type safety of the Java source language and part of the JVM Axiomatic semantic of Java

• FORMAVIE (Trusted Logic, Schlumberger) - Coq Modelisation of security properties of the whole Card system Several applets may run on the card preserving confidentiality

Expected properties of inductive definitions

• Jakarta (INRIA Sophia-Antipolis) - Coq Public semantics of JavaCard Virtual machine, byte-code verifier Functional representation of execution steps On well-typed programs, defensive and offensive machine coincide • Efficient behavior with a large number of rules of construction • Executable specifications

   – TWELF, http://www-2.cs.cmu.edu/˜ twelf/

– Functional representation (Jakarta)

Shallow embedding

Interpret a program in the proof assistant by its semantics

• The LOOP project (B. Jacobs, Nijmegen,PVS)

• Jive (P. Poetzsch-Heffter, Kaiserslautern, Isabelle/HOL)

• Jack (J.-L. Lanet,Gemplus , B)

• Krakatoa (C. Marché, Orsay,Coq) Use concrete data-structures, functions A cryptographic protocol

(L. Paulson in Isabelle/HOL) A system of paid TV

• The decoder n asks the smart-card n whether the fees have been paid.

1. D_{n} ⟶ C_{n} : (D_{n}, m_{1})
2. C_{n} ⟶ D_{n} : (C_{n}, m_{2})

• They share a secret (encrypted) information m_{1}, m_{2}.

• Every exchanged message is public.

Modelisation

Inductive definitions of agents and messages

Inductive agent : Set
   := C : nat→agent | D : nat→agent | I : agent.
Variables key,data : Set.
Inductive message : Set :=
        Name  : agent → message
      | K   : key → message
      | Dat  : data → message
      | Enc : message → key → message
      | P  : message → message → message.

Protocol

Parameterised by the messages m_{1}, m_{2} and a predicate paid such that (paid n) true when the consumer n has paid the fees. Three predicates mutually defined :

send : agent → message → Prop
receive : agent → message → Prop
known : message → Prop

send follows the protocol, but the intruder may send any message he knows. Anybody receives any sent message The intruder knows any message he received, or any public knowledge or what can be deduced from that.

Definitions send and receive

Inductive send  : agent → message → Prop :=
     init   : ∀ n:nat.(send (D n) (P (Name (D n)) m1))
   | trans1 : ∀ n:nat.(receive (C n) (P (Name (D n)) m1)) → (paid  n)
              → (send (C n) (P (Name (C n)) m2))
   | cheat : ∀ m:message.(known m) → (send I m)
with receive : agent → message → Prop :=
     link : ∀ m:message.(A,B:agent) (send A m)→(receive B m)
Definition ok [n:nat] : Prop
   := (receive (D n) (P (Name (C n)) m2)).

Definition known

known : message → Prop :=
  spy: ∀ m:message.(receive I m)→(known m)
| name: ∀ a:agent.(known (Name a))
| decomp_l: ∀ m1,m2:message.(known (P m1 m2))→(known m1)
| decomp_r: ∀ m1,m2:message.(known (P m1 m2))→(known m2)
| compose: ∀ m1,m2:message.
            (known m1)→(known m2)→(known (Pair m1 m2))
| crypt : ∀ m:message. ∀ k:key.
           (known m)→(known (K k))→(known (Enc m k))
| decrypt : ∀ m:message. ∀ k:key.
             (known (Enc m k))→(known (K k))→(known m).

The protocol works properly if the fee has been paid

Lemma paid_get :
   ∀ m1,m2:message.∀ n:nat.(paid n) → (ok m1 m2 n).

First flaw when only one message

Lemma flaw : ∀ m:message. ∀ n:nat.(ok m m n).

1. D_{n} ⟶ I : (D_{n}, m)
2. I ⟶ D_{n} : (C_{n}, m)

Proving correctness

No flaw when nobody has paid.

Definition m1 := (Enc (Data d1) k).
Definition m2 := (Enc (Data d2) k).
Hypothesis no_paid : ∀ n:nat.¬(paid n).
Hypothesis d1_not_d2 : ¬(d1=d2).
Lemma no_flaw : ∀ n:nat.¬(ok m1 m2 n).

Invariant

Inductive invknown :  message → Prop :=
   base : ∀ a:agent.(invknown (Name a))
 | mes  : (invknown m1)
 | invcomp : ∀ m1,m2:message.
       (invknown m1)→ (invknown m2)→(invknown (P m1 m2)).

Lemma invknown_not_ok
   : ∀ n:nat.¬(invknown (P (Name (C n)) m2)).

by inversion of invknown using the shape of m2.

Lemma no_flaw
   : ∀ n:nat.(ok m1 m2 n)→(invknown (P (Name (C n)) m2)).

by mutual induction, anything which is sent or received satisfies

invknown.

A second flaw Variable p:nat.

Hypothesis p_paid : (paid p).
Lemma flaw2 : ∀ n:nat. (ok m1 m2 n).

Trace of the proof

\begin{aligned}D_{p} & ⟶ C_{p} & : (D_{p}, m_{1}) \\ C_{p} & ⟶ D_{p}, I & : (C_{p}, m_{2}) \\ D_{n} & ⟶ C_{n} & : (D_{n}, m_{1}) \\ I & ⟶ D_{n} & : (C_{n}, m_{2}) \end{aligned}

C. Paulin-Oregon-June 2003 134

Inductive definitions in this example

• Limit the knowledge of the intruder

• Correctness with respect to a certain model

• Automatic proof-tool for finding flaws

• Use proof-term as trace of execution Proofs by reflexion

Internalizing a proof procedure. Example Simplify expressions with addition and numerals on natural numbers :

e ⟶ e_{1} + ⋯ + e_{n} + n

with e_{i} an expression which is not an addition nor a numeral and n a numeral. Require tedious steps of rewriting on +.

Reflexion strategy

• lift e to a concrete expression e′

• program a normalisation function norm on concrete expressions • compute (norm e′) to an expression e′′

• show (norm e′) and e′′ represents the same natural number. Consequences

• Meta-strategy programming becomes norm definition

• General proof of correctness of norm

• Reasoning steps are replaced by computation on norm

• Introduce intermediate representation

C. Paulin-Oregon-June 2003 137

Reflexion : quoting

Inductive aexpr : Set :=
    Var : nat → aexpr
  | Plus : aexpr → aexpr → aexpr
  | Num : nat → aexpr.
Fixpoint interp [v:nat→ nat; e:aexpr] : nat :=
   Cases e of (Var x) => (v x)
           | (Plus e1 e2) => (interp v e1)+(interp v e2)
           | (Num n) => n

end.

Reflexion : normalisation

Fixpoint flat [e:aexpr] : nat * (list nat) :=
 Cases e of (Var x) => (O,(cons x (nil nat)))
    | (Plus e1 e2) => let (n1,l1) = (flat e1) in
      let (n2,l2) = (flat e2) in ((n1+n2),(app l1 l2))
    | (Num n) => (n,(nil nat))

end.

Fixpoint exprlv [n:nat; l: (list nat)] : aexpr :=
 Cases l of nil => (Num n)
   | (cons x m) => (Plus (Var x) (exprlv n m))

end.

Definition norm [e:aexpr] : aexpr :=
    let (n,lv)=(flat e) in (exprlv n lv).

Reflexion : Correctness and usage

Lemma flat_correct : ∀ v:nat→ nat.∀ e:aexpr.
    (interp v e)=(interp v (norm e)).

Usage

Variables x,y,z:nat.
Lemma test : ((5+x)+1)+((y+2)+((x*y)+z))=0

Definition v:= [n]Cases n of

   0 ⇒ x | 1 ⇒ y | 2 ⇒ z | 3 ⇒ (x * y) | _⇒ O

end.

Reflexion : Usage

Lemma test :((5+x)+1)+((y+2)+((x*y)+z))=0
Change (interp v
        (Plus (Plus (Plus (Num 5) (Var O)) (Num 1))
        (Plus (Plus (Var 1) (Num 2))
              (Plus (Var 3) (Var 2)))))=O.
Rewrite flat_correct; Simpl.

Result

x + (y + (x ∗ y + (z + 8))) = 0

• Good data-structures

• Efficient reduction strategy

• Automate reasoning on programs Inductive definitions : summary

• A high-level scheme useful in many contexts

• Non recursive data-types related to logic

• Strong relationship between induction and recursion

• Strong rules may lead to inconsistency

• Encodings in HOL and type theory