[Note] R and Statistical analysis

[0] 裝/用 Package

> install.packages("package_name")
> library("package_name")

[1] 信度分析

現在是用這個套件
http://personality-project.org/r/html/alpha.html
裡面包含 Cronbach's alpha 和 Guttman's lambda 6

> library(psych)
> alpha(data_frame)

-----
還有這個也可以算 alpha
http://rss.acs.unt.edu/Rdoc/library/ltm/html/cronbach.alpha.html
但是沒有用過

[2]效度分析

靠北複雜，跳過

[3]相關分析

內建的 cor() 就很夠用了
http://www.statmethods.net/stats/correlations.html

> cor(data_frame)

或

> cor(data_frame), method="method_name")

[4] 結果輸出

> write.table(mydata, "file_name")

> library(xlsx)
> write.xlsx(mydata, "file_name")

[5] counting

計數

> table(sort(mydata$column_title))

*to be continued*

Notes on notes

最近想要找一個好的軟體來作筆記： lyx 寫起來太綁手綁腳、 quicknote 會突然掉進死亡螺旋然後把我的資源吃光光、 textmate 的 unicode 簡直是悲劇一場，最後還是裝了 Evernote 。

Evernote 用了幾個禮拜，大體上都還不錯。但是他的排版我實在是不太喜歡，非常非常有純文字的感覺，視覺上真的不太好看。我自己的習慣是用類似 markdown 的方法去編輯/排版所以我後來裝了 Mou 來作為 evernote 的編輯器，(也就是每次都從 evernote 複製到 mou 去編輯然後再貼回去儲存)。不過這樣弄實在是又蠢又麻煩，所以最後跑去 bitbucket 開個 repository 然後直接跳過 evernote 的複製-貼上-同步的愚蠢步驟。目前為止一切還算不錯！

[Note] Infographics and Fonts

看到一系列關於 infographics 的文章，覺得相當值得看一下，考慮說要放在這邊還是另一個 blog ，最後想說「和資訊相關的東西所以還是放這裡好了」。

Infographics 就是現在在雜誌或是一些網站上常常看到的那種豐富圖表。通常是一個不太複雜的圖，但是可以同時表現出若干個重點和足夠的資訊量。對於視覺效果和產生直覺來說都非常的適合。例如說這張圖：


inSide 有關於這個主題的幾篇文章。這篇 就是個不錯的範例，裡面講到了一些基本概念和方便的工具。

另外也有這系列的 Infographics 教學 可以看，裡面包含了：

• 介紹 
• 排版 
• 配色 
• 字型  
• 素材 
• 製作軟體

同一個 blog ，裡面還有兩篇文章是關於 typefaces 和 fonts 的。寫得蠻清楚的，紀錄一下以後可以來學一下。畢竟這樣是「永遠沒真正學起來的痛」之一。

• 字型字體，傻傻分不清楚 
• 字型的基本構造 
• 推薦的10個字型

同場加映，同網誌還有每月推薦字型。

[wiki]dokuwiki gitit

最近在弄 flolac12 的網站
照慣例是用 dokuwiki 在架
說是說方便啦
不過好像還是有點瑣碎

重點是, php 真是討厭 orz

找了一下發現
http://gitit.net/

雖說圖樣是呆板了點
但是似乎編輯起來非常方便

[temp] 一堆還沒看的網頁

[agda 教學]
http://www.cs.nott.ac.uk/~txa/g53cfr/
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Modules
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Records

[types in agda]

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.SimpleInductiveTypes

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ParameterizedInductiveTypes

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.UniversePolymorphism

[category]
http://www.haskell.org/haskellwiki/Category_theory
http://en.wikibooks.org/wiki/Haskell/Category_theory

[monad]
http://www.haskell.org/haskellwiki/Category_theory/Monads
http://en.wikibooks.org/wiki/Haskell/Understanding_monads

[monad transformer]
http://en.wikibooks.org/wiki/Haskell/Monad_transformers
http://conway.rutgers.edu/~ccshan/wiki/blog/posts/Monad_transformers/
http://www.randomhacks.net/articles/2007/03/05/three-things-i-dont-understand-about-monads
https://github.com/copumpkin/categories/

[Notes] Semantics, Category and their Implementation 1

此篇為彼篇之後續...

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

[Notes] Domain and Fixed Point

此篇大量參考 FLOLAC 08' 的 Denotational Semantics 講義。

A poset(partially ordered set) is a set D with a binary relation ⊑ s.t. the following properties hold:

1. reflexive: x ⊑ x 
2. anti-symmetric: x ⊑ y and y ⊑ x -> x ≡ y 
3. transitive: x ⊑ y and y ⊑ z -> x ⊑ z 

For a poset D, a set X ⊆ D is directed if:

1. X ≠ { } 
2. ∀ x,y ∈ X, ∃ z ∈ X s.t. x ⊑ z and y ⊑ z 

For a poset D, D is a cpo(complete partial order) if:

1. ∃ ⊥ ∈ D s.t. ∀ x ∈ X, ⊥ ⊑ x
2. Every directed set X ⊆ D has a least upper bound denoted as ⨆X

A cpo D is called domain as well.

---

Let D be a poset with ⊑ and f be a total function from D to D.

• x ∈ D is a fixed point of f iff f x = x
• x ∈ D is a least fixed point of f iff x is a fixed point of f and for every fixed point y of f, x ⊑ y.

**The Least Fixed Point Theorem**

Let D be a domain.

• ∀ f : D -> D, ∃ a least fixed point 
• ∃ fix : (D -> D) -> D, s.t. ∀ f : D -> D, fix f is the least fixed point of f.

For a function f : (D -> D), we can define a directed set Xf ⊆ D by

• Xf = {⊥,f ⊥,ff ⊥,fff ⊥,...}.

By the continuity of f,

f ⨆Xf
= f ⨆{⊥, f ⊥, ff ⊥, fff ⊥, ...}
= ⨆f{Xf}
= ⨆f{⊥, f ⊥, ff ⊥, fff ⊥, ...}
= ⨆{⊥, f ⊥, ff ⊥, fff ⊥, ...}
= ⨆Xf.

Thus, for any function f : D -> D, there exist a fixed point ⨆Xf of f. For least, we can support x is a fixed point as well. Then

⊥ ⊑ x,
f ⊥ ⊑ f x,
ff ⊥ ⊑ ff x,
...
fn ⊥ ⊑ fn x, (we write fn for applying f n times)
...

Because x is a fixed point of f, fd x will be x obviously. Collecting both sides as set we will obtain

{⊥,f ⊥,ff ⊥,fff ⊥,...} and {x},

then taking least upper bound of both set, 

⨆Xf ⊑ x

Thus, for any function f : D -> D, there exist a least fixed point ⨆Xf of f. Finally, we can define fix by 

fix f = ⨆Xf

for any function f : D -> D.

---

Relevance to (denotational) semantics:

The semantics of program g is a function g. For example, a program can be defined as follow:

g args = h (g args') : A -> B

This is not a simple case that we can find a corresponding g easily. However we can define another program/function f/f that can help us to define g. For example, we define

f : (A -> B) -> (A -> B),
f g = \args -> h (g args') = g.

Obviously, g is the least fixed point of f and the ⨆Xf as well. In this case, the domain D = (A -> B).

[Note] about reduction and normal form

[Redex]

我們知道，可以繼續簡化的 term 叫做 redex (reducible expression, reducible subterm)。
例如說

(λx.x+1) 10
(λxλy.x*y) 1
square (square 5)
1+4*5

[Reduction Strategies]

對一個 redex 我們可以優先從最裡面(innermost)或是最外面(outermost)來做拆解。兩種不同的方式即稱為 innermost reduction 和 outmost reduction。另一種解釋是： innermost reduction 會一直挑 innermost redex (不包含任何 redex 的 redex )來簡化，而outermost reduction 則相對會一直去選 outermost redex (不被任何 redex 包含的 redex)來簡化。

fst (square 10, root 100) -- outermost reduction
=> square 10
=> 100

fst (square 10, root 100) -- innermost reduction
=> fst (100, root 100)
=> fst (100, 10)
=> 100

[Non-strict and Lazy]

Non-strict reduction(evaluation) 是指只有在出現必須簡化(運算)的情況才去簡化(運算)。non-strict 是一種抽象的性質，實際上存在有若干種不同的實作方式：

<1> Normal order reduction
即是 outermost + leftmost。

(λx.x (λy.id y)) (λzw.fst (z,w))
=> (λzw.fst (z,w)) (λy.id y))
=> (λw.fst ((λy.id y),w))
=> (λy.id y)
=> (λy.y)

<2> call-by-name
基本上 call by name 關鍵的概念在於將 arguments 直接貼入 function body 而沒有任何先行運算這件事情上。(相對於 call by value 會先算好 arguments 再放到 function 中) 也就是說 call by name 是將 arguments 以 capture-avoiding substitution 的方式直接貼進 function body，等到非要算不可才去開始計算那些 copies。這些 argument 的 copies 被稱為 thunk，一個"尚未被運算的值加上如何運算它的描述"。

(λx.x (λy.id y)) (λzλw.fst (z,w))
=> (λzλw.fst (z,w)) (λy.id y))
=> (λw.fst ((λy.id y),w))

不過 call by name 也有個缺點：如果 argument 被用到不只一次，就會因為同一個 argument 被貼了很多份 thunks，所以變成要重複計算這些 thunks 的值。也因此，以這種方式做出來的 non-strict evaluation 在效率上會比較慢一些。

P.S.
從 evaluation 的角度來看，normal order 和 call by name 之間的一個差別在於：normal order 比 call by name 還要貪心一點：call by name 如果碰上一個 λ-abstraction (尚未拿到 arguments 的 function) 就不會去 reduce。但是 normal order 還是會試圖多做幾步。

(λfλg.f g) (λx.id x) (λx.x+2*3-5)
=> (λx.id x) (λx.x+2*3-5)
=> id (λx.x+2*3-5)
=> (λx.x+2*3-5) -- call by name will stop here! and, view this term as a normal form (..weak head normal form?)
=> (λx.x+1) -- only normal order will achieve here! this is a "real" normal form

所以另外有種說法是說：call by name 是 "normal order" + "停在 λ-abstraction 時"。

<3> call-by-need
是 call-by-name 的變體：原本 call-by-name 中 arguments 的 re-evaluation 不會發生。也就是說，所有會用到的 arguments 都只有第一次被使用的時候會被算一次。也因此 reduction 不是以 tree 的方式在進行，而是以 (directed) graph 的方式在處理。

call-by-need 即是一般所謂的 lazy evaluation。也就是說 lazy 是 non-strict 的一個實作。

[Normal Form]

而一個 term 如果不包含任何 redex，則被稱為 normal form。換句話說， normal form 就是一個無法再套用任何 reduction rule 來簡化的 term。

(λx.x+1) 10 => 10+1 => 11
(λxλy.x*y) 1 => λy.1*y
square (square 5) => square 25 => 625
1+4*5 => 1+20 => 21

[β-Reduction/Redex/NF]

在 λ-caululus 中我們用 β-reduction 來描述 application 的概念，也就是說，我們用

(λx.t) u =β t[u/x]

來描述「將 t 中出現的 x 都以 u 來取代」。

而，一個可以套用 β-eduction 的 redex 稱為 β-redex。換個說法就是：一個具有

(λx.t) u

這種長相的 term。

如果一個 term 不能再做任何的 β-reduction，則稱為 β-normal form。

[η-Conversion/Redex/NF]

Extensionality (extensional equality) - 如果兩個 function 對所有相同 input 都會產出一樣的 result。而在 λ-caululus 中我們用 η-conversion 來描述這個性質如下

(λx.t) x =η t , if x ∉ FV(t)

與 β-reduction 同樣地, 也有 η-redex 以及 η-normal form 的存在。更甚者，還有 βη-reduction 以及 βη-normal form 等等。

[Head Normal Form]

如果在一個 term 的最外層既不是 redex 也不是一個 reducible λ-abstraction，則此 term 被稱為一個 head normal form。換句話說，一個 head normal form 的 top-level 必定是

• 變數 (variable)
• 數值 (data value)
• 參數不足的內建函數 (build-in function applied to too few arguments)
• 不可簡化的 λ 函數 (lambda abstraction whose body is not reducible)

例如說

• x
• 11
• zipWith (*)
• (λxλy.x+y) (10)
• (λxλy.x+y) (length [1..10]) -- HNF 中的 argument 可以是 redex, 但是 normal form 不行
• (λx.id x) (λy.sum y) -- Not a HNF, because (λx.id x) could be reduced to (λx.x)

[Weak Head Normal Form]

weak head normal form 是 head normal form 或者 top-level 處是任何的 λ-abstraction。換個說法，weak head normal form 就是「把對 λ-abstraction 的限制拔掉的 head normal form」。

• (λxλy.x+y) (length [1..10])
• (λx.id x) (λy.sum y) -- in WHNF but not HNF

[Normalization Properties]

若一個 rewriting system 中所有 term 不管經由哪種 sequence of rewrites 都會產生出 normal form，則該系統被認為具有 strong normalization property。相對地，如果所有的 term 至少存在有一個 sequence of rewrites 可以產生出 normal form，則稱為 weak normalization property。例如

fst (square 10, length [1..])
=> square 10
=> 100

和

fst (square 10, length [1..])
=> fst (100, length [1..])
=> fst (100, 1+length [2..])
=> fst (100, 1+1+length [3..])
=> ...

只有第一種 reduction 會產生出 normal form，第二種則不會。所以這個 system 一定只具有 weak normalization property。

有趣的是，pure untyped λ-calculus 既沒有 strong 也沒有 weak normalization property。因為在 pure untyped λ-calculus 裡面我們可以寫出類似

(λx.xx)(λx.xx)

這樣的 term。而這種 term 不會 terminates，所以不會存在一個 normal form。
但是某些 typed λ-calculus 就具有 strong normalization property，例如說 simply typed λ-calculus 和 System F。換句話說這些 system 保證上面所有寫出來的 term 都會 terminates。

-- 後記 --
這篇前前後後斷斷續續寫了應該快三天吧
期間一直被事情打斷
不然就是因為一堆名詞問題卡住
然後開始無限翻書地獄
終於大概寫完了
還不知道有多少混淆和錯誤呢

[mac] The "gettext"

Mac OS X provide a BSD-gettext. When I build some software needed GNU-gettext, however, I will need to install a GNU-gettext by, for example, homebrew. But, because system gets confused if both are in the library path, the homebrew will NOT symlink GNU-gettext to /usr/local .

Due to the reason showed above, I have to add path by myself when I build some software by myself. e.g.

LDFLAGS="$LDFLAGS /usr/local/Cellar/gettext/0.18.1.1/lib"
CPPFLAGS="$CPPFLAGS /usr/local/Cellar/gettext/0.18.1.1/include"

[android] Install and HelloAndroid Step by Step

[3-1] Selecting packages to install

1. install via homebrew
> brew install android-sdk

2. initialization about Android SDK and AVD.
> android

3. setup the SDK and AVD management.

3-1. switch to "Available" page to select packages you want to install, click button:"install selected"

3-2. switch to "Installed" page to update packages by click button:"Update All..."

[3-2] Updating packages

[3-3] "Virtual devices" page

[3-3] new AVD window

3-3. To create a new AVD(Android Virtual Devices): switching to "Virtual Devices" page and clicking button:"new".
(Picture - [3-3] "Virtual devices" page)

On the popped window, we could decide what properties of AVD we want. Select your target carefully, and, remember which target version you select.
(Picture - [3-3] new AVD window)

After clicking button:"Create AVD", this AVD will be showed on the AVD list. now, select a AVD you want to run and click button:"start". There will pop a "Launch Option" window, you could just clicking the button:"Launch".
(Picture - [3-3] "Virtual devices" page)

4. After Init. of Android opening, you could see a nice look.

[4] AVD with waiting for turn-on

[4] readied screen

5. Create hello world project via native example.
Do NOT close the AVD. switch to console:
> android create project --package com.example.helloandroid --activity HelloAndroid --target target id --path project-path

Hint: the target id have to be matched with the AVD that we are running. To query the id of target:
> android list targets

for example, the target name of my AVD is Android 2.2, and, in the result of query, I could find out that "id: 4" matches what I need.

...skipped..
id: 4 or "android-8"
Name: Android 2.2
Type: Platform
API level: 8
Revision: 2
Skins: HVGA, QVGA, WQVGA400, WQVGA432, WVGA800 (default), WVGA854
...skipped..

now, my creating command will be
> android create project --package com.example.helloandroid --activity HelloAndroid --target 4 --path ~/haha

6. compiling and installing
> cd where-your-project-is
> ant install
wait a few seconds, you should see something like

...skipped...
BUILD SUCCESSFUL
Total time: 9 seconds

7. switch to AVD, you will find out the HelloAndroid app:

---

竟然寫了兩個小時.. 囧>
godfat大大, 夠詳細了..吧？ XD

[筆記]Haskell X Fractal

想做Fractal
但是仔細想想
Parallel Haskell不柔
Fractal沒真的仔細看過
GUI(現在只有wxHaskell可以選)只跑過demo
慘絕人寰之餘
紀錄一下還沒時間看的網頁吧

http://haskell.org/haskellwiki/WxHaskell/Quickstart#Painting

http://gregheartsfield.com/fractal-hs/

http://hackage.haskell.org/packages/archive/haskore/0.1.0.4/doc/html/src/Haskore-Example-Fractal.html

http://boson4.phys.tku.edu.tw/high_school/unit_fractals.htm

http://classes.yale.edu/Fractals/MandelSet/MandelDef/Definition/Definition.html

http://en.wikipedia.org/wiki/Mandelbrot_set

[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
雖說有一點點鈍鈍的
但是目前還不錯用

[Temp]Parallel Functional Programming

http://www.mathematik.uni-marburg.de/~eden/
資料蠻多的
值得一試

[AI]Learning categories in neural network

今天終於釐清了兩年前遇到的問題：程式在做參數式學習的時候都會需要根據已知的情況去調整參數向量，但是應該要「看完整本書在學起來？」還是「看完一段就學一次？」這一直是當時在實作Perceptron的時候卡到的小疑惑。不過那時候不是很熟悉整個情況，所以也說不出個很顯著的所以然來。最後是根據給定的演算法去做。

今天又遇到這個問題了，不過這次有比較清楚的腦海地圖了。

舉個例子來解釋：假設今天某個classify system吃3個參數作為input，所以該system應該具有一個weight vector長做這樣：

並且我們有三個classified instance：




而每一次W(weight vector)乘上(inner product)其中一個X(input instance(again, it is a vector))然後產生一個O(output)，並且我們已知該instance X具有一個正確的結果T。根據某個函數f(T-O), 我們可以得到∆W：「W目前應該更新的程度值」。舉例如下：

這表示產生出來的∆W的意思是「僅需要更新bias值」。

但是這裡就有個問題了，因為大多的learning model都會需要一再的對整個instance space去做運算。所以到底是每看完一筆instance就更新？

還是看完整個instance space以後再去更新？


前面這種稱為針對資料做逐一學習的方法稱為：Incremental Learning，而相對地，對全部資料作一次性的學習稱為：Batch Learning。

另Batch Learning a.k.a. Epoch Learning。
而Incremental Learning則又被稱為
1. Pattern Learning
2. Instantaneous Learning

不過Pattern Learning會容易和Pattern Recognition產生混淆，而Instantaneous Learning容易造成「以為learning的行為是instantaneously」的誤會。所以兩者現在都已經不常使用了。

[reStructuredText] Pygments Intro. & Install

參考了劍心的這篇，也弄了pygments來用用看。

不過我不是用port install來裝。原因不明地，> sudo port install py26-pygments以後，不知道怎麼打開它。@@
> pygmentize
> pygments
> py-pygments
> py26-pygments
等等的排列組合都試過了，但是就是不能用。
不知道是哪個地方跳針了還是如何? @@
最後解決的方法是去PyPI下載source code以後自己build就可以用了。(我的python版本=2.5.1)
> wget 'http://pypi.python.org/packages/source/P/Pygments/Pygments-1.2.2.tar.gz#md5=920e706a817437eae3a1406380421a3d'
> tar -xzf Pygments-1.2.2.tar.gz
> cd Pygments-1.2.2
> sudo python setup.py install

---

pygments有四個重要的元件：Lexers, Formatters, Filters和Styles。Lexers是source code parser；Formatters是output generator；Filters是針對特別需求時可以更改部份輸出結果用的工具；Styles是色彩字體等格式的定義。詳情可以參考Pygments Online Document中的Builtin components的部份。

(註：要使用有關圖檔的formatter都需要安裝PIL(Python Image Library)。build的方法幾乎和build pygments一模一樣。只是wget的target要換一下罷了。
> wget http://effbot.org/downloads/Imaging-1.1.7.tar.gz
> tar -xf Imaging-1.1.7.tar
> cd Imaging-1.1.7
> sudo python setup.py install )

(註：在Mac上，style的定義檔存放在/Library/Python/2.5/site-packages/Pygments-1.2.2-py2.5.egg/pygments/styles/這裡面。劍心的twilight.py我就是直接賽進這邊就可以用了。)

---

pygmentize身上也有非常多參數可以下。最基本的兩個flag分別是-f和-o。-f 可以指定要使用的formatter(也就是指定輸出格式)；-o 則是和一般compiler一樣指定輸出檔名。當然，因為formatter本身就包含了format在內，所以也可以不要用-o，不過這樣一來就要自己做檔案輸出。以下兩個作法是等價的。
> pygmentize -f html -o setup_c.html setup.c
> pygmentize -f html setup.c > setup_c.html

-O可以進一步設定lexer和formatter的選項。-O可以一次接受複數個選項，但是這也造成了-O不能接受含有","或"="的選項。因此也就有了-P的出現，-P一次只能吃一個選項參數，但是選項參數中就可以包含","或"="。
> pygmentize -f html -O full,style=twilight,linenos=1 01.hs
> pygmentize -f html -P "heading=Pygments, the Python highlighter" full,linenos=1 setup.py
相似於-O和-P, -F是用來在token stream上面增加filter用的。用法大概是這樣-F keywordcase:case=upper,whitespace:spaces=True、-F whitespace:spaces=True。
(註，這三個參數都可以重複一直使用。)

pygmentize預設只會生出資訊而不會把style的定義也一併輸出，也就是說，
> pygmentize -f html setup.py > test.html
用browser打開test.html以後會發現是黑白的。
因此我們可以用
> pygmentize -f html -S twilight -a .pygments > style.css
來取得名為twilight的style的css檔

還有, 參數-N可以查詢某source code的lexer。
例如說> pygmentize -N Makefile會輸出make。

此外pygmentize也提供兩個flag, -L和-H, 可以查詢lexers, formatters和filters的資訊(-L還可以查詢styles)。例如
> pygmentize -L會傾印lexers, formatters, filters和styles的資訊
> pygmentize -L styles會指定印出styles的資訊
> pygmentize -H formatter html會印出html的help info.

---

這是測試的結果(原因不明的在blogger上面Line#和Code會有點錯開)

1 2 3 4 5 6 7 8 9 10 11

import GHC.Conc import System.Info import Text.Printf import Data.Version main = do printf "Compiled with %s-%s on %s/%s\n" compilerName (showVersion compilerVersion) os arch printf "Running with %d OS threads\n" numCapabilities

[OS] Taste of House

今天早上google了一下發現已經有人拿haskell來寫OS了，叫做House。其細節還沒細看，不過倒是抓下來試了一下。測試的環境基本上和這篇是一樣的。

首先在House的網站上載 hOp-x.y.flp 然後暴力把.flp給改成.img，接著就直接用VirtualBox去掛載這個映像檔到flppy device上面去，然後開機就可以了。

開機以後會進入GRUB的選單，接著就看想要進text mode還是graphics mode就好。

graphics mode大概長這樣，非常明顯這只是一個展示用的範例。這裡只提供了一些固定的功能可以稍微玩玩看。我甚至連怎麼關機或是離開都不知道。XD



這裡還發現一篇paper: A Principled Approach to Operating System Construction in Haskell (ICFP 2005)。最近如果沒有其他壓力的話，蠻想來研究看看這怎麼做的。

[OS] DIY of Operating System

昨天晚上睡覺前一時興起翻了翻之前買的OS DIY的書
前兩章非常簡單, 都是在做介紹和環境配置
不過它書上是在Windows上跑
而我是用Mac OS X, 其間工具等等差異也就不用我贅述。

基本上我最後用到的工具目前只有作為Virtual Machine的VirtualBox, 和十六進位編輯器Hex Fiend還有assemblerNASM。

第一個測試很簡單，只是去寫一個Boot Sector。

首先把單純的程式碼打一打。

      org 07c00h
      mov ax, cs
      mov ds, ax
      mov es, ax
      call DispStr
      jmp $
  DispStr:
      mov ax, BootMessage
      mov bp, ax
      mov cx, 16
      mov ax, 01301h
      mov bx, 000ch
      mov dl, 0
      int 10h
      ret
  BootMessage:   db "Hello World"
  times  510-($-$$) db 0
  
  dw  0xaa55

然後assemble一下：> nasm boot.asm -o boot.bin。
接者打開Hex Fiend把boot.bin打開，另存新檔成xxx.img

然後打開VirtualBox去新開一個Virtual Machine，接著再把剛剛的xxx.img給mount到Storage > Floppy Controller > Floppy Device 0上面去。最後再打開這台virtual machine就可以看到如下成果：

[Beamer+CJK]Chinese Slides

因為學校需要，所以研究了一下如何在beamer中顯示中文問題。

本來是想用XeLatex+beamer去跑，不過它一直和我說某某東西找不到，google了一下, 發現要解決那個似乎是個大工程。所以後來就改看看CJK+beamer方不方便。結果出乎意料的，還算方便的順利生出中文投影片來了。

不過就是字體有點醜，不過因為太趕了，也就沒有去研究怎麼裝好看一點的字體。

---

貼上兩張圖片以茲證明：

---

最後，附上prototype一份:

\documentclass[CJKutf8]{beamer}
\usepackage{CJKutf8}
\usetheme{Warsaw}
%\usetheme{JuanLesPins}
%\usetheme{Malmoe}
%\usetheme{PaloAlto}
%\usetheme{Goettingen}
%\usetheme{CambridgeUS}
%\usetheme{AnnArbor}
\AtBeginDocument{%
\begin{CJK}{UTF8}{bsmi}}
\AtEndDocument{%
\end{CJK}}
\begin{document}
\title{中文逼門投影片via西街ㄎ}
\author{作者是我}
\date{\today}
\frame{\titlepage}
\section{標題總覽}
\frame{\tableofcontents}
\section{第一章}
\subsection{第一節}
\frame{
\frametitle{吃飽太閒}
好飽好飽}
\subsection{第二節}
\frame{
\frametitle{吃飽撐著}
好撐好撐}
\end{document}

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
則再往後取一個

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