遞歸程序

在本節中我們概覽作為指稱語義的最初主題的函數式遞歸程序的語義。

在遞歸的語義中，域典型的是偏序，它可以被理解為已定義性(definedness)的次序。例如，在自然數上的偏函數的集合可以給出為如下次序:

給定偏函數 f 和 g，設“f≤g”意味着“在 f 定義的所有值之上 f 一致於 g”。 通常假定這個域的某個性質，比如鏈的極限的存在性(參見cpo)和一個底元素。偏函數的偏序有一個底元素，完全未定義函數。它還有鏈的最小上界。各種額外性質經常是合理的和有用的: 在域理論條目中有更詳盡細節。

我們特別感興趣於在域之間的“連續”函數。它們是保持次序結構和保持最小上界的函數。

在這種設置下，類型被指示為域，而域的元素粗略的捕獲了類型的元素。給予帶有自由變量的一個程序段的指稱語義，依據它從它的環境類型的指稱到它的類型的指稱的連續函數。例如，段落 n*g(n-1) 有類型 Nat，它有兩個自由變量: Nat 類型的n 和 Nat -＞ Nat 類型的 g。所以它的指稱將是連續函數

。 在這個偏函數的次序下，可以如下這樣給出階乘程序的指稱。首先，我們必須開發基本構造如 if-then-else, ==, 和乘法的指稱。還必須開發函數抽象和應用的指稱語義。程序段

λ n:N. if (n==0)then 1 else n*g(n-1) 可以接着被給予作為在偏函數的域之間的連續函數的一個指稱

。 階乘程序的指稱被定義為函數 F 的最小不動點。它因此是域 的一個元素。

這種不動點存在的原因是 F 是連續函數。一種版本的Tarski不動點定理聲稱在域上的連續函數有最小不動點。

證明不動點定理的一種方式給出了為什麼以這種方式給出遞歸的語義合適的直覺認識，所有在域 D 的帶有底元素 ⊥ 的連續函數 F:D→D 都有不動點，它給出自

⊔i∈NF(⊥)。 這裏的符號 F 指示 F 的 i 次應用。符號“⊔”意味着“最小上界”。

把這個鏈的構件認為是“迭代”的有益的。在上述階乘的情況下，我們有在偏函數的域上的函數 F。

F(⊥) 是完全未定義偏函數 N→N； F(⊥) 是定義在 0 上，得到 1，在其他地方未定義的函數； F(⊥) 是定義直到 4 的階乘函數: F(⊥)(4) = 24。它對於大於 4 的參數是未定義的。 所以這個鏈的最小上界是完全定義的階乘函數(它湊巧是全函數)。