CODEWITHSUNDEEP
agda
MaiaVictor
MaiaVictor

Reputation: 52987

How to normalize rewrite rules that always decrease the input's size?

Mind the following datatype:

data AB : Set where
  A : AB -> AB
  B : AB -> AB
  C : AB

rwt : AB -> AB
rwt (B (A ab)) = rwt ab
rwt (A ab)     = A (rwt ab)
rwt (B ab)     = B (rwt ab)
rwt C          = C

ab : AB
ab = rwt (rwt (B (B (A (A (A (A (B (B (A (B C)))))))))))

Here, rwt is meant to replace all occurrences of B (A x) by x. The way it is written, though, doesn't guarantee the result is in normal form, which can be seen by the fact we needed two applications of rwt to get to A (A (B (B x))), which can't be further rewritten.

Is there any way to write reduce : AB -> AB in Agda that will return the same result as if we called rewrite repeatedly until no B (A x) is left? And, can we also get a proof of that (perhaps reduce : (input : AB) -> Σ AB (λ output . is-reduction-of input && is-in-nf output)?

An attempt:

The program below will always return the normal form of ab:

reduce : AB -> ℕ -> AB
reduce (A ab) (suc n) = reduce ab n
reduce (A ab) zero    = A (reduce ab zero)
reduce (B ab) n       = reduce ab (suc n)
reduce C      (suc n) = B (reduce C n)
reduce C      zero    = C

But how do we prove it actually returns a term without "redexes", and that it is equivalent to rwt (rwt (rwt ... ab))? I'm asking because I expect there to be popular techniques to deal with that situation.

Upvotes: 1

Views: 117

Answers (1)

András Kovács
András Kovács

Reputation: 30103

You could define rewriting inductively, then say that a normal term is not rewritable to anything. Then, prove that reduce is sound and returns normal forms.

open import Data.Empty
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

data AB : Set where
  A : AB -> AB
  B : AB -> AB
  C : AB

-- 1-step rewrite
infix 3 _~>_
data _~>_ : AB → AB → Set where
  BA : ∀ {x} → B (A x) ~> x
  A  : ∀ {x y} → x ~> y → A x ~> A y
  B  : ∀ {x y} → x ~> y → B x ~> B y

-- reflexive-transitive closure
infixr 5 _◅_
data Star {A : Set}(R : A → A → Set) : A → A → Set where
  ε   : ∀ {x} → Star R x x
  _◅_ : ∀ {x y z} → R x y → Star R y z → Star R x z

-- n-step rewrite
infix 3 _~>*_ 
_~>*_ : AB → AB → Set
_~>*_ = Star _~>_

normal : AB → Set
normal ab = ∀ {ab'} → ¬ (ab ~> ab')

-- TODO
reduceSound  : ∀ ab → ab ~>* reduce ab 0
reduceNormal : ∀ ab → normal (reduce ab 0)

You will need to generalize reduceSound and reduceNormal for cases other than 0. Otherwise, both are provable by direct induction, so I don't think it could be made easier by any particular technique.

Upvotes: 2

Related Questions