問題如下。我們需要給予程式如階乘函式的定義以語義function factorial(n:Nat):Nat ≡ if (n==0)then 1 else n*factorial(n-1)。 這個階乘程式的意義應當是在自然數上一個函式，但是由於它的遞歸定義，如何以複合方式理解它是不明白的。
基本介紹
- 中文名：遞歸程式
- 外文名：definedness
- 解釋：最初主題的函式式遞歸程式的語義
- 原因：存在的原因是 F 是連續函式
簡介,其他信息,
簡介
在本節中我們概覽作為指稱語義的最初主題的函式式遞歸程式的語義。
在遞歸的語義中，域典型的是偏序，它可以被理解為已定義性(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 的參數是未定義的。 所以這個鏈的最小上界是完全定義的階乘函式(它湊巧是全函式)。
