[Notes] Semantics, Category and their Implementation 1

此篇為彼篇之後續...

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

一個 program g 的 denotational semantics 是一個 function g，標記成

[[g]] = g。

那麼，我們如何去找出這個合適的 g ？ 若 g 是 non-recursive 的話，那麼我們就直接根據 g 的定義去描述 g。例如說我們寫一個 program 如下：

g True = False
g False = True

則我們可以直接看出

[[g]] = {(T,F),(T,F),(⊥,⊥)} = not。

相對地，如果 g 是一個 recursive program，那麼我們就需要另外想辦法去組合出出相對應的那個 function g。回顧一下這篇的最後一塊有關 semantics 的部份，我們知道我們可以定義合適的 function f 以及其對應的 program f 使得

• f g = g
• f g = g 

換句話說，我們讓 g 是 f 的 least fixed point。這樣我們就可以根據 least fixed point 的一些性質來明確的描述出 g。

舉例來說，有一個 recursive program 如下：

g = \n -> if n==0 then 1 else n*(g (x-1))，

那麼，我們便可以寫出另一個 non-recursive program 如下

f g = \n -> if n==0 then 1 else n*(g (x-1))。

現在，假設我們知道 [[f]] = f，根據 least fixed point theorem 我們會知道說：對 function f，我們可以用 fix 來得到 least fixed point of f：

f (fix f) = fix f。

另外，我們還知道

fix f = ⊔Xf ; Xf = {⊥, f ⊥, ff ⊥, fff ⊥, ...}

因此，這邊實際上要做的事情就是去計算一個 directed set, Xf, 的 least upper bound。

從頭來過一次，我們的問題及解決的過程如下：

• 有一個 recursive program g，我們想要找出其 semantics [[g]]
• 寫一個 program f g = g，並且定義出相對應的 f g = ...
• 也就是說，我們做出一個 f 並且用這個 f 的 least fix point 去描述 g
• 因此，我們實際上是在找 fix f
• 也就是說，我們要找 ⊔Xf
• 最後，我們知道 g 的 semantics 實際上就是 Xf 的 least upper bound
• 也就是在找 {⊥, f ⊥, ff ⊥, fff ⊥, ...} 的 least opper bound

---

傳統這邊會用的例子就像上面舉例的 g 一樣，是一個拿自然數, N, 當作參數的程式。然後從 ⊥ 開始去執行一個 fixed point iteration 來計算出 Xf 的 least upper bound，而這就是我們要找的 [[g]]。這邊直接拿前面那個例子繼續：

我們有如下的 program ：

g = \n -> if n==0 then 1 else n*(g (x-1))，

據此我們寫出 function f：

f g = \n -> if n==0 then 1 else n*(g (n-1))。

接著我們要從 undefined function 開始一步一步地將 f applies 上去以找出 least upper bound of Xf。為了區別不同 domain 上面的 bottom，這裡用 ⊥(D) 來表示 domain D 上面的 bottom，因此 undefined function = ⊥(N->N) = {(n,⊥(N))|n<-Nat}。(<-) 表示 set 上的 membership。另外，這邊也用 fk 表示連續 apply k次的 f。

f0 n = ⊥(N->N) = {(n,⊥(N))|n∈N}
f1 n = f (f0 n) = {(0,1)}U{(n,⊥(N))|n>0}
f2 n = f (f1 n) = {(0,1),(1,1)}U{(n,⊥(N))|n>1}
...
fk+1 n = f (fk n) = {(n,n!)|n<=k}U{(n,⊥(N))|n>k}
...

明顯地，[[g]] = fix f = ⊔Xf = n! forall n ∈ N。

關於其他例子與 functor，請看下一篇。