4.1 指稱語意
指稱語意(denotational semantics)談一個程式是什麼。
在我們的討論範圍中，有堅實基礎、有不含糊的定義的東西只有數學物件。
因此，指稱語意試圖把程式語言對應到數學物件。
最簡單的指稱語意可能是基於集合論的：把型別視為集合，把程式語言中的函數視為集合論中的函數。
例如，Nat 便是自然數的集合；(A * B) 是 A 與 B 的笛卡兒積：
在更嚴謹的說法中，我們通常用一個語意函數$\llbracket\_\rrbracket$將語法對應到其意義。因此我們會說 $\llbracket |A*B| \rrbracket = \llbracket |A| \rrbracket \times \llbracket |B| \rrbracket$. 此處採用較不正式的說法。
(A * B) ~&= \{ (a,b) \mid a \in A, b \in B \} 但函數又是什麼呢？集合論中，一個型別為 A -> B 的函數可視為 A * B 的一個子集；若 f x = y，該子集中便有 (x,y) 這個元素。例如，double :: Nat -> Nat 可表示成如下的集合：
\{(0,0), (1,1), (2,4), (3,6), (4,8) \ldots \} 能稱為函數的集合還需滿足兩個額外條件：
簡單性(simplicity): 對所有 $x \in |A|$, 該集合中僅存在一對唯一的
(x,y)。意即每個輸入只對應到一個輸出。完整性(totality): 對所有 $x \in |A|$, 在該集合中都存在某對
(x,y)。意即值域中的每個元素都被涵蓋到。
至於遞迴函數呢？以階層 fact 為例，其定義為：
fact :: Nat -> Nat
fact Zero = 1
fact (Suc n) = (Suc n) * fact n
我們可想成：有一個從集合到集合的函數 factF，
\Varid{factF}~X ~=~ \{(Zero,1)\} \cup \{(Suc n, (Suc n) \times m) \mid (n,m) \in X \} 給任何集合 X，factF 傳回這樣的集合：
新集合中有
(Zero,1)--- 這對應到fact Zero = 1.對
X之中的每一個(n,m), 新集合中有(Suc n, (Suc n) * m)--- 這對應到fact (Suc n) = (Suc n) * fact n.
而函數 fact 的語意就是 factF 唯一的定點 (fixed point).
意即 fact 是唯一滿足 fact = factF fact 的集合。
關於定點的較完整理論可參照第 2.9 節。
確實，fact 可寫成集合如下：
fact = {(0,1),(1,1),(2,2),(3,6),(4,24)...}
若將 fact 餵給 factF,
factF fact
= {(0,1)} ∪ {(Suc n, (Suc n) * m) | (n,m) `elem` {(0,1),(1,1),(2,2),(3,6)...}}
= {(0,1)} ∪ {(1,1),(2,2),(3,6),(4,24)...}
我們又得到了 fact. 因此 fact 確實是 factF 的定點。
但，要把「fact 便是 factF 的定點」當作 fact 的定義，我們還得確定：確實只有這麼一個集合滿足 fact = factF fact。
讀者稍加檢查一下，即可發現確實如此 ---
例如，把 fact 添一項或刪一項，都會使得 factF fact 不等於 fact.
並不是所有從集合到集合的函數都有唯一的定點。考慮如下兩個函數：
g 0 = 0
g x = g (Suc x)
h 0 = 0
h x = (-1) * h x
若以類似 fact 的方式試圖將它們寫成某函數的定點，我們可能寫出如下的 gF 和 hF:
gF X = {(0,0)} ∪ {(n,m) | (Suc n,m) `elem` X}
hF X = {(n,(-1*m)) | (n,m) `elem` X}
但 gF 的定點有
{(0,0),(1,1),(2,1),(3,1)...}
{(0,0),(1,2),(2,2),(3,2)...}
{(0,0),(1,10),(2,10),(3,10)...} {-"~~..."-}
等無限多個。而 hF 有一個唯一定點：空集合，但空集合違反了前述的完整性要求。
如同 g 和 f 這樣的函數，在我們目前介紹的簡單指稱語意中是沒有定義的。
它們沒有語意，在我們的語言中是不該有的存在。
它們剛好也是執行起來不會終止的函數。
因此，我們似乎可以猜測「有唯一定點」和「執行會終止」似乎有些關聯。
但，如前所述，我們的指稱語意中沒有「執行」的觀念。
那是操作語意擅長描述的。
值得一提地，指稱語意採取了一個靜態的世界觀。 一個函數單純地是輸入與輸出的對應，沒有「執行」的觀念，沒有執行快慢的考量，也沒有預設「終止」的概念。
函數 double1 x = x + x 與 double2 x = 2 * x 使用不同的演算法，但它們的語意都是同一個集合，因此被視為同一個函數 --- 在語意上我們無法區分 double1 與 double2。
在指稱語意中，當我們說兩個函數相等，意指它們的語意是同一個集合。
例如，map Suc . concat = concat . map (map (Suc)), 因為兩者的語意都是下述的集合：
{([],[]), ... ([[1],[2]], [2,3]),... ([[1],[2,3]],[2,3,4]), ...}