[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) .