AC-normalisation

suc-alg.lp

// Levels as in agda syntax
constant symbol L : TYPE;
symbol Z : L;
symbol S : L → L;
symbol ∪ : L → L → L; notation ∪ infix right 10;
symbol ⋄ : L → L;


// Nat to count succesors 
constant symbol ℕ : TYPE;
constant symbol 0ₙ : ℕ; builtin "0" ≔ 0ₙ;
constant symbol sₙ : ℕ → ℕ; builtin "+1" ≔ sₙ;

// max function on natural numbers
symbol ⊕ₙ : ℕ → ℕ → ℕ; notation ⊕ₙ infix right 10;

rule 0ₙ ⊕ₙ $y ↪ $y
with $x ⊕ₙ 0ₙ ↪ $x
with sₙ $x ⊕ₙ sₙ $y ↪ sₙ ($x ⊕ₙ $y);

// addition on natural numbers

symbol + : ℕ → ℕ → ℕ; notation + infix right 5;

rule 0ₙ + $y ↪ $y
with $x + 0ₙ ↪ $x
with sₙ $x + $y ↪ sₙ ($x + $y)
with $x + sₙ $y ↪ sₙ ($x + $y)
with ($x + $y) + $z ↪ $x + ($y + $z);


constant symbol z : L;
symbol s : ℕ → L → L;
associative commutative symbol ⊕ : L → L → L; // associative right by default
notation ⊕ infix right 10;

// agda's level syntax is translated into the ⊕ algebra 
rule Z         ↪ s 0 z
with S $x      ↪ s 1 $x
with $x ∪ $y   ↪ $x ⊕ $y
with ⋄ $x      ↪ s 0 ($x ⊕ z);

rule s $p (s $q $x) ↪ s ($p + $q) $x
with s $p ($x ⊕ $y) ↪ s $p $x ⊕ s $p $y;

rule s $p $x ⊕ s $q $x ↪ s ($p ⊕ₙ $q) $x
with s $p $x ⊕ (s $q $x ⊕ $y) ↪ s ($p ⊕ₙ $q) $x ⊕ $y;

compute λ x y, ((S (S (⋄ x))) ∪ (S (⋄ y))) ∪ Z;

compute λ x y, s 1 y ⊕ (s 2 x ⊕ (s 0 z ⊕ s 2 z));