```
```

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).

```
```

Index

This page has been generated by coqdoc