[Hom] Few exercises of homomorphism - sumcap

這裡我只想專注在CS-generalization上面。所以，為了強調我們不太需要知道sumcap細節上是什麼，這邊故意不去解釋相關的函數。有關steep、rcap和sumcap，請參考 Determining List Steepness in a Homomorphism。

和上一篇一樣，這裡也使用 T 表示 term，同時繼續使用那四種箭頭。

---

根據sumcap的定義(我們不考慮empty-list的情況)：

sumcap [x] = ↔ Tb = (x,x)

For original definition of leftwards(foldr) and rightwards(foldl)：

⟨sum, rcap⟩ = foldr step (0, ∞) where step x (s, y) = (x + s, (x - s) ↓ y)
⟨sum, rcap⟩ = foldl step (0, ∞) where step (s, y) x = (s + x, (y - x) ↓ x)

we can obtain Tc and Ts as follows：

Tc ↔ sumcap (x << xs) = (x + (fst.sumcap xs), (x - (fst.sumcap xs)) ↓ (snd.sumcap xs))
Ts ↔ sumcap (ys >> y) = ((fst.sumcap ys) + y, ((snd.sumcap ys) - y) ↓ y)

Rb is defined as follows：

Rb = { a ↓ a → a }

GO!!!

σ1 = {
X0 ↦ (x,x) ⊛ (sumcap xs) ⇀ (x + (fst.sumcap xs), (x - (fst.sumcap xs)) ↓ (snd.sumcap xs))
}
σ2 = {
X0 ↦ (sumcap ys) ⊛ (y, y) ⇀ ((fst.sumcap ys) + y, ((snd.sumcap xs) - y) ↓ y)
}
Tg = X0

decomposition: ⊛, ⇀, (,) and ↓

σ1 = {
X1 ↦ (x,x)
X2 ↦ (sumcap xs)
X3 ↦ x + (fst.sumcap xs)
X4 ↦ x - (fst.sumcap xs)
X5 ↦ snd.sumcap xs
}
σ2 = {
X1 ↦ (sumcap ys)
X2 ↦ (y,y)
X3 ↦ (fst.sumcap ys) + y
X4 ↦ (snd.sumcap xs) - y
X5 ↦ y
}
Tg = X1 ⊛ X2 ⇀ (X3, X4 ↓ X5)

decomposition (+)
這邊特別標記一下，我在這邊用了一個rule term，
sumcap as ↔ ((fst.sumcap) as, (snd.sumcap) as)。
但是這個rule term其實並沒有出現在任何一個關於Rc,Rs,Rb甚至是R++的論述裡面。
充其量應該只能說這是從semantic equality來的..
這可能要找時間好好想想是怎回事 @@

σ1 = {
X1 ↦ (x,x)
X2 ↦ (sumcap xs)
↦ (fst.sumcap xs, snd.sumcap xs)
X4 ↦ x - (fst.sumcap xs)
X5 ↦ snd.sumcap xs
X6 ↦ x
X7 ↦ fst.sumcap xs
}
σ2 = {
X1 ↦ (sumcap ys)
↦ (fst.sumcap ys, snd.sumcap ys)
X2 ↦ (y,y)
X4 ↦ (snd.sumcap xs) - y
X5 ↦ y
X6 ↦ fst.sumcap ys
X7 ↦ y
}
Tg = X1 ⊛ X2 ⇀ (X6 + X7, X4 ↓ X5)

docomposition: (,) in left hand side

σ1 = {
X4 ↦ x - (fst.sumcap xs)
X5 ↦ snd.sumcap xs
X6 ↦ x
X7 ↦ fst.sumcap xs
X8 ↦ x
X9 ↦ x
X10 ↦ fst.sumcap xs
X11 ↦ snd.sumcap xs
}
σ2 = {
X4 ↦ (snd.sumcap ys) - y
X5 ↦ y
X6 ↦ fst.sumcap ys
X7 ↦ y
X8 ↦ fst.sumcap ys
X9 ↦ snd.sumcap ys
X10 ↦ y
X11 ↦ y
}
Tg = (X8,X9) ⊛ (X10,X11) ⇀ (X6 + X7, X4 ↓ X5)

decomposition: (-)
finding out agreements

σ1 = {
X5 ↦ snd.sumcap xs (agree with X11)
X6 ↦ x (agree with X8)
X7 ↦ fst.sumcap xs (agree with X10)
X8 ↦ x
X9 ↦ x
X10 ↦ fst.sumcap xs
X11 ↦ snd.sumcap xs
X12 ↦ x (agree with X9)
X13 ↦ fst.sumcap xs (agree with X10)
}
σ2 = {
X5 ↦ y (agree with X11)
X6 ↦ fst.sumcap ys (agree with X8)
X7 ↦ y (agree with X10)
X8 ↦ fst.sumcap ys
X9 ↦ snd.sumcap ys
X10 ↦ y
X11 ↦ y
X12 ↦ snd.sumcap ys (agree with X9)
X13 ↦ y (agree with X10)
}
Tg = (X8,X9) ⊛ (X10,X11) ⇀ (X6 + X7, (X12 - X13) ↓ X5)

agreement!

σ1 = {
X8 ↦ x
X9 ↦ x
X10 ↦ fst.sumcap xs
X11 ↦ snd.sumcap xs
}
σ2 = {
X8 ↦ fst.sumcap ys
X9 ↦ snd.sumcap ys
X10 ↦ y
X11 ↦ y
}
Tg = (X8,X9) ⊛ (X10,X11) ⇀ (X8 + X10, (X9 - X10) ↓ X11)

There is no any free variable!!
Tg = (X8,X9) ⊛ (X10,X11) ⇀ (X8 + X10, (X9 - X10) ↓ X11) .

[Hom] Few exercises of homomorphism - max and scanr

為了方便, 下面用 T 表示 term，

Tb = base term
Tc = cons term
Ts = snoc term
Tg = generator term

箭頭方面，

↦ : variable-term binding
↔ : conversion relation
→ : rewriting relation
⇀ : some "arrow" operator
(for example, ⇀ could be ↔ or →)

另外，也使用下面的一些 function

(<<) : cons
(>>) : snoc
(↑) : max
(↓) : min

---

example 01 - max

Step 1 - To find out the base, cons and snoc term

max [a] ↔ Tb = a
Tc = x ↑ (max xs) ↔ Tb ⊛ (max xs) = x ⊛ (max xs)
Ts = (max ys) ↑ y ↔ (max ys) ⊛ Tb' = (max ys) ⊛ y

Step 2 - To find out base rule term, Rb
這個case因為用不到，剛好免了。

Step 3 - Initializing substitutions and generator term

σ1 = {X0 ↦ x ↑ (max xs) ⇀ x ⊛ (max xs)}
σ2 = {X0 ↦ (max ys) ↑ y ⇀ (max ys) ⊛ y}
Tg = X0

其實這邊看也看得出來 ⊛ 就是 ↑
不過我還是套了三次 decomposition (for ↔, ⊛ and ↑)
還有兩次的 agreement (x=x且max ys=max ys; max xs = max xs且y=y)
最後就會得到 Tg = x3 ⊛ x4 ⇀ x3 ↑ x4 .

---

example 02 - scanr

For simply, there fix the higher-order function argument of scanr, i.e. scr = scanr ⊕, mp a xs = map (⊕ a) xs.

Step 1 - To find out the base, cons and snoc term

For given definitions

scr (x << xs) = (x ⊕ (head (scr xs))) << (scr xs)
scr (ys >> y) = (mp y (scr ys)) >> y

we can obtain following rule terms:

scr [a] ↔ Tb = [a]
[x] ⊛ (scr xs) ↔ Tc = [x ⊕ (head (scr xs))] ++ (scr xs)
(scr ys) ⊛ [y] ↔ Ts = (mp y (scr ys)) ++ [y]

Step 2 - To find out base rule term, Rb

Rb = {
mp a [b] → [a ⊕ b]
head [a] → a
}

Step 3 - Initializing substitutions and generator term, and, run!!

σ1 = {X0 ↦ [x] ⊛ (scr xs) ⇀ [x ⊕ (head (scr xs))] ++ (scr xs)}
σ2 = {X0 ↦ (scr ys) ⊛ [y] ⇀ (mp y (scr ys)) ++ [y]}
Tg = X0

decomposition: ⊛, ⇀ and (++)

σ1 = {
X1 ↦ [x]
X2 ↦ (scr xs)
X3 ↦ [x ⊕ (head (scr xs))]
X4 ↦ (scr xs)
}
σ2 = {
X1 ↦ (scr ys)
X2 ↦ [y]
X3 ↦ (mp y (scr ys))
X4 ↦ [y]
}
Tg = X1 ⊛ X2 ⇀ X3 ++ X4

agreement: X4-X2

σ1 = {
X1 ↦ [x]
X2 ↦ (scr xs)
X3 ↦ [x ⊕ (head (scr xs))]
}
σ2 = {
X1 ↦ (scr ys)
X2 ↦ [y]
X3 ↦ (mp y (scr ys))
}
Tg = X1 ⊛ X2 ⇀ X3 ++ X2

decomposition: mp

σ1 = {
X1 ↦ [x]
X2 ↦ (scr xs)
X3 ↦ [x ⊕ (head (scr xs))] ↦ mp (head (scr xs)) [x] {by "mp a [b] → [a ⊕ b]"}
X4 ↦ head (scr xs)
X5 ↦ [x]
}
σ2 = {
X1 ↦ (scr ys)
X2 ↦ [y]
X3 ↦ (mp y (scr ys))
X4 ↦ y
X5 ↦ (scr ys)
}
Tg = X1 ⊛ X2 ⇀ (mp X4 X5) ++ X2

agreement: X5-X1

σ1 = {
X1 ↦ [x]
X2 ↦ (scr xs)
X4 ↦ head (scr xs)
}
σ2 = {
X1 ↦ (scr ys)
X2 ↦ [y]
X4 ↦ y ↦ head [y]
}
Tg = X1 ⊛ X2 ⇀ (mp X4 X1) ++ X2

decomposition: head

σ1 = {
X1 ↦ [x]
X2 ↦ (scr xs)
X4 ↦ (scr xs)
}
σ2 = {
X1 ↦ (scr ys)
X2 ↦ [y]
X4 ↦ [y]
}
Tg = X1 ⊛ X2 ⇀ (mp (head X4) X1) ++ X2

agreement: X4-X2

σ1 = {
X1 ↦ [x]
X2 ↦ (scr xs)
}
σ2 = {
X1 ↦ (scr ys)
X2 ↦ [y]
}
Tg = X1 ⊛ X2 ⇀ (mp (head X2) X1) ++ X2

There is no any free variable!!
Tg = X1 ⊛ X2 ⇀ (mp (head X2) X1) ++ X2 .

---

這兩個例子中，做 CS-generalization 的過程確實相當的機械化。任何需要的 term rewriting 都是直接套用Rb裡面的就好。
另外，過程中我發現幾個hint：

1. 一旦產生出 ⇀ 之後，一概都以右手邊的free variable優先處理
2. 需要term rewriting時，都是在Rb裡面找到一個合適的rule term。並且，很多時候都是先從rule term的右手邊去match一個合適的。
3. 做decomposition的時候不要太貪心，有時候會因為一次decompose太多root function，而使的某一個free varable錯過一個好的binding時機。
4. term rewriting會很直接的影響到agreement。例如說scanr的例子，[x ⊕ (head (scr xs))]要寫成mp (⊕ x) [head (scr xs)]還是mp (⊕ (head (scr xs))) [x]，這會對後面造成很大的影響。而且這又取決於⊕是不是commutative之類的前提/假設。另外，在sumcap的例子裡面(請參考下一篇)，對(+)做decomposition的過程中，要不要把 a+b 換成 b+a 也會是個需要都嘗試看看的部份。因為和mp的情況一樣，有可能需要交換一下順序才做的下去，也有可能不交換才可以，當然也可能不管怎樣都可以做下去。所以，我想這裡是個比較難說「不需要人的輔助」的部份。