[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

Type of de Burjin index

好亂,整理成一篇文章好了
順便釐清看看

前言一下
list A ::= [] | list A : a.
且, 用 list 表示 context: Γ.

首先,來看幾個case

λ.0 : [] ; a -> a
λλ.0 : [] ; a -> b -> b
λλ.1 : [] ; a -> b -> a
λλλ.2 : [] ; a -> b -> c -> a

然後根據某條rule

λ_ : Term (G,T) T' -> Term G (T -> T')

就變成了

0 : [a] ; a
λ.0 : [a] ; b -> b
λ.1 : [a] ; b -> a
λλ.2 : [a] ; b -> c -> a

後三個case可以再來一次

0 : [a,b] ; b
1 : [a,b] ; a
λ.2 : [a,b] ; c -> a

最後一個case還可以更進一步

2 : [a,b,c] ; a

結論
確實,不管有幾層λ-binder
如果是取 zero
那就是直接取出context最後進來的
如果是取 suc zero
就是往後數一個
取 suc suc zero
則再往後取一個

--
明白以後..
突然覺得這兩三天的時間...
實在是花得很浪費= =

Desktop

因為聽到學校在用Verilog
所以突然對Verilog和Lava重新燃起興趣

到處找找資料以後
發現還是要在windows上才方便使用
所以只好整理一下我可憐的那台vista
今年總統大選那時
為了看網路電視,整個被我搞得亂七八糟...囧

重整了一下
新灌了MSYS和nmake兩個工具
GHC本來就有
Lava正在抓
Xilinx ISE正在灌(4G,囧)

不過話又說回來
HDL我根本不會用呀~~ XD