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

　　

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