和上一篇一樣，這裡也使用 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)we can obtain Tc and Ts as follows：
⟨sum, rcap⟩ = foldl step (0, ∞) where step (s, y) x = (s + x, (y - x) ↓ x)
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 = {decomposition: ⊛, ⇀, (,) and ↓
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
σ1 = {decomposition (+)
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)
這邊特別標記一下，我在這邊用了一個rule term，
sumcap as ↔ ((fst.sumcap) as, (snd.sumcap) as)。
但是這個rule term其實並沒有出現在任何一個關於Rc,Rs,Rb甚至是R++的論述裡面。
充其量應該只能說這是從semantic equality來的..
這可能要找時間好好想想是怎回事 @@
σ1 = {docomposition: (,) in left hand side
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)
σ1 = {decomposition: (-)
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)
finding out agreements
σ1 = {agreement!
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)
σ1 = {There is no any free variable!!
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)
Tg = (X8,X9) ⊛ (X10,X11) ⇀ (X8 + X10, (X9 - X10) ↓ X11) .
