[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的情況一樣，有可能需要交換一下順序才做的下去，也有可能不交換才可以，當然也可能不管怎樣都可以做下去。所以，我想這裡是個比較難說「不需要人的輔助」的部份。