Как нормализовать правила перезаписи, которые всегда уменьшают размер ввода? - PullRequest
Новая
       7

Как нормализовать правила перезаписи, которые всегда уменьшают размер ввода?

0 голосов
/ 09 сентября 2018

Запомните следующий тип данных: 

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 предназначен для замены всех вхождений B (A x) на x. Однако то, как оно написано, не гарантирует, что результат будет в нормальной форме, что видно по тому факту, что нам потребовалось два приложения rwt, чтобы добраться до A (A (B (B x))), которые нельзя переписать дальше.

Есть ли способ написать reduce : AB -> AB в Agda, который будет возвращать тот же результат, как если бы мы неоднократно вызывали rewrite до тех пор, пока не останется B (A x)? И мы можем также получить доказательство этого (возможно reduce : (input : AB) -> Σ AB (λ output . is-reduction-of input && is-in-nf output)?

Попытка:

Приведенная ниже программа всегда возвращает нормальную форму 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

Но как мы можем доказать, что он на самом деле возвращает термин без "redexes" и что он эквивалентен rwt (rwt (rwt ... ab))? Я спрашиваю, потому что я ожидаю, что найдутся популярные методы для решения этой ситуации.

1 Ответ

0 голосов
/ 09 сентября 2018

Вы можете определить переписывание индуктивно, а затем сказать, что обычный термин не переписывается ни для чего. Затем докажите, что reduce является звуком и возвращает нормальные формы. 

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)

Вам нужно будет обобщить reduceSound и reduceNormal для случаев, отличных от 0. В противном случае, оба доказуемы с помощью прямой индукции, поэтому я не думаю, что это можно сделать с помощью какой-либо конкретной техники.

...