如何规范化总是减小输入大小的重写规则？

Question

注意以下数据类型：

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

此处，rwt 旨在用 x 替换所有出现的 B (A x)。但是，它的编写方式并不能保证结果是正常形式，我们需要两次应用 rwt 才能得到 A (A (B (B x)))，这可以看出这一点，这是不可能的进一步改写。

有没有什么方法可以在 Agda 中编写 reduce : AB -> AB 来 return 与我们重复调用 rewrite 直到没有 B (A x) 相同的结果离开了？而且，我们也可以得到证明吗（也许 reduce : (input : AB) -> Σ AB (λ output . is-reduction-of input && is-in-nf output）？

一次尝试：

下面的程序总是returnab的正常形式：

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

但是我们如何证明它实际上 return 是一个没有 "redexes" 的项，并且它等价于 rwt (rwt (rwt ... ab))？我问是因为我希望有流行的技术来处理这种情况。

Answer 1

你可以归纳地定义重写，然后说一个正常的术语是不可重写的。然后，证明 reduce 是合理的并且 returns 是范式。

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)

对于 0 以外的情况，您需要概括 reduceSound 和 reduceNormal。否则，两者都可以通过直接归纳法证明，所以我不认为可以通过任何特定技术使它变得更容易。

如何规范化总是减小输入大小的重写规则？

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

agda

一次尝试：