Library ARS

Abstract Reduction Systems, from Semantics Lecture at Programming Systems Lab, https://www.ps.uni-saarland.de/courses/sem-ws13/


Require Export Base.

Notation "p '<=1' q" := ( x, p x q x) (at level 70).
Notation "p '=1' q" := (p <=1 q q <=1 p) (at level 70).
Notation "R '<=2' S" := ( x y, R x y S x y) (at level 70).
Notation "R '=2' S" := (R <=2 S S <=2 R) (at level 70).

Relational composition

Definition rcomp X Y Z (R : X Y Prop) (S : Y Z Prop)
: X Z Prop :=
  fun x z y, R x y S y z.

Power predicates

Require Import Arith.
Definition pow X R n : X X Prop := it (rcomp R) n eq.

Section FixX.
  Variable X : Type.
  Implicit Types R S : X X Prop.
  Implicit Types x y z : X.

  Definition reflexive R := x, R x x.
  Definition symmetric R := x y, R x y R y x.
  Definition transitive R := x y z, R x y R y z R x z.
  Definition functional R := x y z, R x y R x z y = z.

Reflexive transitive closure

  Inductive star R : X X Prop :=
  | starR x : star R x x
  | starC x y z : R x y star R y z star R x z.


  Lemma star_simpl_ind R (p : X Prop) y :
    p y
    ( x x', R x x' star R x' y p x' p x)
     x, star R x y p x.

  Lemma star_trans R:
    transitive (star R).

Power characterization

  Lemma star_pow R x y :
    star R x y n, pow R n x y.

  Lemma pow_star R x y n:
    pow R n x y star R x y.

Equivalence closure

  Inductive ecl R : X X Prop :=
  | eclR x : ecl R x x
  | eclC x y z : R x y ecl R y z ecl R x z
  | eclS x y z : R y x ecl R y z ecl R x z.

  Lemma ecl_trans R :
    transitive (ecl R).

  Lemma ecl_sym R :
    symmetric (ecl R).

  Lemma star_ecl R :
    star R <=2 ecl R.

Diamond, confluence, Church-Rosser

  Definition joinable R x y :=
     z, R x z R y z.

  Definition diamond R :=
     x y z, R x y R x z joinable R y z.

  Definition confluent R := diamond (star R).

  Definition semi_confluent R :=
     x y z, R x y star R x z joinable (star R) y z.

  Definition church_rosser R :=
    ecl R <=2 joinable (star R).

  Goal R, diamond R semi_confluent R.

  Lemma diamond_to_semi_confluent R :
    diamond R semi_confluent R.

  Lemma semi_confluent_confluent R :
    semi_confluent R confluent R.

  Lemma diamond_to_confluent R :
    diamond R confluent R.

  Lemma confluent_CR R :
    church_rosser R confluent R.


  Lemma pow_add R n m (x y : X) : pow R (n + m) x y rcomp (pow R n) (pow R m) x y.

  Lemma rcomp_1 (R : X X Prop): R =2 pow R 1.

End FixX.

  Instance star_PreOrder X (R:X X Prop): PreOrder (star R).

  Instance ecl_equivalence X (R:X X Prop): Equivalence (ecl R).

  Instance R_star_subrelation X (R:X X Prop): subrelation R (star R).

  Instance pow_star_subrelation X (R:X X Prop) n: subrelation (pow R n) (star R).

  Instance star_ecl_subrelation X (R:X X Prop) : subrelation (star R) (ecl R).

  Instance R_ecl_subrelation X (R:X X Prop): subrelation R (ecl R).