[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。

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