[Notes] FPUG meetup #1

今天去了由 ihower 主辦的 functional programming user group meetup。 會間有兩場講座，一場由大貓主講另一場由godfat主講。

首先，真的很開心有人辦這樣的 meetup。完全讓我想到當年搞的要死要活的 haskell教學讀書會。事實證明在豆腐大學辦的 MTN 除了幫我自己賺到女友一位以外，還真是一點實際價值都沒有。當時搞的要死要活的寫投影片借教室借設備等等，卻沒有真正把 functional p. 推廣得很好。這次的聚會雖說大概不會有機會輪到我上去屁話，但是還是很高興有不少人重視與使用(至少是試圖使用) functional lang.。

幾點小問題：場地空調有點太冷。而且我一直以為會有供餐，就算吃不飽也多少可以擋一餐。事實證明，完全沒有嘛(翻桌)！含我在內光我認識的人就有四個是空著肚子在等放飯。最後是，椅子真的不太好坐，最後實在是腰酸背痛 >"< 嘛，不過這好像都是場地的問題。

實際上我覺得就內容而言，大概只有一個(大)問題。前後兩場的難易程度實在是相差太遠，雖說我大概都聽得懂，但是我相信很多人對第二段的內容完全丈二金剛。一方面應該是兩個主講人對於內容深度下修的程度不一，另一方面確實讓人感覺兩邊沒有協調好。不過，單就難度差來說，也可以就直接當作前半是入門模式，後半是晉級模式。不過這樣的講法對於初次聚會這點來說也有點難以自圓其說就是了。

另外，關於 FLOLAC，godfat 最後結尾附近有件事情說的很好。去 FLOLAC 先聽/看/見聞到很多東西，然後自己慢慢消化就好。某否則太多東西確實平常根本碰觸不到。

順便藉此機會想一下，如果是我上去講我要講什麼題目呢？馬後砲來看，果然開頭還是應該歷史一下，然後就是各種 syntax 介紹還有常見的函數練習。沒錯，就和當初我在豆腐大學做的事情一模一樣。基本沒問題以後才是衝 lambda-calculus 還有 program construction 那些的。希望趕快會有下一場！

[Notes] Semantics, Category and their Implementation 1

此篇為彼篇之後續...

主要涵蓋了 denotational semantics 以及 fixed point iteration。

[Exer] Gray Code in Unfoldr

有點難記
寫在blogger方便記憶好了

seed :: pair of integer
fst seed = decimal number
snd seed = length of gray code

graycode = unfoldr g p
p = (==0) ◦ snd
g = (div ◦ (id × (2^) ◦ (-1)) × (flip (-) ◦ ((+1) × (2^)) × (-1) ◦ snd) ◦ dup) ◦ dup

dup x = (x,x)

實在是長到有點令人厭煩XD
接下來是 unfoldl

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

[Note]Ray Tracing with Haskell using package:parallel

[草記=只是暫時紀錄,整篇會重寫]


這兩天都在弄ray tracing的事情
找了好幾個C/C++版本的code來參考
不過, 幾乎是看沒有懂
最後當然還是決定投靠haskell, XD

找了幾個版本的範例程式
其中一個用gtk作ui
這個版本暫時擱置
因為我gtk一直怪怪的,跑不出東西 Orz

另一個是平行版本

剩下一個是這個和這個

除了gtk那個, 剩下都是直接輸出ppm檔
所以沒有parallel的那兩個都不需要特別題什麼
而且他們也沒有import什麼package進來
簡直就是一整個貼心 XD

parallel那個就囧了
一開始compile一直說 parse error
所以把L49和L5?的兩個"!"給砍了
然後就發現package有問題
所以灌了 AC-vector 1.2.2 和 parallel-2.2.0.1
compile以後, 還是有問題
他說*<>沒定義而且*|重複定義...
弄了好一會兒以後發現
因為原作者是用AC-vector 1.1.1
而AC-vector每次改版都大改... @@
所以又用 ghc-pkg hide AC-Vector-1.2.2
把新版的AC-vector disable掉
一番折騰之後
終於ok了
但是跑一下發現, CPU 只吃了50% @@
所以想說該不會是因為沒有開ghc的選項
所以找了一下以前的資料：
在ghc --make ....... 後面加上一個「-threaded」
然後跑程式的時候加上 +SRT -N2 的選項
e.g. ./ray4-hs 5 50 +RTS -N2 > out.ppm
btw, parallel這個程式需要兩個參數, 遞迴的次數 和 邊長

而David J. King的那個版本則是>./ray 500 > out.ppm
500也是邊長參數

ps - .ppm閱讀 :
有人推薦xv, 不過因為它是x window所以難用
最後我裝了ToyViewer
雖說有一點點鈍鈍的
但是目前還不錯用

[Derivation] Gray Code

這學期的 Computational Intelligence 的第二個作業提到了要用Gray Code來做encoding。雖說我還在考慮整個作業是不是要用Haskell來寫，不過gray code的generator應該蠻好寫的。比起imperative language應該會有個比較乾淨的寫法。

首先，為了先來個直覺的pointwise版。來看一下兩個很簡單的情況：

length = 1 => [[0],[1]]
length = 2 => [[0,0],[0,1],[1,1],[1,0]]

我們可以考慮第二個case是由兩個部份構成[0,0],[0,1] 和 [1,1],[1,0]。很明顯, 前段是把 0 接上 [0],[1]，而後段是把 1 接上 [1],[0]。而"[1],[0]"是"[0],[1]"的inverse！

根據上面的觀察結果
我們可以定義出第一版的gray-pw為

gray-pw 0 = [[]]
gray-pw (n+1) = let hypo = gray-pw n in
    (map (0:) hypo) ++ (map (1:) (reverse hypo))

--
待續 :
1) point-free版本
2) deriving for faster

Strong/Weak

今天決定要把"偷偷愛撫劈"看完
看到一半之處,文中提到了Church-Rosser Theorem

Church-Rosser Theorem:

如果一個expression可以用兩種不同的方法去reduce
而且他們都會得出normal forms
那麼這兩個normal forms就會是一樣的。

不過這個版本的Theorem並沒有說一定要reduce出normal form
也有可能並不存在一個normal form
thus, 並不是每個reduction sequence都會得到normal form
所以我們在原本的Theorem上面加上了strong normalisability

Strong Church-Rosser Theorem:

對一個expression
無論我們用什麼順序去reduce
我們都一定可以得出一個唯一的normal form。

而因為reduction在total function中具有Strong Church-Rosser這樣的性質
所以我們可以很自由的任意決定我們reduction sequence.

也因為total fp有這樣的性質
所以total fp也被稱為 Strong fp
相對的, partial fp就叫做 Weak fp

[Haskell] unit ( )

很早就知道nullary tuple，也就是unit ( )的存在。
不過一直以來都不太清楚那是做什麼的，只隱約知
道type ( )有兩個elements : unit ( ) 和 bottom _|_ 。
雖說大概可以猜說這個unit type是用來描述Relative
Nothing和Absolute Nothing這樣的概念。但是也
一直想不太到實際上這要做什麼。

不過前幾天在書上看到一段在講unit。其中也有舉了
一個簡單的例子。看完以後有種恍然大悟的感覺。

圓周率一般的寫法如下

pi :: Float
pi = 3.14159

這樣當然是正確的，沒什麼不好現在我們加入unit。

pifun :: ( ) -> Float
pifun ( ) = 3.14159

這樣有什麼好處呢？如此一來我們就有一個function
可以用。比起原本的pi，pifun因為是function，所以
我們可以有更大的彈性以及更好的一些性質。例如
說我們現在可以對pifun用compose，而不在只是
把pi當作value餵給另一個function。

(*2).(pifun)
(*2) pi

最後，補充一下有關Absolute Nothing和Relative
Nothing的事情。在Ontology(形上學)中，主要是
以Being(存在)為探討的主題。而相對於Being的概念，
就有了Nothing(無)的概念。後來隨著各代哲學家的研究，
出現了Absolute Nothing(絕對無)和Relative Nothing
(相對無)這兩種略有不同的Nothing。AN是相對Being
的東西，他相當於"完全沒有存在任何東西"。RN則比較
像是欠缺什麼,也有點像是比較不嚴謹的AN。一個顯著
的例子就是 Φ 和 { } 之間的差別：
Φ 是沒有任何東西。
{ } 有一個空的東西。