|
This Coq module contains a formalization of the computation model based on the combinators K and S. We define an inductive datatype for programs and an inductive reduction relation to express the small-step semantics.
The main result of this module is the confluence of the calculus. It contains also the corollary which says that each term has at most one normal form. (Vincent Cremet - mars 2003 - Coq-7.4) |
| The terms of the calculus. |
Inductive Term: Set :=
K: Term |
S: Term |
app: Term -> Term -> Term.
| One step reduction relation. |
Inductive one_step: Term -> Term -> Prop :=
redk: (m, n: Term) (one_step (app (app K m) n) m) |
reds: (m, n, p: Term) (one_step (app (app (app S m) n) p) (app (app m p) (app n p))) |
redl: (m, m', n: Term) (one_step m m') -> (one_step (app m n) (app m' n)) |
redr: (m, n, n': Term) (one_step n n') -> (one_step (app m n) (app m n')).
| Transitive, reflexive closure of a relation. |
Inductive trclosure[A: Set; reduce: A -> A -> Prop] : A -> A -> Prop :=
trcl_refl: (m: A) (trclosure A reduce m m) |
trcl_trans: (m, n: A) (trclosure A reduce m n) -> (p: A) (trclosure A reduce n p) ->
(trclosure A reduce m p) |
trcl_step: (m, n: A) (reduce m n) -> (trclosure A reduce m n).
| Transitive reflexive closure is monotonic (unused in the confluence proof). |
Lemma trcl_monotonic: (A: Set; rel1, rel2: A -> A -> Prop)
((m, n: A) (rel1 m n) -> (rel2 m n)) ->
((m, n: A) (trclosure A rel1 m n) -> (trclosure A rel2 m n)).
| Reflexive closure of a relation. |
Inductive rclosure[A: Set; red: A -> A -> Prop] : A -> A -> Prop :=
rcl_refl: (m: A) (rclosure A red m m) |
rcl_step: (m, n: A) (red m n) -> (rclosure A red m n).
| The transitive reflexive closure of the reflexive closure of a relation is the transitive reflexive closure of the relation (not used in the confluence proof). |
Lemma tr_rcl_is_trcl:
(A: Set) (rel: A -> A -> Prop)
(m, n: A) ((trclosure A (rclosure A rel) m n) <-> (trclosure A rel m n)).
| General reduction. |
Definition reduce := (trclosure Term one_step).
Lemma reduce_left: (m, m': Term) (reduce m m') -> (n: Term) (reduce (app m n) (app m' n)).
Lemma reduce_right: (m, m': Term) (reduce m m') -> (n: Term) (reduce (app n m) (app n m')).
| The diamond property for a binary relation. |
Definition diamond [A: Set; reduce: A -> A -> Prop]: Prop := (m, n1: A)
(reduce m n1) -> (n2: A) (reduce m n2) ->
(EX p: A | (reduce n1 p) /\ (reduce n2 p))
.
| Definition of the confluence of the calculus. |
Definition confluence: Prop := (diamond Term reduce).
| Definition of the concept of computation of a result by a term. |
Definition computes [m, n: Term]: Prop :=
(reduce m n) /\ (p: Term) ~(one_step n p).
| Parallel reduction (needed for the proof of confluence). |
Inductive par_step: Term -> Term -> Prop :=
par_refl: (m: Term) (par_step m m ) |
park: (m, m', n, n': Term) (par_step m m') -> (par_step n n') ->
(par_step (app (app K m) n) m') |
pars: (m, m', n, n', p, p': Term) (par_step m m') -> (par_step n n') ->
(par_step p p') ->
(par_step (app (app (app S m) n) p) (app (app m' p') (app n' p'))) |
parapp: (m, m', n, n': Term) (par_step m m') -> (par_step n n') ->
(par_step (app m n) (app m' n')).
| The diamond property is preserved by reflexive, transitive closure. |
Lemma diamond_trcl: (A: Set; reduce: A -> A -> Prop)
(diamond A reduce) -> (diamond A (trclosure A reduce)).
| The parallel reduction relation is included in the general reduction relation. |
Lemma par_sub_reduce: (m, n: Term) (par_step m n) -> (reduce m n).
| The one-step reduction relation is included in the parallel reduction relation. |
Lemma onestep_sub_par: (m, n: Term) (one_step m n) -> (par_step m n).
| The transitive reflexive closure of the parallel reduction relation coincides with the general reduction relation. |
Lemma parstar_is_reduce: (m, n: Term)
((trclosure Term par_step m n) <-> (reduce m n)).
| In some cases we can deduce informations on the shape of a reduced term. |
Lemma km: (m, n: Term) (par_step (app K m) n) ->
(EX m': Term | (n = (app K m')) /\ (par_step m m')).
Lemma sm: (m, n: Term) (par_step (app S m) n) ->
(EX m': Term | (n = (app S m')) /\ (par_step m m')).
Lemma smn: (m, n, p: Term) (par_step (app (app S m) n) p) ->
(EX m': Term | (EX n': Term | (p = (app (app S m') n')) /\ (par_step m m') /\ (par_step n n'))).
| Different ways for an application to reduce. |
Lemma decompose: (m1, m2, n: Term) (par_step (app m1 m2) n) ->
(n = (app m1 m2)) \/
(EX l | (EX l' | (EX m2' | m1 = (app K l) /\ (par_step l l') /\ (par_step m2 m2')
/\ (n = l')))) \/
(EX l1 | (EX l2 | (EX l1' | (EX l2' | (EX m2' |
m1 = (app (app S l1) l2) /\ (par_step l1 l1') /\ (par_step l2 l2') /\ (par_step m2 m2')
/\ (n = (app (app l1' m2') (app l2' m2')))))))) \/
(EX m1': Term | (EX m2': Term | (par_step m1 m1') /\ (par_step m2 m2')
/\ (n = (app m1' m2')))).
| Parallel reduction satisfies the diamond property. |
Theorem diamond_par_step: (diamond Term par_step).
| Diamond property is substitutive. |
Lemma substDiamond: (A: Set)(rel1, rel2: A -> A -> Prop)
((m, n: A) ((rel1 m n) <-> (rel2 m n))) -> (diamond A rel1)
-> (diamond A rel2).
| The calculus of combinators K and S is confluent. |
Theorem pConfluence: confluence.
| A stuck term can only reduce to itself. |
Lemma pStuck: (m, n: Term) (reduce m n) -> ((p: Term) ~(one_step m p)) -> (m = n).
| The relation which results to programs is in fact a function. |
Lemma pComputes: (m, n1, n2: Term)
(computes m n1) -> (computes m n2) -> (n1 = n2).