由于我们不需要no 案例的证明，因此切换到这种数据类型可能会更好：
data Dec' {p} (P : Set p) : Set p where
yes : (p : P) → Dec' P
no : Dec' P
因为有n * (n - 1)no 案例和n yes 案例。所以这种表示是相当可扩展的。
还可以使所有这些可判定性自动工作。
这是转换的主要功能：
vecApply : {α γ : Level} {X : Set α} {Z : Set γ} -> (n : ℕ) -> nary n X Z -> Vec X n -> Z
vecApply 0 x _ = x
vecApply (suc n) f (x ∷ xs) = vecApply n (f x) xs
replace' : (n : ℕ) -> nary n AExp (AExp × AExp) -> AExp -> AExp
replace' n f e with getSubterms n f e
replace' n f e | nothing = e
replace' n f e | just xs with vecApply n f xs
replace' n f e | just xs | e' , e'' with e ≟AExp e'
replace' n f e | just xs | .e , e'' | yes refl = e''
replace' n f e | just xs | e' , e'' | no = e
所以你提供了一些函数，它接收n 参数并返回两个表达式。例如：
_==_ : {α β : Level} {A : Set α} {B : Set β} -> A -> B -> A × B
_==_ = _,_
0+-func : AExp -> AExp × AExp
0+-func = λ a2 -> APlus (ANum 0) a2 == a2
第一个表达式是您要查找的内容，第二个表达式用于替换第一个表达式。首先，您需要编写一个函数来查找所有适当的子表达式。例如
ex1-func : (_ _ : AExp) -> AExp × AExp
ex1-func = λ a1 b1 -> AMult (APlus a1 b1) (APlus a1 b1) == ANum 0
对于ex1-func 和这个词
let a1 = ANum 0
in let b1 = ANum 1
in AMult (APlus a1 b1) (APlus a1 b1)
这个函数应该按照这个顺序返回ANum 0 ∷ ANum 1 ∷ []。
要首先实现这一点，您需要确定某个表达式中的所有“漏洞”（上例中的a1 和b1）。然后你需要删除重复项（a1 有两个“洞”，而ex1-func（和任何其他函数）两个洞只接收一个a1）。
这是一个肮脏的解决方案：
enlarge : AExp -> AExp
enlarge a = APlus a a
size : AExp -> ℕ
size (APlus a _) = 1 + size a
size _ = 0
small big : AExp
small = ANum 0
big = enlarge small
transT : Set
transT = AExp -> AExp
transTs : Set
transTs = L.List transT
left : transT
left (ANum x ) = ANum x
left (APlus a b) = a
left (AMinus a b) = a
left (AMult a b) = a
right : transT
right (ANum x ) = ANum x
right (APlus a b) = b
right (AMinus a b) = b
right (AMult a b) = b
directions : AExp -> AExp -> transTs
directions (ANum _) (ANum _) = L.[]
directions (APlus a1 a2) (APlus b1 b2) =
L.map (λ f -> f ∘ left) (directions a1 b1) L.++ L.map (λ f -> f ∘ right) (directions a2 b2)
directions (AMinus a1 a2) (AMinus b1 b2) =
L.map (λ f -> f ∘ left) (directions a1 b1) L.++ L.map (λ f -> f ∘ right) (directions a2 b2)
directions (AMult a1 a2) (AMult b1 b2) =
L.map (λ f -> f ∘ left) (directions a1 b1) L.++ L.map (λ f -> f ∘ right) (directions a2 b2)
directions _ _ = id L.∷ L.[]
add : {l : ℕ} -> ℕ -> transT -> Vec transTs l -> Vec transTs l
add _ d [] = []
add 0 d (x ∷ xs) = (d L.∷ x) ∷ xs
add (suc n) d (x ∷ xs) = x ∷ add n d xs
naryApply : {α γ : Level} {X : Set α} {Z : Set γ} -> (n : ℕ) -> nary n X Z -> X -> Z
naryApply 0 x _ = x
naryApply (suc n) f x = naryApply n (f x) x
naryApplyWith : {α γ : Level} {X : Set α} {Z : Set γ}
-> (n : ℕ) -> nary n X Z -> (X -> X) -> X -> Z
naryApplyWith 0 x _ _ = x
naryApplyWith (suc n) f g x = naryApplyWith n (f x) g (g x)
directionses : (n : ℕ) -> nary n AExp (AExp × AExp) -> Vec transTs n
directionses n f = L.foldr (λ f -> add (size (f e)) f) (replicate L.[]) $
directions (proj₁ $ naryApply n f big) (proj₁ $ naryApply n f small) where
e = proj₁ $ naryApplyWith n f enlarge small
open RawMonad {{...}}
getSubterms : (n : ℕ) -> nary n AExp (AExp × AExp) -> AExp -> Maybe (Vec AExp n)
getSubterms n f e = (λ _ -> map (λ fs -> lhead id fs e) dss) <$> flip (mapM M.monad) dss
(L.sequence M.monad ∘ neighbWith (λ f g -> dec'ToMaybe⊤ $ f e ≟AExp g e)) where
dss = directionses n f
我们的想法是将您的函数应用于两个不同的术语，然后找到不同之处。这里的“差异”是一个函数列表，如left ∘ right ∘ right（这很脏，但我想可以改进）。现在您可以导航了。然后你再次应用这个函数，但现在每个词都比以前大，所以可以区分它们（这就是 size 函数所做的）。最后，此函数检查是否所有相同的孔都被相同的表达式填充。如果是这样，它会在每个“相同的家庭”中选择随机（实际上是第一个）表达式并将它们收集到一个向量中。
replace' 函数中的其他内容非常简单。将变换函数应用于子表达式向量，并将最终项与原始项进行比较。如果它们是相同的，那么你找到了一个子表达式，它可以像转换函数所说的那样被转换。
现在您需要从一个子项转到所有子项：
replace : (n : ℕ) -> nary n AExp (AExp × AExp) -> AExp -> AExp
replace n f = transform (replace' n f)
这就是改造的全部。证明东西是相当对称的。
sound' : ∀ n f
-> soundnessProof n f
-> ∀ e -> aeval (replace' n f e) ≡ aeval e
sound' n f p e with getSubterms n f e
sound' n f p e | nothing = refl
sound' n f p e | just xs with vecApply n f xs | vecApplyProof p xs
sound' n f p e | just xs | e' , e'' | p' with e ≟AExp e'
sound' n f p e | just xs | .e , e'' | p' | yes refl = p'
sound' n f p e | just xs | e' , e'' | p' | no = refl
唯一的区别——sound' 收到了你的转换函数的健全性证明。
soundnessProof : (n : ℕ) -> nary n AExp (AExp × AExp) -> Set
soundnessProof 0 (e' , e'') = aeval e'' ≡ aeval e'
soundnessProof (suc n) f = ∀ x -> soundnessProof n (f x)
这表示，对于所有参数f 必须返回具有相同“含义”的两个术语的元组。回想一下这个例子：
_==_ : {α β : Level} {A : Set α} {B : Set β} -> A -> B -> A × B
_==_ = _,_
0+-func : AExp -> AExp × AExp
0+-func = λ a2 -> APlus (ANum 0) a2 == a2
vecApplyProof 在值级别是对称的，但在类型级别稍微复杂一些：
vecApplyProof : {n : ℕ} {f : nary n AExp (AExp × AExp)}
-> soundnessProof n f -> (xs : Vec AExp n)
-> uncurry (λ p1 p2 -> aeval p2 ≡ aeval p1) $ vecApply n f xs
vecApplyProof {0} p _ = p
vecApplyProof {suc n} p (x ∷ xs) = vecApplyProof {n} (p x) xs
而且你还需要从一个子表达式移动到所有子表达式：
generalize : ∀ f -> (∀ e -> aeval (f e) ≡ aeval e)
-> (∀ e -> aeval (transform f e) ≡ aeval e)
generalize f p (ANum x) = p (ANum x)
generalize f p (APlus a b) rewrite p (APlus (transform f a) (transform f b))
| generalize f p a | generalize f p b = refl
generalize f p (AMinus a b) rewrite p (AMinus (transform f a) (transform f b))
| generalize f p a | generalize f p b = refl
generalize f p (AMult a b) rewrite p (AMult (transform f a) (transform f b))
| generalize f p a | generalize f p b = refl
sound : (n : ℕ) -> (f : nary n AExp (AExp × AExp))
-> soundnessProof n f
-> (∀ e -> aeval (replace n f e) ≡ aeval e)
sound n f p = generalize _ (sound' n f p)
最后一个例子：
fancy-func : (_ _ _ _ : AExp) -> AExp × AExp
fancy-func = λ a1 a2 b1 b2 -> AMult (APlus a1 a2) (APlus b1 b2) ==
APlus (APlus (APlus (AMult a1 b1) (AMult a1 b2)) (AMult a2 b1)) (AMult a2 b2)
opt-fancy : AExp → AExp
opt-fancy = replace 4 fancy-func
test-opt-fancy :
let a1 = ANum 0
in let a2 = AMinus a1 a1
in let b1 = ANum 1
in let b2 = AMinus b1 b1
in opt-fancy (AMinus (AMult (APlus a1 a2) (APlus b1 b2)) (ANum 0)) ≡
(AMinus (APlus (APlus (APlus (AMult a1 b1) (AMult a1 b2)) (AMult a2 b1)) (AMult a2 b2)) (ANum 0))
test-opt-fancy = refl
fancy-lem : ∀ a1 a2 b1 b2 -> a1 * b1 + a1 * b2 + a2 * b1 + a2 * b2 ≡ (a1 + a2) * (b1 + b2)
fancy-lem = solve
4
(λ a1 a2 b1 b2 → a1 :* b1 :+ a1 :* b2 :+ a2 :* b1 :+ a2 :* b2 := (a1 :+ a2) :* (b1 :+ b2))
refl
where
import Data.Nat.Properties
open Data.Nat.Properties.SemiringSolver
opt-fancy-sound : ∀ e → aeval (opt-fancy e) ≡ aeval e
opt-fancy-sound = sound 4 fancy-func
(λ a1 a2 b1 b2 -> fancy-lem (aeval a1) (aeval a2) (aeval b1) (aeval b2))
整个故事：http://lpaste.net/106670
编辑：directions 函数中的组合策略错误（例如，_∘_ left 而不是λ f -> f ∘ left）。现已修复。