【導(dǎo)讀】PCF語言可以看成由三部分組成：帶函數(shù)和積類型的純類型化?演算、自然數(shù)類型和布。爾類型、不動點算子。如果想對PCF作這樣的修改，必須決定命名基本的字符和串的一種方式，就象。公理去刻畫這些函數(shù)，給出該語言的公理語義。一旦有了表達式的語法和公理語義，可以進。一步可以選擇歸約公理，寫程序，研究指稱語義。第3章到第5章分別對PCF這樣的語言的三個組成部分進行透徹的研究。系統(tǒng)了解這樣的語言。本章研究像自然數(shù)類型和布爾類型這樣的代數(shù)數(shù)據(jù)類型。這樣做的主要原因是，既維護和代數(shù)方面的文獻的一致性，同時強調(diào)代數(shù)數(shù)據(jù)。理論中，類型和類別的區(qū)別是這樣，類型有一組運算而類別沒有。應(yīng)每個類別有一個集合，對應(yīng)項中使用的每個函數(shù)符號有一個函數(shù)。向的代數(shù)等式給出，代數(shù)項的歸約公理習慣稱為重寫規(guī)則。論的討論指出了數(shù)學(xué)中傳統(tǒng)的考慮和程序設(shè)計中代數(shù)數(shù)據(jù)類型使用之間的一些區(qū)別。其中任何變量不會指派多個類別。

　　

【正文】 ??， M?N 當且僅當 E M = N [?]。很容易 檢查， ?是 T 上的一個同余關(guān)系。剩下要證明的是，對商代數(shù) A = T??，有 E ? Th (A)。證明的步驟本質(zhì)上同于定理 的證明步驟。 ? 可以用這個定理來證明，在所有類別都非空（從而所有載體也都非空）的情況下， 節(jié)的沒有規(guī)則 (nonempty)的證明系統(tǒng)的最小模型完備性。因為當所有的類別都非空時，可以像例 中描述的那樣，由代換規(guī)則刪除等式中多余變量，因此 (nonempty)成為一個導(dǎo)出規(guī)則。 推論 如果 ?是每個類別都 ?非空的基調(diào)，那么對 ?每個語法理論 E，存在一個代數(shù) A，使得 E ? Th (A)。 同態(tài)和初始性 同態(tài)和同構(gòu) 同態(tài)是從一個代數(shù)到另一個代數(shù)的保結(jié)構(gòu)的映射，本節(jié)將同態(tài)和同構(gòu)的概念從單類代數(shù)推廣到多類代數(shù)，并用同態(tài)來定義初始代數(shù)。 對多類代數(shù)來說，從 ?代數(shù) A 到 B 的同態(tài) h : A ? B是一簇映射 h = {hs | s ? S }，使得對 ?的每個函數(shù)符號 f : s1 ? … ? sk ? s，有 ) . .. , ,( )) . .. , ,(( 11 1 kssBkAs ahahfaafh k? 直觀上，同態(tài)看成是從 A 的值到 B 的值的“翻譯”。 例 令 N = ?N, 0, 1, ? ?，令 ?是模 k 的等價關(guān)系。那么把 n?N 映射到它的等價類 [n]?是從 N 到 N??的一個同態(tài)，因為 h (0) = 0N?? = [0]? h (n + m) = h (n) ?N?? h (m) = [n + m]? 通常，任何代數(shù)到它商代數(shù)的同態(tài)都用這種方式定義。 ? 16 例 含義函數(shù)是從項代數(shù) T= Terms(?, ?)到任意代數(shù) A的一個同態(tài) h : T ? A。如果 ?是 A 的一個滿足 ?的環(huán)境，該同態(tài)的定義是 h(M) = A M ? 這是一個同態(tài)，因為從項的含義可知 h (f M1 … Mk ) = A f M1 … Mk ? = f A(A M1 ? … A Mk ?) = f A(h (M1 ) … h (Mk ) ) 還可以定義從商代數(shù) Terms(?, ?)??E, ?到滿足 E 的代數(shù)的同態(tài)。 ? 為了精確論述同態(tài)和含義間的聯(lián)系，需要環(huán)境之間的一個“翻譯”。如果 h : A ?B，并且 ?是 A 的一個環(huán)境，那么定義 B 的 環(huán)境 ?h為： ?h (x) = h (? (x) ) 對任何變量 x 如果 ?滿足某個類別指派 ?，那么 ?h也滿足。 引理 令 h : A ?B 是任意同態(tài)，并且 ?是滿足類別指派 ?的任意 A 環(huán)境。那么對任何項 M? Terms(?, ?)，有 h (A M ?) = B M ?h 當 M 中不含變量時， h (A M ) = B M 證明 該證明直截了當基于項的歸納。當項是變量時，直接從 ?h的 定義可得。對于復(fù)合項 f M1 … Mk，從歸納假設(shè) h (A Mi ? ) = B Mi ?h，由同態(tài)的定義得 h (A f M1 … Mk ? ) = f B(h (A M1 ?), …, h(A Mk ?)) = f B(B M1 ?h, …, B Mk ?k) 這就證明了該引理。 ? 如果 h : A ? B 和 k : B ? C 都是 ?代數(shù)的同態(tài)，那么它們的合成 k ? h : A ? C 是通過合成每個類別映射而得到的一蔟映射 (k ? h)s = ks ? hs。 引理 如果 h : A ?B 和 k : B ?C都 是 ?代數(shù)的同態(tài)，那么合成 k ? h : A ? C也是 ?代數(shù)的同態(tài)。 這個證明作為一個習題。 一個雙射（入射并且一對一）的同態(tài)叫做 同構(gòu) 。若從 A 到 B 有一個同構(gòu)，就說 A 和 B是同構(gòu)的，寫成 A ? B。直觀上說，同構(gòu)就是重新命名元素而不改變代數(shù)結(jié)構(gòu)，因而它們本質(zhì)上是相同的。 初始代數(shù) 初始代數(shù)在研究 代數(shù)數(shù)據(jù)類型時是重要的，因為它們通常和代數(shù)規(guī)范“預(yù)期”的或“標準”的實現(xiàn)一致。如果 C 是一類 ?代數(shù)并且 A?C，若對每個 B?C，存在唯一的同態(tài) h : A ?B，那么 A 在 C 中叫做 初始代數(shù) （ initial algebra）。如果把同態(tài) h : A ?B 看成是從 A 到 B 的一個翻譯，那么初始代數(shù)是“典型”的，因為可以把初始代數(shù)“翻譯”到該類中的所有其它代數(shù)。初始代數(shù)有盡可能少的非空載體，即其它代數(shù)的空載體個數(shù)不會多于初始代數(shù)的空載體個數(shù)，因為初始代數(shù)的每一個元素必須映射到其它代數(shù)（經(jīng)過某個同態(tài)）的一個元素。再具體一點，不存 在從一個非空集合到空集的函數(shù)，但是從空集到任何集合有唯一的函數(shù)，把函數(shù)看成二元組集合的話，該函數(shù)是一個空集。另外，初始代數(shù)滿足盡可能少的閉等式（由引理 ）。本節(jié)的主要結(jié)論是，閉項代數(shù)的商是初始的（命題 ），另外還描述了初始代數(shù)的等式理論（命題 ）。 例 考慮基調(diào) ?0，它有一個類別 nat，有函數(shù)符號 0 : nat 和 S : nat ? nat。令 C 是所有 ?0代數(shù)構(gòu)成的代數(shù)類。閉項代數(shù) T ? Terms(?0, ?)是 C的初始代數(shù)，它的載體是所有閉項0, S (0), S(S (0) ), …, S k(0), … 。該代數(shù)的函數(shù) S 把 Sk(0)映射到 Sk?1(0)。該代數(shù)的元素少到能解釋所有的函數(shù)符號，并且該代數(shù)滿足項之間盡可能少的等式。 17 要證明 T 在 C 中是初始的，第一步是證明從閉項代數(shù)到 C 的任何代數(shù)有一個同態(tài)。正好，例 A 是從 T 到任何 ?代數(shù) A 的一個同態(tài)。剩下是證明該同態(tài)的唯一性。如果 h 是從 T到 ?代數(shù) A 的任意同態(tài)，那么由引理 ， h 和含義函數(shù)是相同的。注意，對于含變量的項，這 個議論是不成立的。 ? 下面先證明任何代數(shù)類的所有初始代數(shù)都是同構(gòu)的。 引理 假定 h : A ?B 和 k : B ?A 都是同態(tài)，并且 h ? k=IdB， k ? h =IdA。那么 A 和 B是同構(gòu)的。（其中 Id 是恒等函數(shù)。 ） 證明 根據(jù)同構(gòu)的定義，直接證明對每個類別 s，同態(tài) hs 是雙射便可以了。顯然， hs一定是入射的，因為 ks把每一個 x?Bs映射回到某個 y? A s使得 hs (y)=x?；陬愃频耐评恚梢钥闯?hs是一對一的。其實該證明僅使用 h 和 k 是一簇以類別為索引的函數(shù)這個事實，而并不依賴 于 h 和 k 是同態(tài)。 ? 因為同構(gòu)代數(shù)本質(zhì)上是相同的，這就意味著任何代數(shù)類的初始代數(shù)如果存在的話，那么它唯一到同構(gòu)。 命題 如果 A 和 B 在代數(shù)類 C 中都是初始代數(shù)，那么 A 和 B 是同構(gòu)的。 證明 因為 A和 B在代數(shù)類 C中都是初始代數(shù)，那么存在唯一同態(tài) h : A ?B和 k : B ?A。由引理 ，只要證明 h ? k=IdB并且 k ? h =IdA就可以了。 由引理 ， h ? k 和 k ? h 分別是 A 到 A 和 B 到 B 的同態(tài)。因為 IdA和 IdB也分別是 A到 A 和 B 到 B 的同態(tài)，由初始同態(tài) 的唯一性， h ? k=IdB， k ? h =IdA。 ? 在例 中，在寫符號 nat, 0 : nat 和 S : nat ? nat 時，通常把它們解釋成自然數(shù) 0 和后繼函數(shù)，其實這是該基調(diào)的“預(yù)期模型”。該例中，基調(diào) ?0的初始代數(shù)和該預(yù)期模型同構(gòu)。 如果 E 是一組 ?等式，如果在滿足 E 的所有 ?代數(shù)構(gòu)成的代數(shù)類中 A 是初始的，那么就說 A 對 E 是初始的。 命題 令 E是一組 ?等式，并且令 A = Terms(?, ?)??E, ?是只有閉項并且模可證明的相等性的代數(shù)。那么， A 對 E 來說是初始代數(shù)。 在 E 是空集的情況下，很容易看出 Terms(?, ?)??E, ?和 Terms(?, ?)同構(gòu)。因此，從這個命題知道，閉項代數(shù)在所有的 ?代數(shù)構(gòu)成的類中是初始的。 證明 由項代數(shù)和商的性質(zhì)，從 E可證明的等式在 A中都成立。剩下要證明的是從 A 到任何滿足 E 的代數(shù)有唯一的同態(tài)。 令 B 是滿足 E的一個代數(shù)。對 A 中的任何等價類 ?M?，令 h(?M?)是不含變量的項 M 在 B中的含義 B M 。因為 B 滿足 E，因此這個映射是很好地定義的。很容易 檢查 h 是個同態(tài)。由引理 ，任何其它同態(tài) h? : A ? B 和 h一定有相同的值，因此 h 是從 A 到 B 的唯一同態(tài)。 ? 由此可以得出，任何代數(shù)規(guī)范都有初始代數(shù)。 下面的例子是自然數(shù)作為初始代數(shù)的延伸討論， 節(jié)還有一些其它例子。 例 考慮只有一個類別 nat 的基調(diào) ?1，它有函數(shù)符號 0 : nat， S : nat ? nat和 ? : nat ? nat ? nat。令 E 是等式集合 x + 0 = x x + (Sy) = S (x + y) 在此省略類別指 派，因為這里只有一個類別。令 C 是滿足 E 的所有 ?1代數(shù)構(gòu)成的代數(shù)類。 基于這組 E，可以證明有如下事實： （ 1） Sk0 + Sl0 = Sk + l0； （ 2）對任何閉項 M，存在某個自然數(shù) k，使得 M = Sk0； （ 3）等式 Sk0 = Sl0 是不可證明的，除非 k = l； （ 4）每個等價類正好包含一個形式為 Sk0 的項； 18 （ 5）等價類和形式為 Sk0 的項集間有一個雙射。 可以把這個項代數(shù)的載體看成由閉項 0, S0, …, Sk0, … 構(gòu)成的集合，并且在這個初始代數(shù)中，函數(shù) S 映射 Sk0 ? Sk＋ 10， ?映射 (Sk0, Sl0) ? Sk＋ l0。于是，這個初始代數(shù)和該基調(diào)的標準模型（有后繼算子和加法的自然數(shù)） 同構(gòu)。 該規(guī)范的初始代數(shù)可以和其它有更多或較少元素的代數(shù)相對照。一般來說，如果一個代數(shù)有更多的元素的話，那么這些多余的元素不能由項定義，并且不會出現(xiàn)在該代數(shù)上的計算中，這樣的元素被稱為“假貨”。 如果一個代數(shù)有較少的元素的話，那么就有一些不能被證明為相等的有區(qū)別的元素被等同，這種情況被稱為“混淆”。先用例子來說明這兩種可能性，而把證明例子是非初始的作為習題。 比初始代數(shù)含更多元素的代數(shù)有整數(shù)代數(shù) Z。另一個例子由加“無窮個”整數(shù)到 N 來構(gòu)造。這第二個例子更一般，因為也可以用這種方法來構(gòu)造表、集合、樹和其它規(guī)范的非初始代數(shù)。對 ?1，非初始代數(shù) A = ?Anat, 0A, SA, +A?有 Anat = (?0? ? N) ? ({1} ? Z) 其中 N 是自然數(shù)集合， Z 是整數(shù)集合。直觀上， Anat含一個自然數(shù)的“拷貝”，其中每個元素是二元組 ?0, n?的形式， Anat還含一個整數(shù)的“拷貝”，其中每個元素是二元組 ?1, n?的形式。若把所有這些元素列成一行，可以讓自然數(shù)出現(xiàn)在整數(shù)的左邊： 0, 1, 2, 3, … …, 3, 2, 1, 0, 1, 2, 3, … 然后把左邊的自然數(shù)想象成“小”或“有限”的數(shù)，把右邊的整數(shù)想象成“大”或“無限”的數(shù)，因為它們被看成大于這所有的有限數(shù)。 0A 被解釋為最左邊的零，任何數(shù)的后繼是上面序列中右鄰它的數(shù)。如果同一部分的兩個數(shù)相加，將得到標準的結(jié)果（有限或無限）。如果一個有限數(shù)加到無限數(shù)上，結(jié)果將是無限數(shù)。這就給出了下面的形式定義： 0A = ?0, 0? SA?i, n? = ?i, n +1? ?i, n? +A ?j, m? = ?max(i, j), n +m? 可以檢查，該規(guī)范的兩個公理在這些代數(shù)中都成立。子集 ({1} ? Z)的元素在這兒是“假貨”，它們不能由閉項定義。因為初始代數(shù)所含的元素都可由閉項定義，因此這些“假貨”不出現(xiàn)在初始代數(shù)中。 比初始代數(shù)含元素少的代數(shù)有模 k 的 自然數(shù)（ k 是任意自然數(shù)），在例 已討論了這個代數(shù)。很容易檢查，該規(guī)范的兩個公理在這個代數(shù)中都成立。認為它有混淆是因為在該規(guī)范中不能證明為相等的不同數(shù)碼在該代數(shù)中給出了同樣的值。而在初始代數(shù)中，只有在能證明兩個閉項相等時，它們才有同樣的 值。 ? 初始代數(shù)的一個重要特點是，它可能滿足不能由 E 證明的額外的等式。直觀上，增加元素到一個代數(shù)可能引起帶變量的等式變得不能成立，因為一個新元素可能和所有其它元素共享的一個性質(zhì)沖突。由于初始代數(shù)的載體盡可能小，初始代數(shù)滿足的等式可能在其它滿足E 的，有更多元素的代數(shù)中不成立。一個簡單的例子是只有一個類別和兩個常量 a 和 b 的基調(diào)。滿足 a = b的初始代數(shù)只有一個元素。結(jié)果，初始代數(shù)滿足 x = y，但是它不是等式 a = b的語義蘊涵，因為滿足 a = b的含更多元素的代數(shù)不滿足 x = y。 一個更加自然的例子如下： 例 例 的初始代數(shù)滿足 +的交換性，雖然它不可能從那些等式證明。很容易看出在初始代數(shù)中加法是可交換的，因為對任何不含變量的項 M 和 N，有 E M = Sk0 和 E N = Sl0（對某個 k 和 l），并且 E M + N = Sk+l0 = N + M。但是等式 x + y = y + x 從 E不可證明。可