Поскольку нам не нужны доказательства для 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). Исправлено сейчас.
person
user3237465
schedule
30.06.2014
