邏輯與程式語言

邏輯長久以來一直關注某些問題的答案原則上是否可計算，因為結果界定了形式化的可能性。最近，透過複雜性理論的發展，決策方法的時間效率有了精確的比較。然而，這些是邏輯的應用，而一個大問題是，邏輯的方法是否在另一方面對可計算性理論更應用的部分具有重要意義。

程式語言提供了一個明顯的機會，因為它們的語法形式化已經相當成熟；然而，其語義理論很難說得上是完整的。儘管我們有許多例子，但我們仍需對以下問題給出廣泛的數學答案：什麼是機器？什麼是可計算過程？機器如何（或多好地）模擬一個過程？程式自然地用於描述過程。因此，程式精確含義的定義要求我們解釋計算的對象是什麼（某種程度上是問題的靜態），以及它們如何轉換（動態）。

到目前為止，自動機理論和網路理論雖然在動態方面非常有趣，但僅形式化了該領域的一部分，並且可能過於集中在有限狀態和代數面向。理解高階程式特性似乎需要我們處理無限對象，並且需要經過幾個解釋層次，才能從概念想法轉換到實際機器上的精確模擬。如果我們能找到正確的抽象來表示必要的結構，這些層次就可以在數學上變得精確。

許多獨立工作者透過將資料型別視為在資訊內容排序下的格（或偏序集），以及連續映射的方法所累積的經驗，證明了這種方法在提供清晰且不過度依賴實作的定義和證明方面的靈活性。然而，在我們能說我們有一個統一的理論之前，還有許多工作需要完成，以展示抽象概念化如何能夠（或不能夠）實現。

CR Categories: 1.2, 4.20, 5.21, 5.24, 5.27

作為第十一又二分之一屆圖靈獎得主，我非常高興能與 Michael Rabin 分享這個獎項和這個講台。可惜，自我們在 1959 年合寫論文以來，我們沒有太多合作的機會，這對我來說是一個巨大的損失。我最適合在合作中工作，但要創造適當的條件並不容易——尤其是在跨學科領域和人們被國際界線隔開的情況下。但我一直懷著深厚的興趣和欽佩關注著他的職業生涯。正如今天你們聽到的，Rabin 能夠將邏輯中有關可判定性、可計算性和複雜性的思想應用到具有真正數學和計算意義的問題上。他以及許多其他人正在積極為廣泛的演算法問題類別創造新的分析方法，這為未來發展帶來巨大希望。然而，計算理論的這些方面完全超出我的能力範圍，因為這些年來我的興趣已經與 Rabin 的興趣有所分歧。自 1960 年代後期以來，我自己的工作一直專注於考察邏輯的思想是否可以用於更好地概念化理解程式語言。因此，今天我不會詳細談論我過去與 Rabin 的合作工作，而是談論我自己的發展以及對未來的一些計畫和希望。

在委員會建構龐大「通用」電腦語言的時期，產生了難以對一個語言獲得精確全面觀點的問題。現在看來，我們正處於另一場技術革命的門檻上，我們的機器和軟體概念將被徹底改變。（我剛剛注意到 ACM 再次發起運動，完全取消「機器」這個詞。）那些龐大的語言可能證明不太具適應性，但我認為語義問題肯定會依然存在。我想，這項工作——同樣是與其他人合作完成的，最著名的是已故的 Christopher Strachey——對語義事業的基礎做出了基本貢獻。好吧，我們拭目以待。我也希望語義學的研究不會再與像 Rabin 這樣的研究長時間地脫節。

一段致歉與不致歉的聲明

通常來說，我認為公眾演說者不應道歉：這只會讓聽眾感到不舒服。然而，在這樣的會議上，一個道歉是必要的（以及一個免責聲明）。

認識我背景的人可能會想起 Sir Nicholas Gimcrack，戲劇《The Virtuoso》中的英雄。這是 Thomas Shadwell 在 1676 年寫的，目的是稍微嘲笑當時在 Royal Society of London 進行的非凡實驗。戲劇中，Sir Nicholas 有一處躺在桌子上，試圖透過模仿水盆裡青蛙的動作來學習游泳。當被問到是否曾在水中練習游泳時，他回答說他討厭水，從不靠近它！他說：「我滿足於游泳的『理論部分』；我不在乎實際操作，我很少將任何事物付諸實用……知識是最終目的。」

現在，儘管我們的最終目標相同，但我還是急於表明自己與那種蔑視實踐的態度撇清關係。然而，事實是，我沒有當今程式設計的實踐經驗；出於必要，我不得不局限於理論性程式設計，透過觀察各種青蛙和其他生物間接獲得知識。幸運的是，其中一些青蛙會說話。對於其中一些，我不得不學習一種外語，也許我沒有完全理解他們在做什麼。但我一直努力閱讀並跟上發展。我為自己不是程式設計領域的專業人士而道歉，因此我當然不會試圖佈道：過去許多圖靈獎得主都非常適合這樣做，他們給了我們非常好的建議。我所嘗試做的是，將一些我認為與計算相關的邏輯成果，變得那些可以使用它們的人能夠理解。我也嘗試添加了一些我自己的成果，我必須讓你們來判斷我的活動是否成功。

今天最幸運的是，我不必為缺乏已出版的材料而道歉；如果我是在接到邀請的那天寫這篇演講稿，我可能會這樣。但在《Communications》八月號中，我們有 Robert Tennent [14] 關於指稱語義學的精彩入門文章，我非常強烈推薦它作為起點。Tennent 不僅提供了遠超出 Strachey 和我曾經發表的認真範例，而且他還有一個組織良好的參考書目。

就在上個月，Milne 和 Strachey 合著的那本厚重書籍 [9] 出版了。Strachey 令人震驚的突然和英年早逝不幸地阻止了他對手稿進行修訂。Strachey 的離世讓我們在風格和洞察力上損失良多（更不用說靈感了），但 Robert Milne 出色地執行了他們的計畫。這本書的重要性在於，它從頭到尾深入討論了一個複雜語言。有些人可能會覺得其呈現過於嚴謹，但重點是，這本書的語義不是空泛的猜測，而是真實的東西。它是認真且知情的思考的產物；因此，我們有了詳細的證據來判斷這種方法是否會富有成效。Milne 的組織方式使得讀者可以從概念層面一直理解到最終編譯器。他沒有迴避任何困難。儘管不像 Strachey 在談話中那樣輕鬆尖銳，但這本書是對 Strachey 最後階段工作的非常恰當的紀念，它包含了 Milne 自己大量的原創貢獻。（我之所以能說這些話，是因為我沒有參與撰寫這本書。）

最近出版的還有 James E. Donahue 的著作 [4]。這是一本不太長且非常易讀的作品，討論了上述參考資料沒有涵蓋或從不同角度涵蓋的問題。同樣，這本書完全獨立於 Strachey 和我所寫，我很高興看到它的出現。

Joe Stoy 的教科書 [13] 即將出版。這將補充這些其他作品，並且對於教學應該非常有用，因為 Stoy 在牛津大學和 M.I.T. 都有出色的授課經驗。

在基礎方面，我自己的修訂版論文 (Scott [12]) 即將在《SIAM Journal on Computing》上發表。由於它是從「更經典」的遞歸理論中的列舉算子角度寫的，乍看之下其與實際計算的相關性可能並不明顯。因此，我很欣慰地看到這些其他參考資料以我預期的方式解釋了該理論的用途。

幸運的是，上述所有作者都廣泛引用了文獻，因此我今天可以不必再深入探討歷史細節。我只想說，還有許多其他人接受了 Strachey 和我的一些想法，你們不僅可以在這些參考書目中，還可以在例如最近的兩本會議論文集 Manes [7] 和 Böhm [1] 中找到他們的工作。如果我試圖在這裡列出名字，我肯定會遺漏一些人——那些與我接觸過的人都知道我多麼感激他們的興趣和貢獻。

個人回憶錄

我出生在加州，並在 1950 年代早期作為柏克萊大學的本科生開始我的數理邏輯工作。主要影響當然是 Alfred Tarski 以及他在加州大學的眾多同事和學生。在許多其他事情中，我從 Raphael 和 Julia Robinson 那裡學習了遞歸函數理論，我要感謝他們提供了無數洞見。當時，我還透過自學了解了 Curry 和 Church 的 λ 演算（起初這真的讓我做惡夢）。對我後來的想法特別重要的是研究 Tarski 的語義及其對形式化語言的真值定義。正如你們所知，這些概念至今仍在自然語言哲學中被熱烈討論。我試圖將 Tarski 方法的精神轉移到演算法語言上，這些語言至少在語法上相當形式化。我是否如 Strachey 的方案（並由許多人實施）所指導，找到了術語的正確指稱，這正是需要討論的。我首先要說，僅僅給某些語言賦予指稱並不能解決所有問題。像 (非常純粹的) λ 演算這樣的語言得到了很好的服務，但許多程式概念仍未被涵蓋。

我的研究生工作於 1958 年在普林斯頓大學完成，導師是 Alonzo Church，他也指導了 Michael Rabin 的論文。我和 Rabin 在那時相識，但我們在 1957 年 IBM 的暑期工作中完成了關於自動機理論的合作。這項工作絕非真空進行，因為當時有很多人在這個領域工作；但我們確實設法將一些基本想法突出出來。那時，我肯定在思考如何給機器一個數學定義的專案。我現在認為，有限狀態的方法僅部分成功，並且在實際應用方面沒有太多意義。確實，許多物理機器可以建模為有限狀態設備；但有限性並不是最重要的特徵，而且自動機的觀點通常相當膚淺。

後來的兩個發展使自動機對我來說更具趣味性，至少在數學上：Chomsky 層次體系以及與半群的聯繫。從代數觀點來看（至少符合我的口味），自動機理論的歐幾里得 Eilenberg 在他的書 [5] 中已說了幾乎是最後的話。我也注意到他避免了抽象範疇論。範疇論可能帶來好的結果 (cf. Manes [7])，但過早使用只會讓事情變得太難理解。這是我的個人意見。

從某些方面來說，Chomsky 層次體系最終是令人失望的。上下文無關語言非常重要，每個人都必須學習它們，但我完全不清楚接下來會出現什麼——如果有的話。還有很多其他語言家族，但混沌中沒有太多秩序產生。我不認為這裡已經說了最後的話。正是不知所向，並對我認為過度複雜感到不滿，使我放棄了自動機理論的工作。我曾嘗試透過一種特定的方式將自動機與程式語言聯繫起來，提出一種更系統地分離機器和程式的方法。Eilenberg 非常不喜歡這個想法，但我很高興看到 Clark 和 Cowell 最近的書 [2]，其中在 Peter Landin 的建議下，這個想法被很好地實現了。我承認這不是代數，但在我看來，它是（基礎的、有些理論性的）程式設計。我想看看下一步，那應該介於 Manna [8] 和 Milne-Strachey [9] 之間。

正是在普林斯頓，我第一次接觸到真正的機器——現今幾乎是史前時代的馮諾依曼機器。我必須感謝 Forman Acton。儘管現在看起來很老舊，但它仍然是真實的；我和 Hale Trotter 在它上面玩得很開心。看到 Smithsonian Museum 中完全死寂的屍體，完全沒有任何關於它活著時是什麼樣子的指示，我真是非常傷心。

從普林斯頓大學，我到芝加哥大學數學系任教兩年。雖然當時我見到了 Bob Ashenhurst 和 Nick Metropolis，但我的停留時間太短，無法從他們那裡學習；而且部門之間的距離總是太遠。（當然，由於我只寫與計算相關的聯繫，我並不是在解釋我在數學和邏輯方面的其他活動。）從芝加哥，我到柏克萊待了三年。在那裡，我透過 Harry Huskey 和 René de Vogelaere 認識了許多計算機領域的人，後者向我介紹了 Algol 60 的細節。然而，當時柏克萊沒有計算機科學系這樣一個部門。由於個人原因，我很快決定搬到史丹佛大學。因此，儘管我在柏克萊教了一個學期的計算理論課程，但我的工作沒有取得任何成果。對於柏克萊和計算，我將永遠遺憾的一件事是，我從未學習 Dick 和 Emma Lehmer 工作中的細節，因為我非常欽佩他們用機器在數論中取得成果的方式。現在，透過機器解決了四色問題，我們將看到大規模、特殊用途定理證明的巨大發展。我很遺憾沒有參與其中。

從 1960 年代早期起，史丹佛大學就擁有全國最好的計算機科學系之一，這是所有人都認可的。你們可能會想知道我為什麼要離開。答案可能是我在哲學系和數學系之間的混合任職。我想我個人的困難在於不知道我應該在哪裡以及我想做什麼。但撇開個人缺點不談，我在 Forsythe 出色的系裡有很好的聯繫，與研究生們關係也非常好，我們有很多活躍的課程和研討會。John McCarthy 和 Pat Suppes 以及他們團隊的人對我和我的計算觀點有很大的影響。在邏輯方面，我與同事 Sol Feferman 和 Georg Kreisel 有一個非常活躍的小組。在眾多邏輯學博士生中，Richard Platek 的工作在幾年後，當我看到如何運用他的一些想法時，對我影響很大。

此時，我在阿姆斯特丹休假了一年，這意外地成為我思想發展的轉折點。我不會深入細節，因為故事很複雜；但 1968/69 學年對我來說是深刻危機的一年，回想起來仍然非常痛苦。然而，幸運的是，Pat Suppes 推薦我參加 IFIP Working Group 2.2（現在稱為 Formal Description of Programming Concepts）。那時主席是 Tom Steel，正是在維也納的會議上我第一次遇到了 Christopher Strachey。如果這個小組爭論的激烈程度能說明什麼的話，我真慶幸自己沒有參與像 Algol 委員會那樣重要的事。但我猜爭吵是治療性的：它激發出人們最好和最壞的一面。無論如何，學會自衛是好的。在各個爭論者中，我最喜歡 Strachey 的風格和想法，儘管我認為他常常誇大了他的論點；但他所說的話使我相信我應該學習更多。

直到我在阿姆斯特丹待了一年之後，我才開始與 Jaco de Bakker 交談，並且直到那個夏天透過通信，我們的想法才有了明確的輪廓。我在 WG 2.2 中遇到的 Vienna IBM Group 在這個階段也影響了我。同時，我已經決定離開史丹佛大學，去普林斯頓大學哲學系；但因為我和家人都在歐洲，我請求額外延長一學期的假期，以便在 1969 年秋天拜訪牛津的 Strachey。那個學期對我來說是狂熱活動的一個學期；事實上，有好幾天，我覺得自己得了某種真正的腦熱。那幾個星期與 Strachey 的合作是我職業生涯中最棒的經歷之一。我們在第二年夏天在普林斯頓又重複了一次，儘管興奮程度不同。令人遺憾的是，到 1972 年我永久搬到牛津時，我們都忙於教學和行政事務，真正的合作幾乎不可能了。Strachey 也因持續缺乏研究資金和教學援助而非常沮喪，他基本上退隱下來與 Milne 寫他的書。（這是一項巨大的努力，我不認為這對他的健康有好處；我多希望他能看到它出版。）

回到 1969 年，我開始做的事情是向 Strachey 展示他是完全錯誤的，他應該用另一種方式來做事情。他最初是受到 Roger Penrose 的注意，開始研究 λ 演算，並發展了一種方便的風格，使用這種符號進行函數抽象，來解釋程式概念。然而，這是一種形式裝置，我試圖論證它沒有數學基礎。這個故事我以前講過，所以長話短說，我只想說，首先我實際上用「優越的邏輯」說服了他放棄無型別 λ 演算。但隨後，我的建議帶來一個接一個的結果，我開始看到可計算函數可以在各種各樣的空間上定義。真正的突破是看到函數空間是好的空間，我清楚地記得當時也在牛津訪問的邏輯學家 Andrzej Mostowski 根本不相信我定義的那種函數空間有建構性的描述。但當我看到它們確實有時，我開始懷疑使用函數空間的可能性可能比我們想像的更令人驚訝。一旦對我曾試圖強加給 Strachey 的強制性邏輯型別的剛性產生了懷疑，沒過多久我就找到了一個與其自身函數空間同構的空間，這為「無型別」λ 演算提供了一個模型。故事的其餘部分都在文獻中了。

（關於 λ 演算一個有趣的旁證是 Alan Turing 的作用。他在普林斯頓大學隨 Church 學習，並在 1936/37 年左右將可計算性與（形式的）λ 演算聯繫起來。關於他的工作（以及 λ 演算的進一步影響）如何被 Steve Kleene 看待的具體細節可以在 Crossley [3] 中找到。（當然，Turing 後來關於計算機的想法極大地影響了 Strachey，但這不是進行完整歷史分析的時候。）雖然我從未見過 Turing（他於 1954 年去世），但透過 Church 和 Strachey 以及我現在牛津的同事 Les Fox 和 Robin Gandy 的間接聯繫相當緊密，儘管在我成為普林斯頓研究生時，Church 已經不再研究 λ 演算了，我們從未討論過他與 Turing 的經歷。）

非常奇怪的是，我的 λ 演算模型沒有更早被其他人發現；但我對現在正在發現具有新屬性的新型模型（例如 Gordon Plotkin [10] 的「冪域」）感到非常鼓舞。我個人深信這個領域在理論和應用方面都已穩固建立。John Reynolds 和 Robert Milne 獨立地引入了一種新的歸納證明等價性的方法，Robin Milner 關於 LCF 及其證明技術的有趣工作在愛丁堡持續進行。這個證明模型性質的方向始於 David Park 關於不動點算子和所謂 λ 演算中的悖論組合子之間關係的定理，它開啟了對無限但可計算算子的研究，這種研究現在沿著許多方向繼續進行。另一個工作方向在 Yu.L. Ershov 的領導下在 Novosibirsk 進行，Karl H. Hofmann 及其團隊向我指出了一些與拓撲代數的驚人聯繫。這裡沒有空間甚至開始列出眾多貢獻者。

展望未來幾年，我特別高興在這次會議上報告，Tony Hoare 最近接受了牛津大學的計算講座教授職位，該職位自 Strachey 去世後已永久化。這為未來的合作開闢了各種新的可能性，無論是與 Hoare 本人，還是與他明年上任後將吸引的許多學生。而且，正如你們所知，計算機語言的使用和設計以及程式設計方法的實務面向肯定會在牛津得到強調（我急於補充說 Strachey 也這樣做了），這完全是好事；但理論研究也有極好的希望。

一些語義結構

現在談到技術細節，我想簡要介紹一下我的建構如何進行，以及它如何具有相當大的變化空間。這裡不可能論證這些是「正確」的抽象，這也是為什麼先前提到的參考資料很容易獲得令人感到寬慰的原因。

也許最快能說明我正在探討什麼的是兩個領域：$\mathcal{B}$，布林值領域，以及 $\mathcal{N} = \mathcal{B}^\omega$，布林值無限序列領域。第一個要點是我們將接受偏函數的思想，在數學上表現為函數在某些時候給出偏值。就 $\mathcal{B}$ 而言，這個想法非常簡單：我們寫

$\mathcal{B} = { \text{true}, \text{false}, \perp }$

其中 $\perp$ 是一個額外元素，稱為「未定義」。為了讓 $\perp$ 待在其應有的位置，我們在領域 $\mathcal{B}$ 上施加一個偏序 $\sqsubseteq_\mathcal{B}$，其中

$x \sqsubseteq_\mathcal{B} y \text{ 若且唯若 } x = \perp \text{ 或 } x = y$，

對於所有 $x, y \in \mathcal{B}$。這在 $\mathcal{B}$ 中意義不大，但我們可以將「$\sqsubseteq$」讀作 $x$ 的資訊內容包含在 $y$ 的資訊內容中。因此，元素 $\perp$ 具有空資訊內容。這個方案如圖 1 所示。

圖 1. 布林值。

  true   false
     \   /
      ⊥

（一個旁註：在許多出版物中，我提倡使用格，它們作為偏序集具有「頂部」元素 $\top$ 以及「底部」元素 $\perp$，以便我們可以斷言 $\perp \sqsubseteq x \sqsubseteq \top$ 對於領域的所有元素都成立。這個建議由於許多我不能在這裡詳細討論的原因並未受到好評。一些關於其合理性的討論可以在 Scott [12] 中找到，但那裡研究的結構是特殊的。最好的方法可能是不排除也不包含 $\top$；為簡單起見，我今天不再提及它。）

現在看 $\mathcal{N}$，序列領域，我們將使用速記符號，下標表示坐標；因此，

$x = (x_n)_{n=0}^\infty$

對於所有 $x \in \mathcal{N}$。每個項都滿足 $x_n \in \mathcal{B}$，因為 $\mathcal{N} = \mathcal{B}^\omega$。技術上，這裡指的是結構的「直積」，所以我們定義 $\sqsubseteq$ 在 $\mathcal{N}$ 上為

$x \sqsubseteq y \text{ 若且唯若 } x_n \sqsubseteq_\mathcal{B} y_n \text{ 對所有 } n \text{ 成立。}$

直觀上，序列 $y$ 的資訊比序列 $x$「更好」，若且唯若從 $x$ 到 $y$ 時，一些 $x$ 中「未定義」的坐標變成了「已定義」。例如，以下每個序列都與其後面的序列處於 $\sqsubseteq$ 關係：

$(\perp, \perp, \perp, \perp, \dots)$, $(\text{true}, \perp, \perp, \perp, \dots)$, $(\text{true}, \text{false}, \perp, \perp, \dots)$, $(\text{true}, \text{false}, \text{true}, \perp, \dots)$.

顯然，這個列表可以無限擴展，而且也沒有必要嚴格按照 $n = 0, 1, 2, \dots$ 的順序處理坐標。因此，$\mathcal{N}$ 上的 $\sqsubseteq$ 關係比 $\mathcal{B}$ 上的原始 $\sqsubseteq_\mathcal{B}$ 複雜得多。

$\mathcal{B}$ 和 $\mathcal{N}$ 的一個明顯區別在於 $\mathcal{B}$ 是有限的，而 $\mathcal{N}$ 有無限多個元素。在 $\mathcal{N}$ 中，某些元素也具有無限資訊內容，而在 $\mathcal{B}$ 中則不是如此。然而，我們可以在 $\mathcal{N}$ 中使用偏序來抽象地解釋我們所說的「有限近似」和「極限」。上面列出的序列在 $\mathcal{N}$ 中是有限的，因為它們只有有限多個與 $\perp$ 不同的坐標。給定任何 $x \in \mathcal{N}$，我們可以透過定義將其截斷為有限元素：

$(x | m)_n = \begin{cases} x_n, & \text{若 } n < m; \ \perp, & \text{若非。} \end{cases}$

從我們的定義中很容易看出

$x | m \sqsubseteq x | (m+1) \sqsubseteq x$，

因此 $x | m$ 正在「建立」到一個極限；事實上，這個極限就是原來的 $x$。我們將此寫作

$x = \bigsqcup_{m=0}^\infty (x | m)$，

其中 $\bigsqcup$ 是偏序集 $\mathcal{N}$ 中的上確界（sup 或 least-upper-bound）操作。關鍵是 $\mathcal{N}$ 有許多上確界；而且，只要我們在 $\mathcal{N}$ 中有元素 $y^{(n)}$（無論它們是否有限），我們就可以定義「極限」$z$，其中

$z = \bigsqcup_{n=0}^\infty y^{(n)}$

（提示：問自己 $z$ 的坐標必須是什麼。）我們不能在這裡重述細節，但 $\mathcal{N}$ 確實是一個拓撲空間，而 $z$ 確實是一個極限。因此，儘管 $\mathcal{N}$ 是無限的，但我們很有可能可以將操作歸結為有限操作，並能夠討論 $\mathcal{N}$ 以及更複雜領域上的可計算操作。

除了 $\mathcal{N}$ 上的序列和偏序結構之外，我們可以定義許多代數結構。這就是為什麼 $\mathcal{N}$ 是一個很好的例子。例如，在同構意義上，這個空間滿足

$\mathcal{N} \cong \mathcal{N} \times \mathcal{N}$

其中右邊表示通常的二元直積。抽象地說，領域 $\mathcal{N} \times \mathcal{N}$ 由所有有序對 $(x, y)$ 組成，其中 $x, y \in \mathcal{N}$，我們定義 $\sqsubseteq$ 在 $\mathcal{N} \times \mathcal{N}$ 上為

$(x, y) \sqsubseteq (x', y') \text{ 若且唯若 } x \sqsubseteq x' \text{ 且 } y \sqsubseteq y'$。

但實際上，將 $(x, y)$ 視為已經在 $\mathcal{N}$ 中的序列並無害處；實際上我們可以逐坐標地定義

$((x, y))n = \begin{cases} x{n/2}, & \text{若 } n \text{ 為偶數}; \ y_{(n-1)/2}, & \text{若 } n \text{ 為奇數。} \end{cases}$

上面的對之間 $\sqsubseteq$ 的準則將得到驗證，我們可以說 $\mathcal{N}$ 具有一個（雙射的）配對函數。

配對函數 $(., .)$ 在 $\mathcal{N}$ 上有許多有趣的性質，實際上我們已經注意到它是單調的（直觀地說：當你增加 $x$ 和 $y$ 的資訊內容時，你會增加 $(x, y)$ 的資訊內容）。更重要的是，$(., .)$ 是連續的，精確意義如下：

$(x, y) = \bigsqcup_{m=0}^\infty (x | m, y | m)$

這意味著 $(., .)$ 在取有限近似下表現良好。這只是一個例子；單調函數和連續函數的整個理論對於這種方法非常重要。

即使在我們對 $\mathcal{N}$ 施加的少量結構下，一種語言也應運而生。為了說明，我們集中討論 $\mathcal{N}$ 滿足的兩個同構；即 $\mathcal{N} \cong \mathcal{B}^\omega$ 和 $\mathcal{N} \cong \mathcal{N} \times \mathcal{N}$。第一個將 $\mathcal{N}$ 識別為與布林值（無限）序列有關：而第二個讓我們想起了上面關於配對函數的討論。在圖 2 中，我們給出了一個快速的 BNF 定義，定義了一種具有兩種表達式的語言：布林表達式 ($\beta$) 和序列表達式 ($\sigma$)。

圖 2. 一個簡短的語言。

$\beta$ ::= true | false | head $\sigma$ | if $\beta$ then $\sigma$' else $\sigma$''
$\sigma$ ::= $\beta$* | tail $\sigma$ | merge $\sigma$' $\sigma$''

這種語言確實非常簡潔：沒有變數，沒有宣告，沒有賦值，只有一個微小的常數項選擇。請注意，選擇的符號是為了使這些表達式的含義顯而易見。因此，如果 $\sigma$ 指稱一個序列 $x$，那麼 head sigma 必須指稱序列 $x$ 的第一個項 $x_0$。由於 $x_0 \in \mathcal{B}$ 且 $x \in \mathcal{N}$，我們保持了型別的一致。更精確地說，對於每個表達式，我們可以定義其（常數）值

$\llbracket . \rrbracket$，以便 $\llbracket \beta \rrbracket \in \mathcal{B}$ 對於布林表達式 $\beta$，以及 $\llbracket \sigma \rrbracket \in \mathcal{N}$ 對於序列表達式。由於 BNF 語言定義中有十條規則，我們需要寫下十個方程來完全指定這個例子的語義；我們這裡只給出選定的方程。繼續上一段的評論：

$\llbracket \text{head } \sigma \rrbracket = (\text{let } x = \llbracket \sigma \rrbracket \text{ in } x_0)$

另一方面，表達式 $\beta^*$ 創建一個布林值的無限序列：

$\llbracket \beta^* \rrbracket = (\llbracket \beta \rrbracket, \llbracket \beta \rrbracket, \llbracket \beta \rrbracket, \dots)$

（這種符號雖然粗糙，但很清楚。）同樣的道理：

$\llbracket \text{tail } \sigma \rrbracket = (\text{let } x = \llbracket \sigma \rrbracket \text{ in } (x_n)_{n=1}^\infty)$

而我們有

$\llbracket \text{merge } \sigma' \sigma'' \rrbracket = (\llbracket \sigma' \rrbracket, \llbracket \sigma'' \rrbracket)$.

這些應該足以說明這個想法。也應該清楚的是，我們這裡有的實際上只是一個選擇，因為 $\mathcal{N}$ 滿足更多同構（例如，$\mathcal{N} \cong \mathcal{N} \times \mathcal{N} \times \mathcal{N}$），並且還有更多拆分和重新組合布林值序列的方法——所有這些方法都是可計算的。

函數空間

不應斷定上一節包含了我的整個想法：這會讓我們停留在程式圖式 (program schemes) 的基本層次 (例如 van Emden-Kowalski [6] 或 Manna [8] (最後一章))。有些人稱之為「不動點語義學」(我自己不喜歡「不動點」這個縮寫詞) 只是第一章。第二章已經包含將程序作為參數的程序——高階程序——我們已經遠超程式圖式了。確實，不動點技術可以應用於這些高階程序，但這並不是支持它們的唯一理由。使這成為明確的語義結構是函數空間。我從 1969 年開始就試圖強調這一點，但許多人對我的理解不夠深入。

假設 $\mathcal{D}'$ 和 $\mathcal{D}''$ 是我們一直在討論的領域類型 (例如 $\mathcal{B}$ 或 $\mathcal{B} \times \mathcal{B}$ 或 $\mathcal{N}$ 或更糟的)。讓 $[\mathcal{D}' \to \mathcal{D}'']$ 表示所有將 $\mathcal{D}'$ 映射到 $\mathcal{D}''$ 的單調連續函數 $f$ 的領域。這就是我所說的函數空間。它在數學上並不那麼困難，但 $[\mathcal{D}' \to \mathcal{D}'']$ 再次成為一個「同類」領域（儘管結構更複雜）也並不那麼顯而易見。我不能在這裡證明它，但至少我可以定義 $\sqsubseteq$ 關係在函數空間上：

$f \sqsubseteq g \text{ 若且唯若 } f(x) \sqsubseteq g(x) \text{ 對所有 } x \in \mathcal{D}' \text{ 成立。}$

將函數視為抽象對象並非新鮮事；需要驗證的是它們也是相當合理的計算對象。函數空間 $[\mathcal{D}' \to \mathcal{D}'']$ 上的 $\sqsubseteq$ 關係是驗證這一點的第一步，它導向了一個行為良好的函數有限近似概念。(抱歉！這裡沒有時間更精確地說明。) 當這一點被理解後，函數空間的迭代之路就暢通無阻了；例如在 $[[\mathcal{D}''' \to \mathcal{D}''] \to \mathcal{D}']$ 中。這可能不像乍看之下那麼瘋狂，因為我們的理論將 $f(x)$ 識別為變數 $f$ 和變數 $x$ 的可計算二元函數。因此，作為一個操作，它可以被視為函數空間的一個元素：

$[[[\mathcal{D}' \to \mathcal{D}''] \times \mathcal{D}'] \to \mathcal{D}'']$.

這只是這些算子 (或組合子，Curry 和 Church 稱之為) 理論的開端。

接受所有這些後，讓我們嘗試從 $\mathcal{N}$ 開始進行函數空間的無限迭代。我們定義 $\mathcal{N}0 = \mathcal{N}$ 和 $\mathcal{N}{n+1} = [\mathcal{N}_n \to \mathcal{N}_n]$。因此 $\mathcal{N}_1 = [\mathcal{N} \to \mathcal{N}]$ 且 $\mathcal{N}_2 = [[[\mathcal{N} \to \mathcal{N}] \to \mathcal{N}] \to \mathcal{N}]$。你只需要相信我這一切都高度建構性（因為我們只使用連續函數）。

很清楚的是，這在自然意義上是累加的。首先，$\mathcal{N}$ 以子空間的形式「包含在」$[\mathcal{N} \to \mathcal{N}]$ 中：將每個 $x \in \mathcal{N}$ 與 $[\mathcal{N} \to \mathcal{N}]$ 中對應的常數函數識別。根據我們的定義，這顯然是一個保持序的對應關係。此外，每個 $f \in [\mathcal{N} \to \mathcal{N}]$ 都被一個常數（即 $f(\perp)$，這是所有值 $f(x)$ 中「最好」的元素）粗略地近似。這種子空間和近似之間的關係將表示為

$\mathcal{N} \sqsubseteq [\mathcal{N} \to \mathcal{N}]$。

往更高層次推，我們可以說

$[\mathcal{N} \to \mathcal{N}] \sqsubseteq [[\mathcal{N} \to \mathcal{N}] \to [\mathcal{N} \to \mathcal{N}]]$,

但這次是由於不同的原因。一旦我們確定了 $\mathcal{N} \sqsubseteq [\mathcal{N} \to \mathcal{N}]$ 的原因，我們就必須尊重更高層次 $\mathcal{N}_n$ 的函數空間結構。在特殊情況下，假設 $f \in [\mathcal{N} \to \mathcal{N}]$。我們想將 $f$ 注入到下一個空間中，所以稱其為 $i(f) \in [[\mathcal{N} \to \mathcal{N}] \to [\mathcal{N} \to \mathcal{N}]]$。如果 $g$ 是 $[\mathcal{N} \to \mathcal{N}]$ 中的任何元素，我們被要求定義 $i(f)(g) \in [\mathcal{N} \to \mathcal{N}]$。現在，由於 $g \in [\mathcal{N} \to \mathcal{N}]$，我們有原始的向後投影 $j(g) = g(\perp) \in \mathcal{N}$。因此，由於這是我們在 $\mathcal{N}$ 中能獲得的對 $g$ 的最佳近似，我們只能定義

$i(f)(g) = f(j(g))$。

這給出了下一個映射 $i: \mathcal{N}n \to \mathcal{N}{n+1}$。為了定義相應的投影 $j: \mathcal{N}_{n+1} \to \mathcal{N}_n$，我們以類似的方式論證並定義

$j(\phi)(x) = \phi(i(x))$,

其中 $\phi \in [[\mathcal{N} \to \mathcal{N}] \to [\mathcal{N} \to \mathcal{N}]]$, 且 $i(x) \in [\mathcal{N} \to \mathcal{N}]$ 是值為 $x$ 的常數函數。考慮到這個進展，定義 $i: \mathcal{N}n \to \mathcal{N}{n+1}$ 和 $j: \mathcal{N}_{n+1} \to \mathcal{N}_n$ 完全沒有問題。如此類推，精確地給出了累加的含義：

$\mathcal{N}_0 \sqsubseteq \mathcal{N}_1 \sqsubseteq \mathcal{N}_2 \sqsubseteq \dots \sqsubseteq \mathcal{N}n \sqsubseteq \mathcal{N}{n+1} \sqsubseteq \dots$.

有了這一切，不通過到極限（這次是空間的極限）將是遺憾的，這正是我希望你接受的。透過規定存在一個空間 $\mathcal{N}_\infty$，我們可以將其定義為所有 $\mathcal{N}_n$ 的聯合的完備化。由於各個階段如此互動：

$\mathcal{N}_{n+1} = [\mathcal{N}_n \to \mathcal{N}_n]$,

猜測

$\mathcal{N}\infty = [\mathcal{N}\infty \to \mathcal{N}_\infty]$

成立（至少在同構意義上）並不那麼奇怪。它確實成立，但我只能簡要說明這個同構的原因（和合理性）。首先，各個空間 $\mathcal{N}n$ 被放入了彼此內部，這不僅構成了一個空間之塔，而且還尊重了將組合 $\phi(x)$ 視為兩個變數的代數操作。$\mathcal{N}\infty$ 在精確意義上是 $\mathcal{N}n$ 的聯合的完備化；也就是說，在這些空間中，我們可以思考函數之塔，每個函數都近似於下一個（透過使用 $i$ 和 $j$ 映射），這樣在 $\mathcal{N}\infty$ 中，這些塔就有了極限。如果塔被截斷，那麼我們可以論證每個空間 $\mathcal{N}n \sqsubseteq \mathcal{N}\infty$。

現在為什麼 $\mathcal{N}\infty$ 上的同構成立？取一個在 $[\mathcal{N}\infty \to \mathcal{N}\infty]$ 中的函數（連續的！）。僅憑其連續性，它將由其對有限層次 $\mathcal{N}n$ 的作用決定。也就是說，它將在 $[\mathcal{N}n \to \mathcal{N}n] = \mathcal{N}{n+1}$ 中具有越來越好的近似；因此，這些近似「存在」於 $\mathcal{N}\infty$ 的有限層次中。它們的極限應該恰好將我們帶回到我們開始時的函數 $[\mathcal{N}\infty \to \mathcal{N}\infty]$。同樣，$\mathcal{N}\infty$ 中的任何元素都可以被視為空間 $[\mathcal{N}n \to \mathcal{N}n]$ 中近似函數的極限。誠然，還有細節需要驗證；但最終，$\mathcal{N}\infty$ 和 $[\mathcal{N}\infty \to \mathcal{N}\infty]$ 之間沒有真正的區別：無限高階函數的層次就是它自己的函數空間。（一如既往：這是連續性的結果。）

這裡潛藏著許多結構；事實上，比我最初想的要多。在圖 3 中，我說明了一個同構鏈，顯示 $\mathcal{N}\infty$ 繼承了許多我們已經熟悉的 $\mathcal{N}$ 的特徵。這些之所以有效的原因如下。首先，我們將 $\mathcal{N}\infty$ 視為一個函數空間。現在，函數對可以同構地與接受函數對作為值的函數對應。但是 $\mathcal{N}\infty \times \mathcal{N}\infty = \mathcal{N}\infty$，正如我們已經知道的。最後一步只是將 $\mathcal{N}\infty$ 上的函數放回到 $\mathcal{N}_\infty$ 的元素中。

圖 3. 第一個同構鏈。

$\mathcal{N}\infty \cong [\mathcal{N}\infty \to \mathcal{N}\infty]$ $\cong [\mathcal{N}\infty \to \mathcal{N}\infty] \times [\mathcal{N}\infty \to \mathcal{N}\infty]$ $\cong [\mathcal{N}\infty \to \mathcal{N}\infty \times \mathcal{N}\infty]$ $\cong [\mathcal{N}\infty \to \mathcal{N}\infty]$

利用圖 3 的同構，我們可以得到圖 4 所示的進一步結果。原因相當清楚。取一個從 $\mathcal{N}\infty$ 到 $\mathcal{N}\infty$ 的函數。這個函數的值可以被解釋為函數。但考慮到，一個其值為函數的函數恰好是（在空間同構意義上）一個二元函數。正如我們在圖 3 中所見，$\mathcal{N}\infty \times \mathcal{N}\infty = \mathcal{N}_\infty$，所以我們得到了最終的簡化（在同構意義上）。

圖 4. 第二個同構鏈。

$[\mathcal{N}\infty \to [\mathcal{N}\infty \to \mathcal{N}\infty]]$ $\cong [[\mathcal{N}\infty \times \mathcal{N}\infty] \to \mathcal{N}\infty]$ $\cong [\mathcal{N}\infty \to \mathcal{N}\infty]$

我們所做的是概述了為什麼 $\mathcal{N}\infty$，即無限型別函數的空間，是 λ 演算的模型。λ 演算是一種語言（這裡未顯示），其中每個項都可以被視為同時指稱一個參數（或值）和一個函數。形式細節相當簡單，但語義細節正是我們一直在探討的：空間 $\mathcal{N}\infty$ 的每個元素可以同時被視為空間 $[\mathcal{N}\infty \to \mathcal{N}\infty]$ 的一個元素；因此，$\mathcal{N}_\infty$ 提供了一個模型，但它只是眾多模型之一。

雖然無法明確說明，但我們為一種純程序語言（也包括圖 2 中的對和其他所有東西）概述了一種指稱（或數學）語義。在關於真實程式語言的參考資料中，添加了所有其他特性（賦值、序列、宣告等）。這些參考資料中已經證實，語義定義的方法確實有效。我希望你們會去研究它。

參考資料

  1. Böhm, C., 編. λ-Calculus and Computer Science Theory. Lecture Notes in Computer Science, Vol. 37, Springer-Verlag, New York, 1975.
  2. Clark, K.L., 和 Cowell, D.F. Programs, Machines, and Computation. McGraw-Hill, New York, 1976.
  3. Crossley, J.N., 編. Algebra and Logic. Papers from the 1974 Summer Res. Inst. Australian Math. Soc., Monash U. Clayton, Victoria, Australia. Lecture Notes in Mathematics, Vol. 450, Springer-Verlag, New York, 1975.
  4. Donahue, J.E. Complementary Definitions of Programming Language Semantics. Lecture Notes in Computer Science, Vol. 42, Springer-Verlag, 1976.
  5. Eilenberg, S. Automata, Languages, and Machines, Academic Press, New York, 1974.
  6. van Emden, M.H., 和 Kowalski, R.A. The semantics of predicate logic as a programming language. J. ACM 23, 4 (Oct. 1976), 733-742.
  7. Manes, E.G., 編. Category Theory Applied to Computation and Control. First Int. Symp. Lecture Notes in Computer Science, Vol. 25, Springer-Verlag, New York, 1976.
  8. Manna, Z. Mathematical Theory of Computation. McGraw-Hill, New York, 1974.
  9. Milne, R., 和 Strachey, C. A Theory of Programming Language Semantics. Chapman and Hall, London, and Wiley, New York, 2 Vols., 1976.
  10. Plotkin, G.D. A powerdomain construction. SIAM J. Comptng. 5 (1976), 452-487.
  11. Rabin, M.D., 和 Scott, D.S. Finite automata and their decision problems. IBM J. Res. and Develop. 3 (1959), 114-125.
  12. Scott, D.S. Data types as lattices. SIAM J. Comptng. 5 (1976), 522-587.
  13. Stoy, J.E. Denotational Semantics - The Scott-Strachey Approach to Programming Language Theory. M.I.T. Press, Cambridge, Mass. To appear.
  14. Tennent, R.D. The denotational semantics of programming languages. Comm. ACM 19, 8 (Aug. 1976), 437-453.