1977 ACM 圖靈獎演講

1977 年 ACM 圖靈獎於 10 月 17 日在西雅圖舉行的 ACM 年會上頒發給 John Backus。獎項委員會主席 Jean E. Sammet 在介紹獲獎者時發表了以下評論並宣讀了部分最終引文。完整公告刊載於《Communications》1977 年 9 月號第 681 頁。

「會議室裡可能沒有人沒聽過 Fortran，而且大多數人大概都至少使用過一次，或者至少看過別人在寫 Fortran 程式。可能也差不多一樣多人聽過 BNF 這三個字母，但不一定知道它們代表什麼。嗯，B 代表 Backus，其他字母在正式引文中解釋。在我看來，這兩項貢獻是電腦領域最重要的六項技術貢獻之一，並且都是由 John Backus 完成的（在 Fortran 的案例中也包括一些同事）。正因為這些貢獻，他獲得了今年的圖靈獎。

他的引文簡寫是為了「對實用高階程式設計系統的設計做出了深刻、有影響力且持久的貢獻，特別是透過他在 Fortran 上的工作，以及首次發布程式語言規範的形式化程序」。

完整引文中最重要的部分如下： 「... Backus 在 20 世紀 50 年代初期領導了一個在紐約市的 IBM 小組。該小組努力的最早期產品是一種用於科學和技術計算的高階語言，稱為 Fortran。同一個小組設計了第一個將 Fortran 程式翻譯成機器語言的系統。他們採用了新穎的優化技術來生成快速的機器語言程式。後來又開發了許多其他編譯器，首先是在 IBM 機器上，後來幾乎在所有品牌的電腦上都有。Fortran 於 1966 年被採納為美國國家標準。

在 20 世紀 50 年代後期，Backus 參與了制定 Algol 58 及後續版本 Algol 60 的國際委員會。Algol 語言及其衍生的編譯器在歐洲得到了廣泛接受，既作為開發程式的工具，也作為發布程式所依據演算法的一種形式化方式。

1959 年，Backus 在巴黎舉行的 UNESCO 會議上發表了一篇關於建議中的國際代數語言的語法和語義的論文。在這篇論文中，他首次採用了一種形式化技術來規範程式語言的語法。這種形式化符號後來被稱為 BNF——代表「Backus Normal Form」，或為了表彰丹麥 Peter Naur 的進一步貢獻而稱為「Backus Naur Form」。

因此，Backus 在電腦問題解決的實用世界以及人工語言與計算語言學之間的理論世界都做出了重大貢獻。Fortran 仍然是世界上使用最廣泛的程式語言之一。現在幾乎所有的程式語言都用某種形式化的語法定義來描述。」

程式設計能否擺脫 Von Neumann 風格？一個函式風格及其程式代數

John Backus IBM Research Laboratory, San Jose

授予個人讀者和為其服務的非營利圖書館，對本材料的全部或部分內容用於教學或研究的合理使用的一般權限，條件是必須給予 ACM 的版權聲明，並且提及出版物及其出版日期，以及經 Association for Computing Machinery 許可獲得轉載權的事實。否則，轉載圖、表格、其他實質性摘錄或全部作品，以及再出版或系統性或多次複製，都需要特定許可。

作者地址：91 Saint Germain Ave., San Francisco, CA 94114.

© 1978 ACM 0001-0782/78/0800-0613 $00.75

傳統程式語言變得越來越龐大，但並未變得更強大。其最基本層面的內在缺陷導致它們既臃腫又薄弱：它們繼承自共同祖先——Von Neumann 電腦——的原始逐字元程式設計風格，它們語義與狀態轉換緊密耦合，將程式設計分為表達式世界和語句世界，無法有效地利用強大的組合形式從現有程式構建新程式，以及缺乏用於程式推理的有用數學性質。

另一種函式程式設計風格建立在利用組合形式創建程式的基礎上。函式程式處理結構化資料，通常是非重複和非遞迴的，是層次化構建的，不命名其參數，也不需要複雜的程序聲明機制即可具有通用性。組合形式可以使用高階程式構建更高階的程式，這種風格在傳統語言中是不可能的。

函式程式設計風格與程式代數相關聯，程式代數的變數範圍涵蓋程式，其運算符是組合形式。這個代數可以用來轉換程式，並以一種與高中代數方程轉換非常相似的方式解決其「未知數」為程式的方程。這些轉換由代數法則給出，並在編寫程式的同一語言中進行。選擇組合形式不僅是因為它們的程式設計能力，也因為它們相關代數法則的能力。代數的通用定理給出了大類程式的詳細行為和終止條件。

一類新的計算系統在其程式語言和狀態轉換規則中都使用了函式程式設計風格。與 Von Neumann 語言不同，這些系統的語義與狀態鬆散耦合——每次主要計算只發生一次狀態轉換。

關鍵字詞和短語： 函式程式設計、程式代數、組合形式、函式形式、程式語言、Von Neumann 電腦、Von Neumann 語言、計算系統模型、應用式計算系統、應用式狀態轉換系統、程式轉換、程式正確性、程式終止、元組合 (metacomposition)

CR 分類： 4.20, 4.29, 5.20, 5.24, 5.26

介紹

我深切感謝 ACM 邀請我做 1977 年圖靈演講，並發布此報告，包含演講中承諾的細節。希望看到本文摘要的讀者請參閱最後一節，第 16 節。

1. 傳統程式語言：臃腫且鬆垮

程式語言似乎遇到了麻煩。每一種後繼語言都在清理後，納入了其前身的所有特性，再加上一些新的特性。有些語言的手冊超過 500 頁；其他語言則透過使用密集的符號系統，將複雜的描述塞進更短的手冊。國防部目前計劃由委員會設計一個語言標準，其手冊可能長達 1000 頁。每一種新語言都聲稱擁有一些新的時髦特性，例如強型別或結構化控制語句，但事實是，很少有語言能讓程式設計足夠便宜或更可靠，以證明其生產和學習使用成本是合理的。

由於尺寸的大幅增加只帶來能力的小幅提升，像 Pascal 這樣更小、更優雅的語言仍然很受歡迎。但是，我們迫切需要一種強有力的方法論來幫助我們思考程式，而沒有任何傳統語言能開始滿足這一需求。事實上，傳統語言在我們思考程式的方式上造成了不必要的混亂。

二十年來，程式語言一直在穩步走向其目前臃腫的狀態；結果，程式語言的研究和發明已經失去了很多興奮感。相反，它現在是那些喜歡處理厚厚的細節彙編而不是與新思想搏鬥的人的領域。關於程式語言的討論往往類似於關於多少天使能在針尖上跳舞的中世紀辯論，而不是關於根本不同概念之間的令人興奮的競爭。

許多有創造力的電腦科學家已經從發明語言轉向發明描述語言的工具。不幸的是，他們很大程度上滿足於將他們優雅的新工具應用於研究現有語言的疣和痣。在使用 Dana Scott 開發的優雅工具檢查了傳統語言令人震驚的型別結構後，令人驚訝的是，我們這麼多人仍然被動地滿足於這種結構，而不是積極地尋找新的結構。

本文的目的有兩個：首先，指出傳統語言框架中的基本缺陷使其表達能力的薄弱和癌性增長不可避免；其次，建議探索一些替代途徑，以設計新型語言。

2. 計算系統模型

每種程式語言背後都有一個由其程式控制的計算系統模型。有些模型是純粹的抽象，有些由硬體表示，有些則由編譯或解釋程式表示。在我們更仔細地研究傳統語言之前，簡要回顧現有模型作為當前替代方案世界的介紹是有用的。現有模型可以根據以下標準粗略分類。

2.1 模型準則

2.1.1 基礎。模型是否有優雅且簡潔的數學描述？這對證明模型行為的有用事實是否有用？或者模型是否過於複雜，以至於其描述冗長且數學上用途不大？

2.1.2 歷史敏感性。模型是否包含儲存概念，以便一個程式可以儲存資訊，這些資訊可以影響後續程式的行為？也就是說，模型是否具有歷史敏感性？

2.1.3 語義型別。程式是否連續轉換狀態（它們不是程式），直到達到終止狀態（狀態轉換語義）？狀態是簡單還是複雜？或者「程式」是否可以連續被化簡為更簡單的「程式」，以產生最終的「正規形式程式」，這是結果（化簡語義）？

2.1.4 程式的清晰度和概念性用途。模型的程式是否清晰地表達了過程或計算？它們是否體現了幫助我們 формулировать (formulate) 和 推理 (reason) 過程的概念？

2.2 模型分類

使用上述準則，我們可以粗略地描述計算系統模型的三個類別——簡單運算模型、應用式模型和 Von Neumann 模型。

2.2.1 簡單運算模型。範例：圖靈機、各種自動機。基礎：簡潔且有用。歷史敏感性：有儲存，具有歷史敏感性。語義：狀態轉換，狀態非常簡單。程式清晰度：程式不清晰且概念上無用。

2.2.2 應用式模型。範例：Church 的 lambda 演算 [5]、Curry 的組合子系統 [6]、純 Lisp [17]、本文描述的函式程式系統。基礎：簡潔且有用。歷史敏感性：無儲存，不具有歷史敏感性。語義：化簡語義，無狀態。程式清晰度：程式可以清晰且概念上很有用。

2.2.3 Von Neumann 模型。範例：Von Neumann 電腦、傳統程式語言。基礎：複雜、冗長、無用。歷史敏感性：有儲存，具有歷史敏感性。語義：狀態轉換，狀態複雜。程式清晰度：程式可以中等清晰，概念上用途不大。

上述分類坦率地說是粗糙且有爭議的。一些最近的模型可能不容易歸入這些類別中的任何一個。例如，Arvind 和 Gostelow [1]、Dennis [7]、Kosinski [13] 等人開發的資料流語言部分符合簡單運算模型類別，但它們的程式比該類別中早期模型的程式更清晰，而且或許可以爭辯說有些具有化簡語義。無論如何，這個分類將作為討論領域的粗略地圖。我們只關注應用式和 Von Neumann 模型。

3. Von Neumann 電腦

為了理解傳統程式語言的問題，我們必須首先研究它們的智力來源，Von Neumann 電腦。什麼是 Von Neumann 電腦？三十多年前，當 Von Neumann 和其他人構思它時，它是一個優雅、實用且統一的概念，簡化了當時存在的許多工程和程式設計問題。儘管產生其架構的條件已經發生了根本性變化，但我們仍然將「電腦」的概念與這個三十年前的概念聯繫在一起。

在最簡單的形式中，Von Neumann 電腦有三個部分：中央處理單元（或 CPU）、儲存裝置，以及一個連接管，可以在 CPU 和儲存裝置之間傳輸單個字元（並將位址發送到儲存裝置）。我建議將這根管子稱為 Von Neumann 瓶頸。程式的任務是以某種主要方式改變儲存裝置的內容；考慮到這項任務必須完全透過在 Von Neumann 瓶頸來回泵送單個字元來完成時，它的名稱就清楚了。

諷刺的是，瓶頸中的大部分流量不是有用的資料，而只是資料的名稱，以及僅用於計算這些名稱的運算和資料。在一個字元可以通過管子傳輸之前，它的位址必須在 CPU 中；因此它必須要么通過管子從儲存裝置傳送，要么由 CPU 的某些運算產生。如果位址是從儲存裝置傳送的，那麼它的位址必須要么是從儲存裝置傳送的，要么是在 CPU 中產生的，依此類推。另一方面，如果位址是在 CPU 中產生的，它必須要么由固定規則（例如，「程式計數器加 1」），要么由通過管子傳送的指令產生，在這種情況下，它的位址必須已經被傳送...依此類推。

當然，應該有比通過 Von Neumann 瓶頸來回推動大量字元，以對儲存裝置進行重大更改更不原始的方式。這根管子不僅是問題資料流量的字面意義上的瓶頸，而且更重要的是，它是一個智力瓶頸，使我們一直束縛在逐字元思考，而不是鼓勵我們以手頭任務的更大概念單元來思考。因此，程式設計基本上是在規劃和細述通過 Von Neumann 瓶頸的大量字元流量，而其中大部分流量關心的是尋找資料，而不是資料本身。

4. Von Neumann 語言

傳統程式語言基本上是 Von Neumann 電腦的高階、複雜版本。我們三十年前的信念，認為只有一種電腦，是我們相信只有一種程式語言——傳統的 Von Neumann 語言——的基礎。儘管 Fortran 和 Algol 68 之間存在相當大的差異，但它們都基於 Von Neumann 電腦的程式設計風格這一事實，使得這些差異顯得不那麼重要。儘管我將傳統語言稱為「Von Neumann 語言」以記錄它們的起源和風格，但我當然不因此指責這位偉大的數學家造成了它們的複雜性。事實上，有些人可能會說我對此負有一些責任。

Von Neumann 程式語言使用變數來模仿電腦的儲存單元；控制語句擴充其跳轉和測試指令；指派語句模仿其讀取、儲存和算術運算。指派語句是程式語言的 Von Neumann 瓶頸，它讓我們以逐字元的方式思考，就像電腦的瓶頸一樣。

考慮一個典型的程式；其核心是許多包含帶下標變數的指派語句。每個指派語句產生一個單字元的結果。程式必須使這些語句重複執行多次，同時修改下標值，以便對儲存裝置進行所需的整體更改，因為它必須逐字元完成。因此，程式設計師在設計用於實現必要重複的控制語句巢狀結構時，關心的是通過指派瓶頸的字元流動。

此外，指派語句將程式設計分為兩個世界。第一個世界包含指派語句的右側。這是一個有序的表達式世界，一個具有有用代數性質的世界（除了這些性質經常被副作用破壞）。這是大多數有用計算發生的世界。

傳統程式語言的第二個世界是語句的世界。該世界中主要的語句是指派語句本身。語言中所有其他語句的存在是為了使基於這種原始構建——指派語句——的計算成為可能。這個語句世界是無序的，幾乎沒有有用的數學性質。結構化程式設計可以被看作是一種引入秩序到這個混沌世界的溫和努力，但它在解決由 Von Neumann 程式設計的逐字元風格所產生的根本問題上收效甚微，其原始使用迴圈、下標和分支控制流。

我們對 Von Neumann 語言的固守使得 Von Neumann 電腦的至上地位得以延續，而我們對它的依賴使得非 Von Neumann 語言變得不經濟，並限制了它們的發展。缺乏基於非 Von Neumann 原則的全面、有效的程式設計風格，使得設計師們缺乏新的電腦架構的智力基礎。（有關該主題的簡要討論，請參閱第 15 節。）

應用式計算系統缺乏儲存和歷史敏感性是它們未能為電腦設計提供基礎的根本原因。此外，大多數應用式系統使用 lambda 演算的替換運算作為其基本運算。這種運算具有幾乎無限的能力，但其完整且高效的實現對機器設計師來說存在巨大的困難。此外，為了引入儲存並提高其在 Von Neumann 電腦上的效率，應用式系統傾向於被一個大型 Von Neumann 系統吞噬。例如，純 Lisp 常常被埋在許多具有 Von Neumann 特性的大型擴充中。由此產生的複雜系統為機器設計師提供的指導很少。

5. Von Neumann 程式與函式程式的比較

為了更詳細地了解 Von Neumann 語言的一些缺陷，讓我們比較一個用於內積的傳統程式和一個用稍後將詳細介紹的簡單語言編寫的函式程式。

5.1 一個用於內積的 Von Neumann 程式

c ← 0
for i ← 1 step 1 until n do
  c ← c + a[i] × b[i]

這個程式的幾個性質值得注意： a) 它的語句根據複雜的規則作用於一個不可見的「狀態」。 b) 它不是層次化的。除了指派語句的右側，它不從更簡單的實體構建複雜實體。（然而，較大的程式通常會這樣做。） c) 它是動態且重複的。必須在腦中執行它才能理解它。 d) 它透過重複（指派語句）和修改（變數 i）逐字元計算。 e) 部分資料 n 在程式中；因此它缺乏通用性，只對長度為 n 的向量起作用。 f) 它命名了其參數；它只能用於向量 a 和 b。為了具有通用性，它需要一個程序聲明。這涉及複雜的問題（例如，傳值呼叫與傳名呼叫）。 g) 它的「內務處理」(housekeeping) 運算由分散在不同地方的符號表示（在 for 語句和指派語句中的下標）。這使得將內務處理運算，即最常見的運算，整合到單一、強大、廣泛有用的運算符中成為不可能。因此，在編寫這些運算時，人們總是必須從頭開始，寫「for i ← ...」和「for j ← ...」，後跟散佈著 i 和 j 的指派語句。

5.2 一個用於內積的函式程式

Def Innerproduct = (Insert +)o(ApplyToAll ×)oTranspose

或者，縮寫形式：

Def IP = (/+)o(@x)oTrans.

組合 (o)、插入 (/) 和應用到所有 (@) 是函式形式，它們將現有函式組合起來形成新的函式。因此，fog 是透過先應用 g 再應用 f 獲得的函式，@f 是將 f 應用於參數的每個成員獲得的函式。如果我們寫 f:x 表示將 f 應用於物件 x 的結果，那麼我們可以解釋將 Innerproduct 應用於向量對 <<1, 2, 3>, <6, 5, 4>> 的每個步驟如下：

IP:<<1,2,3>, <6,5,4>>

Definition of IP (IP 的定義)

= (/+)o(@x)oTrans: <<1,2,3>, <6,5,4>>

Effect of composition, o (組合 o 的效果)

= (/+):((@x):(Trans: <<1,2,3>, <6,5,4>>))

Applying Transpose (應用 Transpose)

= (/+):((@x): <<1,6>, <2,5>, <3,4>>)

Effect of ApplyToAll, @ (應用到所有 @ 的效果)

= (/+): <x:<1,6>, ×:<2,5>, x:<3,4>>

Applying x (應用 ×)

= (/+): <6,10,12>

Effect of Insert, / (插入 / 的效果)

= +: <6, +:<10,12>>

Applying + (應用 +)

= +: <6,22>

Applying + again (再次應用 +)

= 28

讓我們將這個程式的性質與 Von Neumann 程式的性質進行比較。 a) 它只作用於其參數。沒有隱藏的狀態或複雜的轉換規則。只有兩種規則，一種是將函式應用於其參數，另一種是在知道函式 f 和 g，即形式的參數時，獲得由功能形式（如組合 fog 或應用到所有 @f）表示的函式。 b) 它是層次化的，由三個更簡單的函式（+、x、Trans）和三個函式形式（fog、@f 和 /f）構成。 c) 它是靜態且非重複的，從結構上有助於理解它，而無需在腦中執行。例如，如果理解形式 fog 和 @f 以及函式 x 和 Trans 的作用，那麼也就理解 @x 和 (@x)oTrans 的作用，依此類推。 d) 它作用於整個概念單元，而不是字元；它有三個步驟；沒有步驟重複。 e) 它不包含任何資料；它是完全通用的；它適用於任何一對匹配的向量。 f) 它不命名其參數；它可以應用於任何一對向量，無需任何程序聲明或複雜的替換規則。 g) 它使用了在許多其他程式中通用的內務處理形式和運算符（例如，@f、distl、distr、trans）；事實上，只有 + 和 x 與內務處理無關。這些形式和函式可以與其他形式和函式組合，創建更高層次的內務處理運算符。

第 14 節概述了一種旨在使上述函式程式設計風格在具有簡單框架的歷史敏感系統中可用的系統；但是，在上述應用式風格可以成為優雅實用程式語言的基礎之前，仍有許多工作要做。目前，上述比較展示了 Von Neumann 程式語言的許多嚴重缺陷，可以作為解釋其目前臃腫狀態的起點。

6. 語言框架與可變換部分

讓我們區分程式語言的兩個部分。首先是其框架，它給出了系統的整體規則；其次是其可變換部分，其存在由框架預期，但其特定行為不受框架指定。例如，for 語句和幾乎所有其他語句是 Algol 框架的一部分，但函式庫函式和使用者定義的程序是可變換部分。因此，語言的框架描述了其固定特性，並為其可變換特性提供了通用環境。

現在假設一個語言有一個很小的框架，它可以完全作為可變換部分容納各種強大特性。那麼這樣的框架就可以支持許多不同的特性和風格，而無需改變自身。與這種愉快的可能性相反，Von Neumann 語言似乎總是擁有巨大的框架和非常有限的可變換部分。為什麼會這樣？答案涉及到 Von Neumann 語言的兩個問題。

第一個問題源於 Von Neumann 的逐字元程式設計風格，它要求字元來回流動到狀態，就像通過 Von Neumann 瓶頸的流量一樣。因此，Von Neumann 語言必須具有與狀態緊密耦合的語義，其中計算的每一個細節都改變狀態。這種與狀態緊密耦合的語義的結果是，每個特性的每一個細節都必須被構建到狀態及其轉換規則中。

因此，Von Neumann 語言的每個特性都必須在其框架中以令人發麻的細節來闡述。此外，需要許多複雜的特性來支撐其基本上薄弱的逐字元風格。結果就是 Von Neumann 語言不可避免的僵硬而巨大的框架。

7. 可變換部分與組合形式

Von Neumann 語言的第二個問題是它們的可變換部分表達能力太弱。它們龐大的尺寸就是雄辯的證據；畢竟，如果設計師知道所有這些複雜的特性（他現在構建到框架中）以後可以作為可變換部分添加，他就不會如此熱衷於將它們構建到框架中。

也許提供強大可變換部分最重要的元素是提供通用的組合形式，可以用來從舊程序構建新程序。Von Neumann 語言只提供原始的組合形式，而且 Von Neumann 框架阻礙了它們的充分利用。

使用組合形式的一個障礙是 Von Neumann 語言中表達式世界和語句世界的分裂。函式形式自然屬於表達式世界；但無論它們多強大，它們只能構建產生單字元結果的表達式。而這些單字元結果必須在語句世界中組合成最終的結果。組合單個字元並非我們真正應該思考的事情，但在 Von Neumann 語言中編寫任何任務的程式，這是一大部分工作。為了幫助從單個字元組合出整體結果，這些語言在語句世界中提供了一些原始的組合形式——for、while 和 if-then-else 語句——但是這兩個世界的分裂阻止了任何一個世界中的組合形式發揮其在一個統一世界中可以達到的全部力量。

Von Neumann 語言中使用組合形式的第二個障礙是它們使用了繁複的命名約定，這些約定因呼叫程序所需的替換規則而變得更加複雜。每一個都需要一個複雜的機制構建到框架中，以便變數、帶下標變數、指針、檔名、程序名、傳值形式參數、傳名形式參數等等都能正確解釋。所有這些名稱、約定和規則干擾了簡單組合形式的使用。

8. APL 與逐字元程式設計

既然我對逐字元程式設計說了這麼多，我現在必須說說 APL [12]。我們要歸功於 Kenneth Iverson，他向我們展示了有些程式既不是逐字元也不是依賴 lambda 表達式，並向我們介紹了使用新的函式形式。由於 APL 指派語句可以儲存陣列，其函式形式的效果擴展到單個指派語句之外。

然而，不幸的是，APL 仍然將程式設計分割為表達式世界和語句世界。因此，編寫單行程式的努力部分是出於留在更有序的表達式世界的願望。APL 只有三種函式形式，稱為內積、外積和化簡。這些有時難以使用，數量不夠，而且它們的使用僅限於表達式世界。

最後，APL 的語義仍然與狀態耦合得太緊密。因此，儘管語言更簡單、更強大，其框架仍具有 Von Neumann 語言的複雜性和僵硬性特徵。

9. Von Neumann 語言缺乏有用的數學性質

到目前為止，我們已經討論了 Von Neumann 語言的整體尺寸和僵化；另一個重要的缺陷是它們缺乏有用的數學性質以及它們對程式推理造成的障礙。儘管關於程式證明已發表了大量優秀著作，但 Von Neumann 語言幾乎沒有任何在這方面有幫助的性質，卻有許多阻礙（例如，副作用、別名）。

指稱語義 [23] 及其基礎 [20, 21] 為程式中隱含的域和函式空間提供了極其有用的數學理解。當應用於應用式語言（如 [16] 中的「遞迴程式」）時，其基礎提供了強大的工具來描述語言和證明程式的性質。另一方面，當應用於 Von Neumann 語言時，它提供了精確的語義描述，並有助於識別語言中的問題區域。但是，語言的複雜性反映在描述的複雜性中，這是一個令人困惑的產生式、域、函式和方程式的集合，在證明程式性質方面僅比語言參考手冊稍微有用一些，因為它較不模糊。

公理語義 [11] 精確地重述了 Von Neumann 程式不夠優雅的性質（即狀態轉換）作為謂詞轉換。逐字元、重複的遊戲並未因此改變，只是場地變了。證明 Von Neumann 程式性質的這種公理遊戲的複雜性使得其從業者獲得的成功更加令人欽佩。他們的成功建立在除了他們的獨創性之外的兩個因素上：首先，遊戲被限制在完整 Von Neumann 語言的小而弱的子集，這些子集具有遠比真實狀態簡單得多的狀態。其次，新的場地（謂詞及其轉換）比舊的（狀態及其轉換）更豐富、更有序且更有效。但是限制遊戲並將其轉移到更有效的領域並不能使其處理真實程式（具有程序呼叫和別名所必需的複雜性），也不能消除基本 Von Neumann 風格的笨拙性質。隨著公理語義擴展以涵蓋更多典型的 Von Neumann 語言，它開始隨著所需複雜性的增加而失去其有效性。

因此，指稱語義和公理語義是描述性形式主義，其基礎體現了優雅而強大的概念；但是使用它們來描述 Von Neumann 語言不可能產生一種優雅而強大的語言，就像使用優雅而現代的機器製造 Edsel 車一樣，不可能產生一輛優雅而現代的汽車。

無論如何，程式證明使用邏輯語言，而不是程式設計語言。證明談論程式，但不能直接涉及它們，因為 Von Neumann 語言的公理是如此難以使用。相比之下，許多普通證明是通過代數方法得出的。這些方法需要具有某些代數性質的語言。然後，代數法則可以以一種相當機械的方式將問題轉化為其解決方案。例如，要解決方程

ax + bx = a + b

（假設 a+b ≠ 0）中的 x，我們依次機械地應用分配律、恆等律和消去律，得到

(a + b)x = a + b
(a + b)x = (a + b) 1
x = 1.

因此，我們證明了 x = 1 而沒有離開代數的「語言」。Von Neumann 語言及其怪異的語法，很少提供這樣的程式轉換可能性。

正如我們稍後將看到的，程式可以用具有相關代數的語言來表達。這個代數可以用來轉換程式，並以與高中代數求解方程非常相似的方式，求解其「未知數」為程式的一些方程。代數轉換和證明使用程式本身的語言，而不是談論程式的邏輯語言。

10. Von Neumann 語言的替代方案是什麼？

在討論 Von Neumann 語言的替代方案之前，讓我說我對上述關於這些語言的負面且不夠精確的討論感到遺憾。但是，我們大多數人對這些巨大、薄弱語言的自滿接受長期以來一直困擾著我。我感到困擾，因為這種接受花費了巨大的努力去使 Von Neumann 語言變得更臃腫，這些努力本可以更好地用於尋找新的結構。因此，我試圖分析傳統語言的一些基本缺陷，並表明這些缺陷無法解決，除非我們發現一種新的語言框架。

在尋找傳統語言的替代方案時，我們必須首先認識到，一個系統除非具有某種狀態（第一個程式可以改變，第二個程式可以存取），否則它不能具有歷史敏感性（允許一個程式的執行影響後續程式的行為）。因此，計算系統的歷史敏感模型必須具有狀態轉換語義，至少在這個弱意義上是如此。但這並不意味著每一次計算都必須嚴重依賴一個複雜的狀態，並且計算的每一個小部分都需要許多狀態變化（如 Von Neumann 語言）。

為了說明 Von Neumann 語言的一些替代方案，我建議概述一類歷史敏感的計算系統，其中每個系統：a) 具有鬆散耦合的狀態轉換語義，其中狀態轉換僅在一次主要計算中發生一次；b) 具有簡單結構的狀態和簡單的轉換規則；c) 嚴重依賴底層應用式系統，既提供系統的基本程式語言，也描述其狀態轉換。

我將這些系統稱為應用式狀態轉換 (AST) 系統，它們在第 14 節中描述。這些簡單系統避免了 Von Neumann 語言的許多複雜性和弱點，並提供了一套強大而廣泛的可變換部分。然而，它們僅被概述為具有各種吸引人性質的廣大非 Von Neumann 系統領域的粗略範例。我過去三四年一直在研究這個領域，但尚未找到一個令人滿意的解決方案，來解決優秀語言必須解決的許多衝突要求。但我相信這項研究已經指明了一種設計非 Von Neumann 語言的有用方法。

這種方法包含四個要素，可以總結如下。 a) 無變數的函式程式設計風格。描述了一個簡單、非正式的函式程式設計 (FP) 系統。它基於使用組合形式來構建程式。給出了一些程式來闡述函式程式設計。 b) 函式程式的代數。描述了一個代數，其變數表示 FP 函式程式，其「運算」是 FP 函式形式，即 FP 程式的組合形式。給出了一些代數法則。給出定理和範例，展示如何將某些函式表達式轉換為等價的無限展開式，解釋函式的行為。將 FP 代數與 Church 和 Curry 的古典應用式系統相關聯的代數進行比較。 c) 形式化函式程式系統。描述了一個形式化 (FFP) 系統，它擴展了上述非正式 FP 系統的功能。因此，FFP 系統是一個精確定義的系統，它提供了使用 FP 系統的函式程式設計風格及其程式代數的能力。FFP 系統可以用作應用式狀態轉換系統的基礎。 d) 應用式狀態轉換系統。如上所述。本文的其餘部分將描述這四個要素，簡要論述電腦設計，最後以本文總結結束。

11. 函式程式系統 (FP Systems)

11.1 介紹

本節將非正式地描述一類稱為函式程式 (FP) 系統的簡單應用式程式設計系統，其中「程式」只是沒有變數的函式。描述後將給出一些範例，並討論 FP 系統的各種性質。

FP 系統建立在固定組合形式（稱為函式形式）的基礎上。這些形式，加上簡單的定義，是從現有函式或物件構建新函式的唯一手段；它們不使用變數或替換規則，並且成為相關程式代數的運算。FP 系統的所有函式都屬於同一型別：它們將物件映射到物件，並且總是接受一個單一參數。

相比之下，基於 lambda 演算的系統建立在 lambda 表達式的基礎上，並伴隨一組用於變數的替換規則，用於構建新函式。Lambda 表達式（及其替換規則）能夠定義所有可能型別和任意參數數量的所有可能可計算函式。這種自由和能力既有明顯優勢，也有缺點。它類似於傳統語言中無限制控制語句的能力：無限制的自由帶來混亂。如果像在 lambda 演算中一樣不斷發明新的組合形式來適應場合，人們將不會熟悉足以用於所有目的的少數組合形式的風格或有用性質。正如結構化程式設計捨棄許多控制語句以獲得結構更簡單、性質更好、理解行為的方法統一的程式一樣，函式程式設計也捨棄 lambda 表達式、替換和多個函式型別。它因此獲得了使用熟悉、具有已知有用性質的函式形式構建的程式。這些程式結構如此，以至於它們的行為通常可以通過類似於解決高中代數問題的代數技術的機械使用來理解和證明。

函式形式，不像大多數程式構建，不需要隨意選擇。由於它們是相關代數的運算，人們只選擇那些不僅提供強大程式設計構建，而且具有吸引人代數性質的函式形式：選擇它們是為了最大化其與系統中其他函式形式相關聯的代數法則的強度和效用。

在下面的描述中，我們將不精確地區分 (a) 函式符號或表達式和 (b) 它所表示的函式。我們將通過範例和用法來表示用於表示函式的符號和表達式。第 13 節描述了 FP 系統的形式化擴展 (FFP 系統)；它們可以用來澄清關於 FP 系統的任何模糊之處。

11.2 描述

一個 FP 系統包含以下：

  1. 一組 O 的物件；
  2. 一組 F 的函式 f，它們將物件映射到物件；
  3. 一個運算，應用；
  4. 一組 F 的函式形式；這些用於組合現有函式或物件以形成 F 中的新函式；
  5. 一組 D 的定義，它們定義 F 中的一些函式並為每個函式分配一個名稱。

下面是非正式描述上述每個實體及其範例。

11.2.1 物件，O。物件 x 是原子、元素 xi 是物件的序列 <x1, ..., xn>，或 ±（「底」或「未定義」）。因此，原子集合 A 的選擇決定了物件集合。我們將 A 視為由大寫字母、數字和 FP 系統符號約定不使用的特殊符號組成的非空字串集合。其中一些字串屬於稱為「數字」的原子類別。原子 ~ 用於表示空序列，並且是唯一既是原子又是序列的物件。原子 T 和 F 用於表示「真」和「假」。

物件的建構有一個重要限制：如果 x 是包含 ± 作為元素的序列，則 x = ±。也就是說，「序列構造子」是「±-保留的」。因此，沒有正常序列包含 ± 作為元素。

物件範例

±
1.5
A B 3
<AB, 1, 2.3>
<φ, 4, <<B>, C>, D>
<φ, 4, ±> = ±

11.2.2 應用。FP 系統有一個單一運算，應用。如果 f 是一個函式，x 是一個物件，那麼 f:x 是一個應用，表示將 f 應用於 x 的結果物件。f 是應用的運算符，x 是操作數。

應用範例

+:<1,2> = 3
tl:<A,B,C> = <B,C>
1:<A,B,C> = A
2:<A,B,C> = B

11.2.3 函式，F。F 中的所有函式 f 都將物件映射到物件，並且都是底保留的：對於 F 中的所有 f，f± = ±。F 中的每個函式要麼是原始的（系統提供的），要麼是定義的（見下），要麼是函式形式（見下）。

有時區分 f:x = ± 的兩種情況很有用。如果 f:x 的計算終止並產生物件 ±，我們說 f 在 x 處未定義，即 f 終止但在 x 處沒有有意義的值。否則我們說 f 在 x 處非終止。

原始函式範例 我們的意圖是為 FP 系統提供廣泛有用且強大的原始函式，而不是那些需要定義有用函式的弱函式。以下範例定義了一些典型的原始函式，其中許多用於後面的程式範例。在以下定義中，我們使用 McCarthy 條件表達式的變體 [17]；因此我們寫

p1 → e1; ... ; pn → en; en+1

代替 McCarthy 表達式

(p1 → e1, ..., pn → en, T → en+1).

以下定義對所有物件 x, xi, y, yi, z, zi 都成立：

選擇函式

1:x = x=<x1, ..., xn> → x1; ±

對於任何正整數 s

s:x = x=<x1, ..., xn> & n≥s → xs; ±

因此，例如 3:<A,B,C> = C 且 2: = ±。注意函式符號 1, 2 等與原子 1, 2 等不同。

尾部

tl:x = x=<x1> → φ; x=<x1, ..., xn> & n≥2 → <x2, ..., xn>; ±

恆等

id:x = x

原子

atom:x = x is an atom → T; x≠± → F; ±

等於

eq:x = x=<y,z> & y=z → T; x=<y,z> & y≠z → F; ±

空

null:x = x=φ → T; x≠± → F; ±

反轉

reverse:x = x=φ → φ; x=<x1, ..., xn> → <xn, ..., x1>; ±

從左分發；從右分發

distl:x = x=<y,φ> → φ; x=<y,<z1, ..., zn>> → <<y, z1>, ..., <y, zn>>; ±
distr:x = x=<φ,y> → φ; x=<<y1, ..., yn>,z> → <<y1,z>, ..., <yn,z>>; ±

長度

length:x = x=<x1, ..., xn> → n; x=φ → 0; ±

加、減、乘、除

+:x = x=<y,z> & y,z are numbers → y+z; ±
-:x = x=<y,z> & y,z are numbers → y-z; ±
x:x = x=<y,z> & y,z are numbers → y×z; ±
%:x = x=<y,z> & y,z are numbers → y/z; ± (where y/0 = ±)

轉置

trans:x = x=<φ, ..., φ> → φ; x=<x1, ..., xn> → <y1, ..., ym>; ±

其中 xi=<xi1, ..., xim> 且 yj=<x1j, ..., xnj>, 1≤i≤n, 1≤j≤m.

與、或、非

and:x = x=<T,T> → T; x=<T,F> ∨ x=<F,T> ∨ x=<F,F> → F; ±

等等。

左追加；右追加

apndl:x = x=<y,φ> → <y>; x=<y,<z1, ..., zn>> → <y, z1, ..., zn>; ±
apndr:x = x=<φ,z> → <z>; x=<<y1, ..., yn>,z> → <y1, ..., yn,z>; ±

右選擇；右尾部

lr:x = x=<x1, ..., xn> → xn; ±
2r:x = x=<x1, ..., xn> & n≥2 → xn-1; ±

等等。

tlr:x = x=<x1> → φ; x=<x1, ..., xn> & n≥2 → <x1, ..., xn-1>; ±

左旋轉；右旋轉

rotl:x = x=φ → φ; x=<x1> → <x1>; x=<x1, ..., xn> & n≥2 → <x2, ..., xn,x1>; ±

等等。

11.2.4 函式形式，F。函式形式是表示函式的表達式；該函式依賴於作為表達式參數的函式或物件。因此，例如，如果 f 和 g 是任何函式，那麼 fog 是一個函式形式，f 和 g 的組合，f 和 g 是它的參數，它表示這樣的函式：對於任何物件 x，

(fog):x = f:(g:x).

一些函式形式可以將物件作為參數。例如，對於任何物件 x，x 是一個函式形式，x 的常數函式，因此對於任何物件 y，

_x_:y = y=± → ±; x.

特別地，± 是處處為 ± 的函式。

下面我們給出一些函式形式，其中許多在本文後面用於程式範例。我們使用帶下標和不帶下標的 p、f 和 g 表示任意函式；並將 x、x1, ..., xn、y 作為任意物件。方括號 [...] 用於表示構造函式形式，它表示一個函式，而尖括號 <...> 表示序列，它們是物件。圓括號既用於特定函式形式（例如 condition 中），也通常用於表示分組。

組合

(fog):x = f:(g:x)

構造

[f1, ..., fn]:x = <f1:x, ..., fn:x>

（記住 <..., ±, ...> = ± 且所有函式都是 ± 保留的，因此 [f1, ..., fn] 也是）。

條件

(p → f, g):x = (p:x)=T → f:x; (p:x)=F → g:x; ±

條件表達式（在 FP 系統之外用於描述其函式）和函式形式 condition 都由「→」標識。它們截然不同但密切相關，如上述定義所示。但不會引起混淆，因為條件表達式的元素都表示值，而函式形式 condition 的元素都表示函式，從不表示值。當沒有歧義時，我們省略右關聯的圓括號；例如，我們寫 p1 → f1; p2 → f2; g 表示 (p1 → f1; (p2 → f2; g))。

常數（此處 x 是物件參數。）

_x_:y = y=± → ±; x

插入

/f:x = x=<x1> → x1; x=<x1, ..., xn> & n≥2 → f:<x1, /f:<x2, ..., xn>>; ±

如果 f 有一個唯一的右單位元 ur ≠ ±，其中對於所有物件 x，f:<x,ur> = {x, ±}，則上述定義擴展為 /f:φ = ur。因此

/+:<4,5,6> = +:<4, +:<5, /+:<6>>> = +:<4, +:<5,6>> = 15
/+ :φ = 0

應用到所有

@f: x = x=φ → φ; x=<x1, ..., xn> → <f:x1, ..., f:xn>; ±

二元轉一元（x 是物件參數）

(bu f x):y = f:<x,y>

因此

(bu + 1):x = 1+x

當...時 (While)

(while p f):x = p:x=T → (while p f):(f:x); p:x=F → x; ±

上述函式形式提供了一種有效的方法來計算它們所表示的函式的值（如果它們終止），前提是可以有效地應用它們的函式參數。

11.2.5 定義。FP 系統中的定義是形式為

Def l = r

的表達式，其中左側 l 是未使用的函式符號，右側 r 是函式形式（可能依賴於 l）。它表達了符號 l 將表示由 r 給出的函式的事實。因此，定義 Def lastl = lorreverse 定義了函式 lastl，它產生序列的最後一個元素（或 ±）。類似地，

Def last = nullotl → 1; lastotl

定義了函式 last，它與 lastl 相同。以下是詳細說明如何使用定義計算 last: <1,2> 的過程：

last: <1,2>

definition of last (last 的定義)

= (nullotl → 1; lastotl):<1,2>

action of the form (p→f, g) (形式 (p→f, g) 的作用)

= lastotl:<1,2> since nullotl:<1,2> = null:<2> = F

action of the form fog (形式 fog 的作用)

= last:(tl:<1,2>)

definition of primitive tail (原始 tail 的定義)

= last:<2>

definition of last (last 的定義)

= (nullotl → 1; lastotl):<2>

action of the form (p→f, g) (形式 (p→f, g) 的作用)

= 1:<2> since nullotl:<2> = null:φ = T

definition of selector 1 (選擇器 1 的定義)

= 2

上面說明了簡單規則：應用已定義的符號時，用其定義的右側替換它。當然，一些定義可能定義非終止的函式。一組定義 D 是良好形成的，如果沒有兩個左側相同。

11.2.6 語義。從上面可以看出，一個 FP 系統由以下集合的選擇決定：(a) 原子集合 A（決定了物件集合）。(b) 原始函式集合 P。(c) 函式形式集合 F。(d) 一個良好形成的定義集合 D。要理解這樣一個系統的語義，需要知道如何計算任何函式 f 和任何物件 x 的 f:x。對於 f 恰好有四種可能性： (1) f 是原始函式； (2) f 是函式形式； (3) D 中有一個定義，Def f = r；以及 (4) 以上皆非。 如果 f 是原始函式，則有其描述並知道如何應用它。如果 f 是函式形式，則形式的描述告訴如何根據形式的參數計算 f:x，這可以通過進一步使用這些規則來完成。如果 f 已定義，Def f = r，如 (3) 中所示，則要找到 f:x，計算 r:x，這可以通過進一步使用這些規則來完成。如果這些都不是，則 f:x = ±。當然，使用這些規則對某些 f 和某些 x 可能不會終止，在這種情況下，我們賦值 f:x = ±。

11.3 函式程式範例

以下範例說明了函式程式設計風格。由於這種風格對大多數讀者來說不太熟悉，起初可能會引起困惑；需要記住的重要一點是，函式定義的任何部分本身都不是結果。相反，每個部分都是必須應用於參數才能獲得結果的函式。

11.3.1 階乘。

Def ! = eq0 → 1; xo[id, !osubl]

其中

Def eq0 = eqo[id, _0_]
Def subl = -o[id, _1_]

以下是 FP 系統在評估 !: 2 時會獲得的一些中間表達式：

!:2
= (eq0 → 1; xo[id, !osubl]):2
= xo[id, !osubl]:2
= x:<id:2, !osubl:2> = x:<2, !:1>
= x:<2, x:<id:1, !osubl:1>> = x:<2, x:<1, !:0>>
= x:<2, x:<1, (eq0 → 1; xo[id, !osubl]):0>>
= x:<2, x:<1, 1:0>> since eq0:0 = T
= x:<2, x:<1, 1>>
= x:<2,1>
= 2.

在第 12 節中，我們將看到如何使用 FP 程式代數的定理來證明 ! 是階乘函式。

11.3.2 內積。我們前面已經看到這個定義如何工作。

Def IP = (/+)o(@x)otrans

11.3.3 矩陣乘法。這個矩陣乘法程式計算任意一對匹配矩陣 <m,n> 的乘積，其中每個矩陣 m 表示為其行的序列：

m = <m1, ..., mr>

其中 mi = <mi1, ..., mid> 對於 i = 1, ..., r。

Def MM = (@aIP)o(@distl)odistro[1, transo2]

程式 MM 有四個步驟，從右到左閱讀；每個步驟依次應用，從 [1, transo2] 開始，應用於其前身的結果。如果參數是 <m,n>，則第一步產生 <m,n'>，其中 n' = trans:n。第二步產生 <<m1,n'>, ..., <mr,n'>>，其中 mi 是 m 的行。第三步 @distl 產生

<distl:<m1,n'>, ..., distl:<mr,n'>> = <p1, ..., pr>

其中

pi = distl:<mi, n'> = <<mi1,nj'>, ..., <mid,nj'>>

對於 i = 1, ..., r，而 nj' 是 n 的第 j 列（n' 的第 j 行）。因此，pi，一個行和列對的序列，對應於第 i 個積行。運算符 @aIP，或 @(aIP)，導致 aIP 應用於每個 pi，進而導致 IP 應用於每個 pi 中的每個行和列對。最後一步的結果因此是構成積矩陣的行序列。如果任一矩陣不是矩形的，或者 m 的行長度與 n 的列長度不同，或者 m 或 n 的任何元素不是數字，結果為 ±。

程式 MM 不命名其參數或任何中間結果；不包含變數、迴圈、控制語句或程序聲明；沒有初始化指令；不是逐字元性質的；是從更簡單的組件層次構建的；使用普遍適用的內務處理形式和運算符（例如，@f、distl、distr、trans）；是完全通用的；當其參數以任何方式不適當時，產生 ±；不必要地限制了評估順序（所有 IP 對行和列對的應用都可以並行或以任何順序完成）；並且，使用代數法則（見下），可以轉換為更「高效」或更「解釋性」的程式（例如，遞迴定義的程式）。這些性質對於典型的 Von Neumann 矩陣乘法程式都不成立。

雖然它具有不熟悉且因此令人困惑的形式，程式 MM 描述了矩陣乘法的基本運算，而沒有過度決定過程或模糊其部分，就像大多數程式那樣；因此，通過形式轉換可以從中獲得許多直接的運算程式。對於 Von Neumann 電腦而言（就空間使用而言），這是一個內在低效的程式，但可以從中衍生出高效的程式，並且可以設想 FP 系統的實現，它們可以在不浪費空間的情況下執行 MM。效率問題超出本文範圍；我只想指出，由於語言非常簡單且不規定 lambda 型變數與資料的任何綁定，系統可能有更好的機會進行某種「延遲評估」[9, 10]，並比基於 lambda 演算的系統更有效地控制資料管理。

11.4 關於 FP Systems 的補充說明

11.4.1 將 FP Systems 作為程式語言。FP 系統是如此簡約，以至於一些讀者可能難以將它們視為程式語言。從這個角度看，函式 f 是一個程式，物件 x 是儲存裝置的內容，f:x 是程式 f 以 x 作為儲存裝置中內容啟動後的儲存裝置內容。定義集合是程式庫。系統提供的原始函式和函式形式是特定程式語言的基本語句。因此，根據原始函式和函式形式的選擇，FP 框架提供了一大類具有各種風格和能力的語言。與這些語言相關聯的程式代數取決於其特定的函式形式集合。本文提供的原始函式、函式形式和程式構成了一種努力，旨在開發這些可能風格中的一種。

11.4.2 FP Systems 的限制。FP 系統有許多限制。例如，一個給定的 FP 系統是一個固定語言；它不具備歷史敏感性：沒有程式可以更改程式庫。它只能在 x 是輸入且 f:x 是輸出的意義上處理輸入和輸出。如果原始函式和函式形式的集合較弱，它可能無法表達所有可計算函式。

FP 系統無法計算程式，因為函式表達式不是物件。FP 系統內也無法定義新的函式形式。（這兩個限制在形式化函式程式 (FFP) 系統中被移除，其中物件「表示」函式。）因此，沒有任何 FP 系統可以擁有一個函式 apply，使得

apply:<x,y> = x:y

因為在左側，x 是一個物件，而在右側，x 是一個函式。（注意，我們一直謹慎地區分了函式符號集合和物件集合：因此 1 是一個函式符號，而 1 是一個物件。）

FP 系統的主要限制是它們不具備歷史敏感性。因此，必須以某種方式擴展它們，才能變得實用有用。有關這些擴展的討論，請參閱有關 FFP 和 AST 系統的章節（第 13 節和第 14 節）。

11.4.3 FP Systems 的表達能力。假設兩個 FP 系統 FP1 和 FP2 都具有相同的物件集合和相同的原始函式集合，但 FP1 的函式形式集合嚴格包含 FP2 的集合。還假設兩個系統都可以表達物件上的所有可計算函式。儘管如此，我們可以說 FP1 比 FP2 更具表達能力，因為 FP2 中的每個函式表達式都可以在 FP1 中複製，但通過使用不屬於 FP2 的函式形式，FP1 可以比 FP2 更直接、更容易地表達一些函式。

我相信上述觀察可以發展成為一種語言表達能力的理論，其中語言 A 在以下粗略表述的條件下比語言 B 更具表達能力。首先，在 A 中，通過將所有現有函式應用於物件並以所有可能的方式相互應用，直到無法形成任何新型別的函式為止，形成所有可能型別的所有可能函式。（物件集合是一個型別；從型別 T 到型別 U 的連續函式集合 [T→U] 是一個型別。如果 f ∈ [T→U] 且 t ∈ T，則可以通過將 f 應用於 t 來形成 f:t ∈ U。）在語言 B 中執行相同的操作。接下來，將 A 中每個型別與 B 中對應的型別進行比較。如果，對於每個型別，A 的型別包含 B 對應的型別，那麼 A 比 B 更具表達能力（或表達能力相等）。如果 A 中某些函式型別與 B 的不可比較，那麼 A 和 B 在表達能力上不可比較。

11.4.4 FP Systems 的優點。FP 系統比傳統語言或基於 lambda 演算的語言簡單得多的主要原因是它們只使用最基本的固定命名系統（在定義中命名函式）和一個簡單固定的用函式替換其名稱的規則。因此，它們避免了傳統語言命名系統的複雜性以及 lambda 演算替換規則的複雜性。FP 系統允許為各種目的定義不同的命名系統（參見第 13.3.4 和 14.7 節）。這些系統不需要複雜，因為許多程式可以完全不需要它們。最重要的是，它們將名稱視為函式，可以與其他函式組合而無需特殊處理。

FP 系統提供了從傳統逐字元程式設計中擺脫的機會，其程度甚至超過 APL [12]（Von Neumann 框架內迄今最成功的嘗試），因為它們在一個統一的表達式世界中提供了更強大的函式形式集合。它們提供了發展更高層次的思考、操作和編寫程式技術的機會。

12. FP Systems 的程式代數

12.1 介紹

下面描述的程式代數是代數外行人的工作，我想表明這是一個外行人可以從中獲利並享受的遊戲，這個遊戲不需要對邏輯和數學有深入的理解。儘管它很簡單，但它可以幫助人們以一種系統化、相當機械的方式理解和證明程式。

到目前為止，證明程式正確需要掌握一些中等程度的數學和邏輯主題：完全偏序集合的性質、連續函式、函式的不動點、一階謂詞演算、謂詞轉換器、最弱前置條件，僅舉幾個不同證明方法中的主題。這些主題對於將設計證明技術作為其專業的專家來說非常有用；他們在此主題上發表了大量優美的著作，從 McCarthy 和 Floyd 的工作開始，以及最近 Burstall、Dijkstra、Manna 及其同事、Milner、Morris、Reynolds 和許多其他人的工作。這項工作的大部分基於 Dana Scott（指稱語義）和 C. A. R. Hoare（公理語義）奠定的基礎。但其理論水平使其超出這個專業領域之外的大多數外行人的範圍。

如果普通程式設計師要證明其程式正確，他將需要比專業人士迄今提出的技術簡單得多。下面的程式代數可能是這種證明規範的一個起點，結合當前代數操作的工作，它也可能幫助為自動化部分規範提供基礎。

這種代數優於其他證明技術的一個優點是，程式設計師可以使用其程式設計語言作為推導證明的語言，而不必在僅僅討論其程式的獨立邏輯系統中陳述證明。

程式代數的核心是法則和定理，它們陳述一個函式表達式與另一個相同。因此，法則 [f,g]oh = [foh, goh] 表明 f 和 g 的構造（與 h 組合）與 (f 與 h 組合) 和 (g 與 h 組合) 的構造是相同的函式，無論函式 f、g 和 h 是什麼。這種法則易於理解、易於證明其有效性、易於使用且功能強大。然而，我們也希望使用這種法則來求解方程，其中「未知」函式出現在方程的兩側。問題是，如果 f 滿足這樣的方程，則 f 的某個擴展 f' 也經常會滿足相同的方程。因此，為了賦予這種方程的解唯一含義，我們將需要程式代數的基礎（它使用 Scott 的連續函式不動點的概念），以確保通過代數操作獲得的解確實是最小且唯一的解。

我們的目標是為程式代數發展基礎，以解決理論問題，使程式設計師可以使用簡單的代數法則和基礎中的一兩個定理來解決問題並創建證明，以與我們解決高中代數問題相同的機械風格進行，並且能夠在不了解不動點或謂詞轉換器的情況下做到這一點。

一個特定的基礎問題出現了：給定形式的方程

f = p0 → q0; ... ; pi → qi; Ei(f),

(1) 其中 pi 和 qi 是不涉及 f 的函式，且 Ei(f) 是涉及 f 的函式表達式，代數的法則經常允許通過推導 formal 「擴展」此方程，添加一個新的「子句」

Ei(f) = pi+1 → qi+1; Ei+1(f)

(2) 然後，通過將 Ei(f) 在 (1) 中替換為 (2) 的右側，得到

f = p0 → q0; ... ; pi+1 → qi+1; Ei+1(f).

(3) 這種形式擴展可以無限進行。基礎必須回答的一個問題是：滿足 (1) 的最小 f 何時可以由無限展開式表示

f = p0 → q0; ... ; pn → qn; ...

(4) 其中涉及 f 的最後一個子句已被刪除，因此我們現在得到一個解，其右側不包含 f？這種解在兩個方面有用：首先，它們在 (4) 的意義上給出了「終止」證明，(4) 意味著 f:x 已定義，當且僅當存在一個 n 使得對於所有小於 n 的 i，pi:x = F 且 pn:x = T 且 qn:x 已定義。其次，(4) 給出了 f 的分情況描述，這通常可以闡明其行為。

後續章節中給出的代數基礎是朝向上述目標的溫和開端。對於有限類型的方程，其「線性展開定理」給出了何時可以從像 (1) 這樣無限可擴展的方程轉向像 (4) 這樣無限展開式的有用答案。對於更大類型的方程，更一般的「展開定理」給出了對類似問題不太有用的答案。希望可以找到涵蓋更多方程類型的更強大的定理。但就目前而言，只需了解這兩個簡單基礎定理的結論，就可以理解本節中的定理和範例。

基礎子節的結果總結在一個單獨的、較早的標題為「展開定理」的子節中，不參考不動點概念。基礎子節本身被放在後面，希望跳過該主題的讀者可以跳過。

12.2 程式代數的一些法則

在 FP 系統的程式代數中，變數的範圍是系統的函式集。「運算」是系統的函式形式。因此，例如，[f,g]oh 是上述 FP 系統代數的表達式，其中 f、g 和 h 是表示該系統任意函式的變數。並且

[f,g]oh = [foh, goh]

是代數的一個法則，它表示，無論為 f、g 和 h 選擇什麼函式，左邊的函式與右邊的函式是相同的。因此，這個代數法則僅僅是關於任何包含函式形式 [f,g] 和 fog 的 FP 系統的以下命題的重述：

命題： 對於所有函式 f, g 和 h 以及所有物件 x, ([f,g]oh):x = [foh, goh]:x.

證明：

([f,g]oh):x = [f,g]:(h:x)           by definition of composition
            = <f:(h:x), g:(h:x)>       by definition of construction
            = <(foh):x, (goh):x>       by definition of composition
            = [foh, goh]:x           by definition of construction

[]

有些法則的域比所有物件的域小。因此，1 o[f,g] = f 對於使得 g:x = ± 的物件 x 不成立。我們寫

definedog )> l o If, g] = f

表示右邊的法則（或定理）適用於物件 x，其中 definedog:x = T 的域。其中

Def defined = _±_ → ±; _T_

即 defined:x = x=± → ±; T。通常我們寫限定的函式等式：

p → f = g

表示對於任何物件 x，每當 p:x = T 時，f:x = g:x。

通常代數關注兩個運算，加法和乘法；它需要的法則很少。程式代數關注更多的運算（函式形式），因此需要更多的法則。

以下每個法則都需要一個對應的命題來驗證其有效性。感興趣的讀者會發現大多數這種命題的證明很容易（下面給出了兩個）。我們首先定義函式的常用排序和基於此排序的等價關係：

定義 f ≤ g 當且僅當對於所有物件 x，f:x = ±，或 f:x = g:x。

定義 f = g 當且僅當 f ≤ g 且 g ≤ f。

很容易驗證 ≤ 是一個偏序關係，f ≤ g 意味著 g 是 f 的擴展，並且 f = g 當且僅當對於所有物件 x，f:x = g:x。我們現在列出一些代數法則，按涉及的兩個主要函式形式組織。

I. 組合與構造

I.1   [f1, ..., fn]og = [f1og, ..., fnog]
I.2   @fo[g1, ..., gn] = [@fog1, ..., @fogn]
I.3   /f o [g1, ..., gn] = f o [g1, /f o [g2, ..., gn]] 當 n ≥ 2
                       = f o [g1, f o [g2, ..., f o [gn-1, gn]...]]
      /f o [g] = g
I.4   f o [_x_, g] = (bu f x)og
I.5   1 o [f1, ..., fn] ≤ f1
      s o [f1, ..., fs, ..., fn] ≤ fs 對於任何選擇器 s, s ≤ n
      defined o fs (對於所有 i≠s, 1≤i≤n) → s o [f1, ..., fn] = fs
I.5.1 [f1og1, ..., fnogn] = [f1, ..., fn]o[g1, ..., gn] (應為：[f1og1, ..., fnogn] = [f1,...,fn] o [g1,...,gn] 僅在 fn o gn 是最後一個元素時成立？檢查原文。原文沒有 o)
      [f1og1, ..., fnogn] 是 [f1og1, ..., fnogn]:x = <f1(g1x), ..., fn(gnx)>. 這無法由 [f1,...,fn]o[g1,...,gn] 獲得。原文是 [fl°gl ..... fn°gn] --= [fl ..... fn] o [gx ..... gn] 我覺得這寫錯了，應該是 [f1og1, ..., fnogn] = [f1,...,fn] o [g1,...,...,gn] 或是其他形式。讓我參考原文的 1.5.1。原文寫作 [flol ..... fnon]o[gx ..... gn] --= [fl°gl ..... fn°gn]。這更奇怪了，因為 [flol ..... fnon] 不像函式形式。看起來這是個印刷錯誤，它應該是關於 [ ] 和 o 的結合律。例如 [f1, f2] o [g1, g2] = <f1(g1x), f2(g2x)>。這個法則似乎是說 [f1og1, ..., fnogn] = [f1,...,fn] o [g1, ..., gn] 是錯的。如果原文 1.5.1 寫的是 [f1,...,fn] o [g1,...,gn] 那麼結果是 <f1(<g1x,...,gnx>), ..., fn(<g1x,...,gnx>)>。這不是 [f1og1,...,fnogn]。讓我再檢查一次原文圖片。原文寫的是 [fl°l ..... fn°n]o[gx ..... gn] --= [fl°gl ..... fn°gn]. 這更有道理，因為 lo[g1,...,gn] = g1, 2o[g1,...,gn]=g2 等等。
      [f1o1, ..., fnon] o [g1, ..., gn] = [f1o1 o [g1, ..., gn], ..., fnon o [g1, ..., gn]] = [f1:g1, ..., fn:gn]? 不對，是 [f1:(1:[g1,...,gn]), ..., fn:(n:[g1,...,gn])] = [f1:g1, ..., fn:gn]. 是的，這個法則的意思是，應用一個構造函式，其每個元素是函式 fi 與選擇器 i 的組合，然後再應用另一個構造函式 [g1,...,gn]，等價於構造函式 [f1og1, ..., fnon] 的應用。法則 I.5.1 應該是 `[f1o1, ..., fnon]o[g1, ..., gn] = [f1og1, ..., fnon]`
      [f1o1, ..., fnon]o[g1, ..., gn] = [f1o1o[g1, ..., gn], ..., fnono[g1, ..., gn]]
      = [f1:(1:[g1, ..., gn]), ..., fn:(n:[g1, ..., gn])]
      = [f1:g1, ..., fn:gn]
      這似乎不等於 [f1og1, ..., fnogn]，因為 [f1og1, ..., fnogn]:x = <f1(g1:x), ..., fn(gn:x)>.
      法則 I.5.1 在原文中寫為 `[flol ..... fnon]o[gx ..... gn] --= [fl°gl ..... fn°gn]`. 似乎應為 `[f1o1, ..., fnon]o[g1, ..., gn] = [f1og1, ..., fnogn]`. 我會按照最可能的正確版本進行翻譯。假設是這個版本。
      [f1o1, ..., fnon] o [g1, ..., gn] = [f1 o (1 o [g1, ..., gn]), ..., fn o (n o [g1, ..., gn])]
      = [f1og1, ..., fnon]
      是的，這看起來是正確的。
      I.5.1 [f1o1, ..., fnon]o[g1, ..., gn] = [f1og1, ..., fnon]
I.6   tlo[f, φ] ≤ φ and tlo[f1, ..., fn] ≤ [f2, ..., fn] for n≥2
      definedof1 → tlo[f1] = φ and tlo[f1, ..., fn] = [f2, ..., fn] for n≥2
I.7   distlo[f, [g1, ..., gn]] = [[f, g1], ..., [f, gn]]
      definedof → distlol[f, φ] = φ
      The analogous law holds for distr. (類似的法則對 distr 成立)
I.8   apndlo[f, [g1, ..., gn]] = [f, g1, ..., gn]
      nullog → apndlo[f,g] = [f]
      And so on for apndr, reverse, rotl, etc. (apndr, reverse, rotl 等等依此類推)
I.9   [..., _±_, ...] = ±
I.10  apndlo[fog, @foh] = @foapndlo[g,h]
I.11  pair & notonull o 1 → apndlo[[1 o 1, 2], distro[tlo 1, 2]] = distr

Where f&g is the function: ando[f,g]; pair = atom → F; eqo[length,2]

II. 組合與條件 (右關聯的圓括號省略) (法則 II.2 在 Manna et al. [16], p. 493 中提及。)

II.1  (p→f, g)oh = poh → foh; goh
II.2  ho(p→f, g) = p → hof; hog
II.3  oro[q,notoq] → ando[p,q] → f; ando[p,notoq] → g; h = p → (q→f, g); h
II.3.1 p → (p→f; g); h = p → f; h

III. 組合與雜項

III.1 ±of ≤ ±
       defined of → kof = k (_k_ is a constant function)
III.1.1 _±_of = fo_±_ = ±
III.2 idof = f
III.3 pair → lodistr = [1o1, 2]
       also: pair → lotl = 2
       etc.
III.4 @(fog) = @fo@g
III.5 nullog → @fog = φ (_φ_ is the empty sequence)

證明兩個法則 我們給出驗證法則 I.10 和 I.11 的命題的證明，它們比大多數其他法則稍微複雜一些。

命題 1

apndl o [fog, @foh] = @foapndl o [g,h]

證明。我們證明對於每個物件 x，上述兩個函式產生相同的結果。 情況 1。h:x 既不是序列也不是 ±。 則當應用於 x 時，兩側都產生 ±。

情況 2。h:x = φ。則

apndl o [fog, @foh]: x
= apndl: <fog:x, @f:φ> = apndl: <f:(g:x), φ> = <f:(g:x)>
@f o apndl o [g,h]: x
= @f o apndl: <g:x, φ> = @f:<g:x> = <f:(g:x)>

情況 3。h:x = <y1, ..., yn>。則

apndl o [fog, @foh]: x
= apndl: <fog:x, @f:<y1, ..., yn>> = apndl: <f:(g:x), <f:y1, ..., f:yn>> = <f:(g:x), f:y1, ..., f:yn>
@f o apndl o [g,h]: x
= @f o apndl: <g:x, <y1, ..., yn>> = @f:<g:x, y1, ..., yn> = <f:(g:x), f:y1, ..., f:yn>

[]

命題 2

pair & notonull o 1 → apndl o [[1 o 1, 2], distr o [tlo 1, 2]] = distr

其中 f&g 是函式: ando[f, g]，且 φ = φof。

證明。我們證明當應用於任何對 <x,y> 時，兩側產生相同的結果，其中 x ≠ φ，如所述限定。 情況 1。x 是原子或 ±。則 distr: <x,y> = ±，因為 x ≠ φ。左側應用於 <x,y> 時也產生 ±，因為 tlo 1:<x,y> = ± 且所有函式都是 ± 保留的。

情況 2。x = <x1, ..., xn>。則

apndl o [[1 o 1, 2], distr o [tlo 1, 2]]:<x, y>
= apndl: <<1:x, y>, distr: <tl:x, y>>
= apndl: <<x1,y>, φ> if tl:x = φ
= <<x1,y>>
= apndl: <<x1,y>, <<x2,y>, ..., <xn,y>>> if tl:x ≠ φ
= <<x1,y>, ..., <xn,y>>
= distr: <x,y>

[]

以上結束了目前的代數法則列表；它遠非詳盡無遺，還有許多其他的。

12.3 範例：兩個矩陣乘法程式的等價性

我們之前看過矩陣乘法程式：

Def MM = (@aIP)o(@distl)odistro[1, transo2].

我們現在將展示其初始段 MM'，其中

Def MM' = (@aIP)o(@distl)odistr,

可以遞迴地定義。（MM' 在第二個矩陣被轉置後，「乘以」一對矩陣。注意，MM' 與 MM 不同，對於所有不是對的參數都給出 ±。）也就是說，我們將證明 MM' 滿足以下等式，該等式遞迴地定義了相同的函式（在對上）：

f = null o 1 → φ; apndl o [aIP o distl o [1 o 1, 2], f o [tlo 1, 2]].

我們的證明將採取的形式是證明以下函式 R，

Def R = null o 1 → φ; apndl o [aIP o distl o [1 o 1, 2], MM' o [tlo 1, 2]]

對於所有對 <x,y>，與 MM' 是相同的函式。R 在第一個矩陣有零行以上時，「乘以」兩個矩陣，方法是計算「積」的第一行（使用 aIP o distl o [1 o 1, 2]），並將其連接到第一個矩陣尾部和第二個矩陣的「積」。因此，我們想要的定理是

pair → MM' = R,

由此立即可得以下結論：

MM = MM' o [1, transo2] = R o [1, transo2];

其中

Def pair = atom → F; eqo[length, 2].

定理： pair → MM' = R

其中

Def MM' = (@aIP)o(@distl)odistr
Def R = null o 1 → φ; apndl o [aIP o distl o [1 o 1, 2], MM' o [tlo 1, 2]]

證明。 情況 1。pair & null o 1 → MM' = R.

pair & null o 1 → R = φ                 by def of R
pair & null o 1 → MM' = φ

since distr: <φ,x> = φ by def of distr, and @aIP o φ = φ by def of Apply to all. Therefore: @aIP o @distl o distr: <φ,x> = φ. Thus pair & null o 1 → MM' = R.

情況 2。pair & not o null o 1 → MM' = R.

pair & not o null o 1 → R = R',

(1) by def of R and R', where

Def R' = apndl o [aIP o distl o [1 o 1, 2], MM' o [tlo 1, 2]].

We note that

R' = apndl o [fog, @foh]

where

f = aIP o distl
g = [1 o 1, 2]
h = distr o [tlo 1, 2]
@f = @(aIP o distl) = @aIP o @distl

(by III.4). (2) Thus, by I.10,

R' = @f o apndl o [g,h].

(3) Now apndl o [g,h] = apndl o [[1 o 1, 2], distr o [tlo 1, 2]], thus, by I.11,

pair & not o null o 1 → apndl o [g,h] = distr.

(4) And so we have, by (1), (2), (3) and (4),

pair & not o null o 1 → R = R' = @f o distr = @aIP o @distl o distr = MM'.

情況 1 和情況 2 一起證明了定理。 []

12.4 展開定理

在以下小節中，我們將「求解」一些簡單的方程（我們所說的「解」是指滿足方程的「最小」函式）。為此，我們需要以下概念和結果，這些概念和結果來自後面關於代數基礎的小節，其中包含了它們的證明。

12.4.1 展開。假設我們有一個形式為

f = E(f)

(E1) 的方程，其中 E(f) 是涉及 f 的表達式。再假設存在一個無限序列的函式 fi，i = 0, 1, 2, ...，每個函式具有以下形式：

f0 = ±
fi+1 = p0 → q0; ... ; pi → qi; ±

(E2) 其中 pi 和 qi 是特定的函式，使得 E 具有以下性質：

E(fi) = fi+1 對於 i = 0, 1, 2, ...

(E3) 則我們說 E 是可展開的，並且 fi 是其逼近函式。

如果 E 是可展開的，且如 (E2) 所示具有逼近函式，並且如果 f 是 (E1) 的解，則 f 可以寫為無限展開式

f = p0 → q0; ... ; pn → qn; ...

(E4) 意思是說，對於任何 x，f:x ≠ ± 當且僅當存在一個 n ≥ 0 使得 (a) 對於所有 i < n，pi:x = F，且 (b) pn:x = T，且 (c) qn:x ≠ ±。當 f:x ≠ ± 時，則對於這個 n，f:x = qn:x。（上述是「展開定理」的推論。）

12.4.2 線性展開。一種更有助於求解某些方程的工具適用於，對於任何函式 h，

E(h) = p0 → q0; E1(h)

(LE1) 並且存在 pi 和 qi 使得

E1(pi → qi; h) = pi+1 → qi+1; E1(h) 對於所有 h ∈ F 和 i = 0, 1, 2, ...

(LE2) 且

E1(±) = ±.

(LE3) 在上述條件下，稱 E 對於這些 pi 和 qi 是線性可展開的。如果是這樣，且 f 是

f = E(f)

(LE4) 的解，則 E 是可展開的，且 f 再次可以寫為無限展開式

f = p0 → q0; ... ; pn → qn; ...

(LE5) 使用 (LE1) 和 (LE2) 生成的 pi 和 qi。

儘管對於給定的函式，(E4) 或 (LE5) 中的 pi 和 qi 並非唯一，但有可能找到額外的約束使其唯一，在這種情況下，展開式 (LE5) 將構成函式的規範形式。即使沒有唯一性，這些展開式也經常允許證明兩個不同函式表達式的等價性，並且它們通常闡明函式的行為。

12.5 遞迴定理

使用上述三個法則和線性展開，可以證明以下一個中等通用性的定理，它為許多遞迴定義的函式提供了明確的展開式。

遞迴定理： 令 f 是

f = p → g; Q(f)

(1) 的解，其中

Q(k) = ho[i, koj] 對於任何函式 k

(2) 且 p, g, h, i, j 是任何給定的函式，則

f = p → g; poj → Q(g); ... ; pojn → Qn(g); ...

(3) (其中 Qn(g) = ho[i, Qn-1(g)oj]，且 jn 是 joj...j (n times) 對於 n ≥ 2) 且

Qn(g) = /h o [i, ioj, ..., iojn-1, gojn].

(4)

證明。我們驗證 p → g; Q(f) 是線性可展開的。令 pn, qn 和 k 是任何函式。則

Q(pn → qn; k)
= ho[i, (pn → qn; k)oj]                by (2)
= ho[i, (pnoj → qnoj; koj)]             by II.1
= ho(pnoj → [i, qnoj]; [i, koj])         by IV.1
= pnoj → ho[i, qnoj]; ho[i, koj]       by II.2
= pnoj → Q(qn); Q(k)                 by (2)

(5) 因此如果 p0 = p 且 q0 = g，則 (5) 給出 p1 = poj 且 q1 = Q(g)，並且通常給出滿足 (LE2) 的以下函式

pn = poj^n

and

qn = Qn(g).

(6) 最後，

Q(±) = ho[i, ±oj]
= ho[i, ±]                                 by III.1.1
= ho±                                      by I.9
= ±                                       by III.1.1.

(7) 因此 (5) 和 (6) 驗證了 (LE2)，(7) 驗證了 (LE3)，其中 E1 = Q。如果我們令 E(f) = p → g; Q(f)，則我們有 (LE1)；因此 E 是線性可展開的。由於 f 是 f = E(f) 的解，結論 (3) 由 (6) 和 (LE5) 得出。

現在

Qn(g) = ho[i, Qn-1(g)oj]
= ho[i, ho[ioj, ..., ho[iojn-1, gojn] ... ]]
= /ho[i, ioj, ..., iojn-1, gojn]         by I.3

(8) 結果 (8) 是第二個結論 (4)。 []

12.5.1 範例：遞迴階乘函式的正確性證明。令 f 是

f = eq0 → 1; xo[id, !osubl]

的解，其中 Def s = -o[id, _1_] (減 1)。則 f 滿足遞迴定理的假設，其中 p = eq0, g = _1_, h = x, i = id, 且 j = s。因此

f = eq0 → _1_; ... ; eq0os^n → Qn(_1_); ...

且

Qn(_1_) = /× o [id, idos, ..., idos^n-1, _1_os^n].

現在 idos^k = s^k by III.2，且 eq0os^n = _±_os^n = ± by III.1.1 and III.l, since eq0os^n:x implies definedos^n:x; and also eq0os^n:x = eq0:(x - n) = x=n. Thus if eq0os^n:x = T, then x = n and

Qn(_1_): n = n × (n - 1) × ... × (n - (n - 1)) × (_1_:(n - n)) = n!.

在 f 的先前展開式中使用這些關於 _1_os^n, eq0os^n 和 Qn(1) 的結果，我們獲得

f:x = x=0 → 1; ... ; x=n → n × (n - 1) × ... × 1 × 1; ...

因此我們證明了 f 恰好在非負整數集上終止，並且是該集合上的階乘函式。

12.6 迭代定理

這實際上是遞迴定理的推論。它為許多迭代程式提供了簡單的展開式。

迭代定理： 令 f 是

f = p → g; hofok

的解（即最小解），則

f = p → g; pok → hogok; ... ; pok^n → hnogok^n; ...

證明。令 h' = ho2, i' = id, j = k, 則

f = p → g; h'o[i', foj]

since ho2o[id, fok] = hofok by I.5 (id is defined except for ±, and the equation holds for ±). Thus the recursion theorem gives

f = p → g; ... ; pok^n → Qn(g); ...

where

Qn(g) = ho2o[id, Qn-1(g)ok] = hoQn-1(g)ok = hnogok^n

by I.5 []

12.6.1 範例：迭代階乘函式的正確性證明。令 f 是

f = eq0o1 → 2; fo[so 1, x]

的解，其中 Def s = -o[id, _1_] (減 1)。我們想證明 f:<x,1> = x! 若且唯若 x 是非負整數。令 p = eq0o1, g = 2, h = id, k = [so 1, x]。則

f = p → g; hofok

因此

f = p → g; ... ; pok^n → gok^n; ...

(1) 由迭代定理，因為 h^n = id。我們想證明

pair → k^n = [an, bn]

(2) 對於所有 n ≥ 1 成立，其中

an = so^n o 1

(3)

bn = /x o [so^n-1 o 1, ..., so 1, 1, 2]

(4) 現在 (2) 對 n = 1 成立，由 k 的定義。我們假設它對某個 n ≥ 1 成立，並證明它對 n + 1 成立。現在

pair → k^n+1 = kok^n = [so 1, x]o[an, bn]

since (2) holds for n. And so (5)

pair → k^n+1 = [soan, xo[an, bn]] by I.1 and I.5

(6) 為了從 (5) 轉到 (6)，我們必須檢查每當 (5) 中 an 或 bn 產生 ± 時，(6) 的右側也產生 ±。現在

soan = so(so^n o 1) = so^n+1 o 1 = an+1

(7)

xo[an, bn] = xo[so^n o 1, /x o [so^n-1 o 1, ..., so 1, 1, 2]]
= /x o [so^n o 1, so^n-1 o 1, ..., so 1, 1, 2] = bn+1 by I.3.

(8) 結合 (6), (7), (8) 得出

pair → k^n+1 = [an+1, bn+1].

(9) 因此 (2) 對 n = 1 成立，並且每當對 n 成立時，對 n + 1 也成立，因此通過歸納法，對所有 n ≥ 1 成立。現在 (2) 對於對給出了：

definedok^n → pok^n = eq0o1o[an, bn] = eq0oan = eq0os^n o 1

(10)

definedogok^n → gok^n = 2o[an, bn] = /x o [so^n-1 o 1, ..., so 1, 1, 2]

(11) (兩者都使用 I.5)。現在 (1) 告訴我們 f:<x,1> 已定義，當且僅當存在一個 n 使得對於所有 i < n，pok^i:<x,1> = F，且 pok^n:<x,1> = T，也就是說，由 (10)，eq0os^n:x = T，即 x=n；且 gok^n:<x,1> 已定義，在這種情況下，由 (11)，

f:<x,1> = /x:<n, n-1, ..., 1, 1> = n!,

這正是我們著手證明的內容。

12.6.2 範例：兩個迭代程式等價性的證明。在這個範例中，我們想證明兩個迭代定義的程式 f 和 g 是相同的函式。令 f 是

f = po 1 → 2; hofo[ko 1, 2].

的解。令 g 是

g = po 1 → 2; go[ko 1, ho2].

的解。則由迭代定理：

f = p0 → q0; ... ; pn → qn; ...
g = p0' → q0'; ... ; pn' → qn'; ...

其中（令對於任何 r，r^0 = id），對於 n = 0, 1, ...

pn = polo[ko 1, 2]^n = polo[ko^n o 1, 2^n]                               by I.5.1
qn = hno2o[ko 1, 2]^n = hno2o[ko^n o 1, 2^n]                               by I.5.1
pn' = polo[ko 1, ho2]^n = polo[ko^n o 1, hno2]                               by I.5.1
qn' = 2o[ko 1, ho2]^n = 2o[ko^n o 1, hno2]                                 by I.5.1.

現在，由上可知，使用 I.5，

definedo2 → pn = pok^n o 1                                                (12)
definedohno2 → pn' = pok^n o 1                                               (13)
definedok^n o 1 → qn = hno2                                                  (14)
definedok^n o 1 → qn' = hno2                                                 (15)

因此

definedohno2 → definedo2 = T
definedohno2 → pn = pn'
definedok^n o 1 → qn = qn'

since pn and pn' provide the qualification needed for qn and qn' to be defined as h^n o 2. 現在假設存在一個 x 使得 f:x ≠ g:x。則存在一個 n 使得對於所有 i < n，pi:x = pn':x = F，且 pn:x = pn':x = T。由 (12) 和 (13) 可知，這只可能發生在 h^n o 2:x = ± 時。但由於 h 是 ± 保留的，對於所有 m ≥ n，h^m o 2:x = ±。因此，由 (14) 和 (15) 可知，qn:x = qn':x = ±。這與假設存在一個 x 使得 f:x ≠ g:x 相矛盾。因此 f = g。

這個範例（由 J. H. Morris, Jr. 提供）在 [16] 的 p. 498 上處理得更為優雅。然而，有些人可能會覺得上述處理更具建設性，更能機械地引導到關鍵問題，並為兩個函式的行為提供了更多洞察。

12.7 非線性方程式

前面的範例涉及「線性」方程（其中「未知」函式不具有涉及自身的參數）。求解「二次」及更高次方程的簡單展開式的存在性問題仍未解決。

前面的範例涉及 f = E(f) 的解，其中 E 是線性可展開的。以下範例涉及一個二次且可展開（但非線性可展開）的 E(f)。

12.7.1 範例：冪等性證明 ([16] p. 497)。令 f 是

f = E(f) = p → id; f^2oh.

(1) 的解。我們想證明 f = f^2。我們驗證 E 對於以下逼近函式是可展開的（第 12.4.1 節）：

f0 = ±
fn = p → id; ... ; poh^n-1 → h^n-1; ± 對於 n > 0

(2a) (2b) 首先，我們注意到 p → fn = id，因此

poh^i → fnoh^i = h^i.

(3) 現在 E(f0) = p → id; ±^2oh = f1， (4) 且

E(fn) = p → id; fn o (p → id; ... ; poh^n-1 → h^n-1; ±) o h
= p → id; fn o (poh → h; ... ; poh^n → h^n; ±oh) by II.1
= p → id; poh → fnoh; ... ; poh^n → fnoh^n; fn o ±    by II.2
= p → id; poh → h; ... ; poh^n → h^n; ±             by (3)
= fn+1.

(5) 因此 E 由 (4) 和 (5) 可展開；所以由 (2) 和第 12.4.1 節 (E4)

f = p → id; ... ; poh^n → h^n; ...

(6) 但是 (6) 由迭代定理給出

f = p → id; foh.

(7) 現在，如果 p:x = T，則 f:x = x = f^2:x，由 (1)。如果 p:x = F，則

f:x = f^2oh:x                     by (1)
= f:(foh:x) = f:(f:x)              by (7)
= f^2:x.

如果 p:x 既不是 T 也不是 F，則 f:x = ± = f^2:x。因此

f = f^2.

12.8 程式代數的基礎

本節的目的是確立第 12.4 節所述結果的有效性。後續章節不依賴於本節，因此希望跳過的讀者可以跳過。我們使用 [16] 中的標準概念和結果，但用於物件和函式的符號等將是本文的符號。

我們將給定 FP 系統的物件集 O（包括 ±）作為所有函式的域（和值域）。我們將 F 視為函式集，將 F 視為該 FP 系統的函式形式集。我們用 E(f) 表示任何涉及函式形式、原始和定義函式以及函式符號 f 的函式表達式，我們將 E 視為將函式 f 映射到相應函式 E(f) 的函式。我們假設所有 f ∈ F 都是 ± 保留的，並且 F 中的所有函式形式都對每個變數對應連續的函式（例如，[f, g] 對 f 和 g 都是連續的）。（FP 系統中給出的所有原始函式都是 ± 保留的，所有函式形式都是連續的。）

定義。令 E(f) 為函式表達式。令

f0 = ±
fi+1 = p0 → q0; ... ; pi → qi; ±

對於 i = 0, 1, ...，其中 pi, qi ∈ F。令 E 具有以下性質：

E(fi) = fi+1 對於 i = 0, 1, ...。

則稱 E 為可展開的，逼近函式為 fi。我們寫

f = p0 → q0; ... ; pn → qn; ...

表示 f = limi(fi)，其中 fi 具有上述形式。我們將右側稱為 f 的無限展開式。我們認為 f:x 已定義，當且僅當存在一個 n ≥ 0 使得 (a) 對於所有 i < n，pi:x = F，且 (b) pn:x = T，且 (c) qn:x 已定義，在這種情況下，f:x = qn:x。

展開定理： 令 E(f) 可展開，逼近函式如上所示。令 f 是滿足

f = E(f).

的最小函式。則

f = p0 → q0; ... ; pn → qn; ...

證明。由於 E 是連續函式（來自 F）的組合，只涉及單調函式（來自 F 的 ± 保留函式）作為常數項，E 是連續的（[16] p. 493）。因此，其最小不動點 f 是 limi(Ei(±)) = limi(fi)（[16] p. 494），根據定義，這就是 f 的上述無限展開式。 []

定義。令 E(f) 為滿足以下條件的函式表達式：

E(h) = p0 → q0; E1(h) 對於所有 h ∈ F

(LE1) 其中存在 pi ∈ F 和 qi ∈ F 使得

E1(pi → qi; h) = pi+1 → qi+1; E1(h) 對於所有 h ∈ F 和 i = 0, 1, ...

(LE2) 且

E1(±) = ±.

(LE3) 則稱 E 對於這些 pi 和 qi 是線性可展開的。

線性展開定理： 令 E 對於 pi 和 qi (i = 0, 1, ...) 是線性可展開的。則 E 是可展開的，逼近函式為

fi = ±
fi+1 = p0 → q0; ... ; pi → qi; ±

(1) (2)

證明。我們想證明 E(fi) = fi+1 對於任何 i ≥ 0。 現在

E(f0) = p0 → q0; E1(±) = p0 → q0; ± = f1

(3) by (LE1) (LE3) (1). 令 i > 0 為固定值，且令

f = p0 → q0; w1                                (4a)
w1 = p1 → q1; w2                                (4b)

等等。

wi-1 = pi-1 → qi-1; ±                             (4i)

則對於此 i > 0

E(fi) = p0 → q0; E1(fi)                              by (LE1)
E1(fi) = p1 → q1; E1(w1)                             by (LE2) and (4a)
E1(w1) = p2 → q2; E1(w2)                             by (LE2) and (4b)

等等。

E1(wi-1) = pi → qi; E1(±)                             by (LE2) and (4i)
= pi → qi; ±                                 by (LE3)

結合上述結果，根據 (2)，對於任意 i > 0，E(fi) = fi+1。 (5) 根據 (3)，(5) 對 i = 0 也成立；因此對所有 i ≥ 0 成立。所以 E 是可展開的，並且具有所需的逼近函式。 []

推論。如果 E 對於 pi 和 qi (i = 0, 1, ...) 是線性可展開的，且 f 是滿足

f = E(f)

(LE4) 的最小函式，則

f = p0 → q0; ... ; pn → qn; ...

(LE5)

12.9 Lambda 演算與組合子的程式代數

由於 Church 的 lambda 演算 [5] 和 Sch6nfinkel 和 Curry 開發的組合子系統 [6] 是表示函式應用概念的主要數學系統，並且由於它們比 FP 系統更強大，因此很自然地詢問基於這些系統的程式代數會是什麼樣子。

Church 和 Curry 系統中等價於 FP 組合 fog 的表達式是

λfgx.(f(gx)) - B

其中 B 是 Curry 定義的一個簡單組合子。Church 或 Curry 系統本身沒有直接等價於 FP 物件 <x,φ> 的構造；然而，跟隨 Landin [14] 和 Burge [4]，可以使用原始函式 prefix、head、tail、null 和 atomic 來引入與 FP 序列對應的列表結構的概念。然後，使用 FP 符號表示列表，lambda 演算中等價於構造的表達式是 λfgx.<fx,gx>。組合子中的等價表達式是一個涉及 prefix、空列表和兩個或更多基本組合子的複雜表達式。它非常複雜，我將不嘗試給出它。

如果在 Church 或 Curry 系統中使用 lambda 演算或組合子表達式來表示函式形式 fog 和 [f,g]，以表達 FP 代數中的法則 I.1，[f,g]oh = [foh, goh]，結果是一個如此複雜的表達式，以至於法則的意義被模糊了。在任何一個系統中澄清其意義的唯一方法是命名這兩個函式：組合 = B，構造 = A，以便 Bfg = fog，且 Afg = [f,g]。那麼 I.1 就變成了

B(Afg)h = A(Bfh)(Bgh),

這仍然不如 FP 法則清晰。

上述觀點是，如果想在 Church 或 Curry 系統中陳述像 FP 代數法則那樣清晰的法則，則需要選擇某些函式（例如，組合和構造）作為代數的基本運算，並賦予它們簡短的名稱，或者最好使用 FP 中那樣的一些特殊符號來表示它們。如果這樣做並提供原始元素、物件、列表等，結果將是一個類似 FP 的系統，其中通常的 lambda 表達式或組合子不出現。即便如此，這些 Church 或 Curry 版本的 FP 系統，由於限制較少，仍有一些 FP 系統所沒有的問題： a) Church 和 Curry 版本可以容納多種型別的函式，並且可以定義在 FP 系統中不存在的函式。例如，Bf 是一種在 FP 系統中沒有對應項的函式。這種額外的能力帶來了型別兼容性的問題。例如，在 fog 中，g 的值域是否包含在 f 的定義域中？在 FP 系統中，所有函式都具有相同的定義域和值域。 b) Church 的 lambda 演算語義依賴於替換規則，這些規則雖然表述簡單，但其含義非常難以完全理解。這些規則的真實複雜性並未得到廣泛認識，但從連續出現的能幹邏輯學家發表「證明」了 Church-Rosser 定理但未能考慮到其中一個或另一個複雜性，就可以看出這一點。（Church-Rosser 定理，或 Scott 對模型存在性的證明 [22]，需要證明 lambda 演算具有一致的語義。）純 Lisp 的定義在相當長的一段時間內包含了一個相關錯誤（「funarg」問題）。類似問題也存在於 Curry 的系統中。 相比之下，FP 系統的形式化版本 (FFP)（在下一節中描述）沒有變數，只有一個基本的替換規則（用函式替換其名稱），並且可以通過沿著 Dana Scott 和 Manna 等人 [16] 發展起來的相對簡單的不動點論證來證明其具有一致的語義。有關此類證明，請參閱 McJones [18]。

12.10 補充說明

上述程式代數需要大量工作，以提供更大類別方程的展開式，並將其法則和定理擴展到這裡給出的基本法則和定理之外。探索一個 FP 類系統的代數將很有趣，該系統的序列構造子不是 ± 保留的（法則 I.5 得到加強，但 IV.1 丟失了）。其他有趣的問題包括：(a) 找到使展開式唯一的規則，為函式提供規範形式；(b) 找到針對各種參數類別的函式展開和分析行為的演算法；以及 (c) 探索使用代數的法則和定理作為形式化、預執行「延遲評估」方案 [9, 10] 或執行時運行的方案的基本規則的方法。這種方案將利用法則 1 o[f,g] ≤ f 等，避免評估 g:x。

13. 形式化函式程式系統 (FFP Systems)

13.1 介紹

正如我們所見，FP 系統的函式集取決於其原始函式集、函式形式集和定義集。特別是，其函式形式集是固定不變的，這個集合在很大程度上決定了系統的能力。例如，如果其函式形式集為空，那麼其整個函式集就只是原始函式集。在 FFP 系統中，可以創建新的函式形式。函式形式由物件序列表示；序列的第一個元素決定它代表哪種形式，而其餘元素則是形式的參數。

在 FFP 系統中定義新函式形式的能力是它們與 FP 系統之間主要區別的一個結果：在 FFP 系統中，物件被系統性地用於「表示」函式。否則，FFP 系統緊密地反映了 FP 系統。它們與早期論文 [2] 中的化簡 (Red) 語言相似，但更簡單。

我們首先給出 FFP 系統的簡單語法，然後非正式地討論其語義並給出範例，最後給出其形式語義。

13.2 語法

我們描述 FFP 系統的物件集 O 和表達式集 E。這些取決於原子集 A 的選擇，我們將 A 視為給定。我們假設 T (真)、F (假)、φ (空序列) 和 # (默認) 屬於 A，以及各種「數字」等。

  1. 底 ± 是一個物件但不是原子。
  2. 每個原子都是一個物件。
  3. 每個物件都是一個表達式。
  4. 如果 x1, ..., xn 是物件 [表達式]，則 <x1, ..., xn> 是一個物件 [表達式] 稱為序列（長度為 n）對於 n ≥ 1。物件 [表達式] xi 對於 1 ≤ i ≤ n 是序列 <x1, ..., xi, ..., xn> 的第 i 個元素。（φ 既是序列又是原子；其長度為 0。）
  5. 如果 x 和 y 是表達式，則 (x:y) 是一個表達式稱為應用，x 是其運算符，y 是其操作數。兩者都是表達式的元素。
  6. 如果 x = <x1, ..., xn> 且 x 的元素中有 ±，則 x = ±。也就是說，<..., ±, ...> = ±。
  7. 所有物件和表達式都是通過有限次使用上述規則形成的。

表達式 x 的子表達式要么是 x 本身，要么是 x 的元素的子表達式。FFP 物件是沒有應用作為子表達式的表達式。給定相同的原子集，FFP 和 FP 物件是相同的。

13.3 關於 FFP 語義的非正式說明

13.3.1 表達式的意義；語義函式 μ。每個 FFP 表達式 e 都有一個意義，μe，它總是一個物件；μe 是通過重複將 e 中每個最內層應用替換為其意義來找到的。如果此過程非終止，則 e 的意義為 ±。最內層應用 (x:y) 的意義（由於它在最內層，x 和 y 必須是物件）是將由 x 表示的函式應用於 y 的結果，就像在 FP 系統中一樣，只是在 FFP 系統中，函式由物件表示，而不是由函式表達式表示，原子（而不是函式符號）表示原始函式和定義函式，而序列表示由函式形式表示的 FP 函式。

物件和它們表示的函式之間的關聯由 FFP 系統的表示函式 ρ 給出。（ρ 和 μ 都屬於系統的描述，而不是系統本身。）因此，如果原子 NULL 表示 FP 函式 null，那麼 ρNULL = null，並且 (NULL:A) 的意義是

μ(NULL:A) = (ρNULL):A = null:A = F.

從現在起，如上所示，我們以兩種含義使用冒號。當它位於兩個物件之間時，如 (NULL:A) 中，它標識一個僅表示其自身的 FFP 應用；當它位於函式和物件之間時，如 (ρNULL):A 或 null:A 中，它標識一個類似 FP 的應用，表示將函式應用於物件的結果。

FFP 運算符是物件這一事實使得函式 apply 成為可能，這在 FP 系統中是無意義的：

apply:<x,y> = (x:y).

apply:<x,y> 的結果，即 (x:y)，在 FP 系統中是無意義的，原因有二。首先，(x:y) 本身不是物件；這說明了 FP 和 FFP 系統之間的另一個區別：一些 FFP 函式，如 apply，將物件映射到表達式，而不是像 FP 函式那樣直接映射到物件。然而，apply:<x,y> 的意義是一個物件（見下文）。其次，(x:y) 甚至不可能成為 FP 系統中的中間結果；由於 x 是物件而不是函式，且 FP 系統不將函式與物件關聯，因此它在 FP 系統中是無意義的。現在如果 APPLY 表示 apply，則 (APPLY:<NULL,A>) 的意義是

μ(APPLY:<NULL,A>)
= μ((ρAPPLY):<NULL,A>)
= μ(apply:<NULL,A>)
= μ(NULL:A) = μ((ρNULL):A)
= μ(null:A) = μF = F.

最後一步來自事實，即每個物件都是它自己的意義。由於意義函式 μ 最終會評估所有應用，可以認為 apply:<NULL,A> 產生 F，儘管實際結果是 (NULL:A)。

13.3.2 物件如何表示函式；表示函式 ρ。正如我們所見，一些原子（原始原子）將表示系統的原始函式。其他原子可以表示定義的函式，就像符號在 FP 系統中一樣。如果一個原子既不是原始的也不是定義的，它表示 ±，一個到處都為 ± 的函式。

序列也表示函式，類似於 FP 的函式形式。序列表示的函式由以下規則（遞迴地）給出。

元組合規則

(ρ<x1, ..., xn>):y = (ρx1):<<x1, ..., xn>, y>,

其中 xi 和 y 是物件。這裡 ρx1 決定了 <x1, ..., xn> 表示什麼函式形式，而 x2, ..., xn 是形式的參數（在 FFP 中，x1 本身也可以作為參數）。因此，例如，令 Def ρCONST = 2o1；那麼 FFP 中的 <CONST, x> 表示 FP 函式形式 x，因為根據元組合規則，如果 y ≠ ±，

(ρ<CONST, x>):y = (ρCONST):<<CONST, x>,y>
= 2 o 1:<<CONST, x>,y> = x.

這裡我們可以看到，序列或形式的第一個控制運算符，在本例中是 CONST，在元組合後始終以一個對作為其操作數，該對的第一個元素是序列本身，第二個元素是序列的原始操作數，在本例中是 y。然後控制運算符可以以各種方式重新排列並重新應用序列的元素和原始操作數。元組合的重要之處在於，它實際上僅通過定義新函式就可以定義新的函式形式。它也允許在沒有定義的情況下編寫遞迴函式。

我們再舉一個函式形式的控制函式範例：Def ρCONS = @applyotlodistr。這個定義的結果是 <CONS, f1, ..., fn>——其中 fi 是物件——表示與 [ρf1, ..., ρfn] 相同的函式。以下展示了這一點。

(ρ<CONS,f1, ..., fn>):x
= (μCONS):<<CONS, f1, ..., fn>,x>                   by metacomposition
= @applyotlodistr:<<CONS, f1, ..., fn>,x>              by def of ρCONS
= @apply:<<f1,x>, ..., <fn,x>>                       by def of tl and distr and o
= <apply:<f1,x>, ..., apply:<fn,x>>                   by def of @
= <(f1:x), ..., (fn:x)>                            by def of apply.

在評估最後一個表達式時，意義函式將為每個應用產生意義，給出 ρfi:x 作為第 i 個元素。

通常，在描述序列所表示的函式時，我們將給出其總體效果，而不是展示其控制運算符如何實現該效果。因此，我們將簡單寫

(ρ<CONS, f1, ..., fn>):x = <(f1:x), ..., (fn:x)>

而不是上面更詳細的描述。

我們需要一個控制運算符 COMP 來為我們提供表示函式形式組合的序列。我們將 ρCOMP 視為原始函式，使得對於所有物件 x，

(ρ<COMP,f1, ..., fn>):x = (f1:(f2:(... :(fn:x)...))) 對於 n ≥ 1。

（我感謝 Paul R. McJones 的觀察，他認為普通組合可以通過這個原始函式實現，而不是像早期論文 [2] 中那樣在基本語義中使用兩個組合規則。）

儘管 FFP 系統允許定義和研究新的函式形式，但預期大多數程式設計會使用固定的形式集合（其控制運算符是原始的），就像 FP 中一樣，以便可以應用這些形式的代數法則，並且可以使用基於這些形式的結構化程式設計風格。

除了用於定義函式形式外，元組合還可以用於直接創建遞迴函式，而無需使用形式為 Def f = E(f) 的遞迴定義。例如，如果 ρMLAST = nullotlo2 → lo2; applyo[1, tlo2]，那麼 ρ<MLAST> = last，其中 last:x = x = <x1, ..., xn> → xn; ±。因此，運算符 <MLAST> 的工作方式如下：

μ(<MLAST>:<A,B>)
= μ(ρMLAST:<<MLAST>,<A,B>>)                        by metacomposition
= μ(applyo[1, tlo2]:<<MLAST>,<A,B>>)
= μ(apply:<<MLAST>,<B>>)
= μ(<MLAST>:<B>)
= μ(ρMLAST:<<MLAST>,<B>>)
= μ(lo2:<<MLAST>,<B>>)
= B.

13.3.3 ρ 與 μ 的性質總結。到目前為止，我們已經展示了 ρ 如何將原子和序列映射到函式，以及這些函式如何將物件映射到表達式。實際上，ρ 和所有 FFP 函式都可以擴展，以便它們對所有表達式定義。通過這些擴展，可以總結 ρ 和 μ 的性質如下：

  1. μ ∈ [表達式 → 物件]。
  2. 如果 x 是一個物件，則 μx = x。
  3. 如果 e 是一個表達式，且 e = <e1, ..., en>，則 μe = <μe1, ..., μen>。
  4. ρ ∈ [表達式 → [表達式 → 表達式]]。
  5. 對於任何表達式 e，ρe = ρ(μe)。
  6. 如果 x 是一個物件且 e 是一個表達式，則 ρx:e = ρx:(μe)。
  7. 如果 x 和 y 是物件，則 μ(x:y) = μ(ρx:y)。換句話說：FFP 應用 (x:y) 的意義是通過將由 x 表示的函式 ρx 應用於 y，然後找到結果表達式（通常是一個物件，此時它就是它自己的意義）的意義來找到的。

13.3.4 單元格 (Cells)、提取 (fetching) 與儲存 (storing)。由於多種原因，創建作為名稱的函式很方便。特別是，我們在描述 FFP 系統中定義的語義時將需要此功能。為了引入命名函式，即能夠從儲存（一個序列的單元格）中提取具有給定名稱的單元格內容，並將具有給定名稱和內容的單元格儲存在這樣的序列中，我們引入稱為單元格的物件和兩個新的函式形式，fetch 和 store。

單元格 (Cells) 單元格是一個三元組 <CELL, name, contents>。我們使用此形式而不是對 <name, contents>，以便將單元格與普通對區分開來。

提取 (Fetch) 函式形式 fetch 將物件 n 作為其參數（n 通常是一個原子，用作名稱）；它寫作 l'n（讀作「fetch n」）。其對於物件 n 和 x 的定義是

l'n:x = x=φ → #; atom:x → ±; (1:x) = <CELL,n,c> → c; l'n o tl:x,

其中 # 是原子「default」。因此，l'n (fetch n) 應用於序列，給出序列中第一個名稱為 n 的單元格的內容；如果沒有名稱為 n 的單元格，結果是 default，#。因此，l'n 是名稱 n 的名稱函式。（我們假設 ρFETCH 是原始函式，使得 ρ<FETCH, n> = l'n。注意 l'n 只是跳過其操作數中不是單元格的元素。）

儲存 (Store) 和 push, pop, purge 像 fetch 一樣，store 將物件 n 作為其參數；它寫作 !n（讀作「store n」）。當應用於對 <x,y> 時，其中 y 是一個序列，!n 會移除 y 中第一個名稱為 n 的單元格（如果有的話），然後創建一個名稱為 n、內容為 x 的新單元格，並將其附加到 y。在定義 !n (store n) 之前，我們將指定四個輔助函式形式。（這些可以與 fetch n 和 store n 組合使用，以在一個儲存序列中獲得多個、具名的 LIFO 堆疊。）這些輔助形式中有兩個是由遞迴函式方程指定的；每個都將物件 n 作為其參數。

(cellname n) = atom → F; eqo[length, 3] → eqo[[CELL, 1], [_n_, 2]]; ±
(push n) = pair → apndlo[[CELL, _n_, 1], 2]; ±
(pop n) = null → φ; (cellname n)o 1 → tl; apndlo[1, (pop n)otl]
(purge n) = null → φ; (cellname n)o 1 → (purge n)otl; apndlo[1, (purge n)otl]
!n = pair → (push n)o[1, (pop n)o2]; ±

上述函式形式的工作方式如下。對於 x ≠ ±，(cellname n):x 若 x 是名稱為 n 的單元格則為 T，否則為 F。(pop n):y 從序列 y 中移除第一個名稱為 n 的單元格；(purge n):y 從 y 中移除所有名稱為 n 的單元格。(push n):<x,y> 將一個名稱為 n、內容為 x 的單元格放在序列 y 的開頭；!n:<x,y> 是 (push n):<x, (pop n):y>。

（因此，(push n):<x,y> = y' 將 x 推到 y' 中名為 n 的「堆疊」頂部；x 可以通過 l'n:y' = x 讀取，並且可以通過 (pop n):y' 移除；因此 l'no(pop n):y' 是堆疊 n 中 x 下方的元素，前提是 y' 中有名稱為 n 的單元格不止一個。）

13.3.5 FFP Systems 中的定義。FFP 系統的語義取決於固定的定義集 D（一個單元格序列），就像 FP 系統依賴於其非正式給定的定義集一樣。因此，語義函式 μ 取決於 D；更改 D 會產生新的 μ'，反映更改後的定義。我們將 D 表示為一個物件，因為在 AST 系統（第 14 節）中，我們將通過將函式應用於 D 來轉換 D，並從中提取數據——此外還將其用作 FFP 語義中函式定義的來源。

如果 <CELL,n,c> 是序列 D 中第一個名稱為 n 的單元格（且 n 是一個原子），則它與 FP 定義 Def n = μc 具有相同的效果，即 (n:x) 的意義將與 μc:x 的意義相同。因此，例如，如果 <CELL, CONST, <COMP, 2, 1>> 是 D 中第一個名稱為 CONST 的單元格，則它與 Def CONST = 2o1 具有相同的效果，且具有該 D 的 FFP 系統會發現

μ(CONST:<<x,y>,z>) = y

並且因此

μ(<CONST, A>:B) = A.

通常，在具有定義 D 的 FFP 系統中，形式為 (atom:x) 的應用的意義取決於 D；如果 l'atom:D ≠ #（也就是說，atom 在 D 中已定義），則其意義為 μ(c:x)，其中 c = l'atom:D，即 D 中第一個名稱為 atom 的單元格的內容。如果 l'atom:D = #，則 atom 在 D 中未定義，此時 atom 要麼是原始的，即系統知道如何計算 ρatom:x，並且 μ(atom:x) = μ(ρatom:x)，否則 μ(atom:x) = ±。

13.4 FFP Systems 的形式語義

我們假設已經選擇了一組原子 A、一組定義 D、一組原始原子 P ⊂ A 及其表示的原始函式。我們假設如果 a 屬於 P，則 ρa 是由 a 表示的原始函式，如果 a 屬於 Q（A-P 中未在 D 中定義的原子集），則 ρa = ±。儘管 μ 對所有表達式都已定義（參見 13.3.3），形式語義僅在其對 P 和 Q 的定義中使用它。ρ 賦予其他表達式 x 的函式，在以下用於評估 μ(x:y) 的語義規則中是隱含確定和應用的。上述對 A 和 D 以及 P 和相關原始函式的選擇決定了 FFP 系統的物件、表達式和語義函式 μD。（我們將 D 視為固定，並寫 μ 代替 μD。）我們假設 D 是一個序列，並且對於任何原子 y，可以計算 l'y:D（由函式 l'y 如第 13.3.4 節給出）。有了這些假設，我們將 μ 定義為函式 ψ 的最小不動點，其中函式 ψμ 對於任何函式 μ（對所有表達式 x, xi, y, yi, z, 和 w）定義如下：

(ψμ)x = x ∈ A → x;
       x = <x1, ..., xn> → <μx1, ..., μxn>;
       x = (y:z) →
         (y ∈ A & (l'y:D) = # → μ((ρy)(μz));
          y ∈ A & (l'y:D) = w → μ(w:z);
          y = <y1, ..., yn> → μ(y1:<y,z>); μ(γμ:z)); ±

上述關於 μ 的描述通過定義和元組合擴展了應用的運算符，然後再評估操作數。假設上述定義中像「x ∈ A」這樣的謂詞是 ± 保留的（例如，「± ∈ A」的值為 ±），並且條件表達式本身也是 ± 保留的。因此 (ψμ)± = ± 且 (ψμ)(±:z) = ±。這結束了 FFP 系統的語義描述。

14. 應用式狀態轉換系統 (AST Systems)

14.1 介紹

本節概述了一類系統，它們是 Von Neumann 系統的替代方案。必須再次強調，這些應用式狀態轉換系統目前的形式不是作為實用程式設計系統提出的，而是作為一類系統的範例，其中應用式風格程式設計在歷史敏感但非 Von Neumann 的系統中得以實現。這些系統與狀態鬆散耦合，並依賴於底層應用式系統來實現其程式設計語言和狀態轉換的描述。以下描述的 AST 系統的底層應用式系統是一個 FFP 系統，但也可以使用其他應用式系統。

要理解 AST 系統結構的原因，首先回顧 Von Neumann 系統 Algol 的基本結構，觀察其局限性，並將其與 AST 系統的結構進行比較是有幫助的。回顧後，將描述一個最小的 AST 系統；給出一個小型、由上而下、自我保護的檔案維護和運行使用者程式的系統程式，並說明如何在 AST 系統中安裝它以及如何運行使用者程式範例。系統程式使用「名稱函式」而不是傳統名稱，使用者也可以這樣做。本節以討論 AST 系統的變體、其一般性質和命名系統的子節結束。

14.2 Algol 的結構與 AST Systems 的結構比較

Algol 程式是一個語句序列，每個語句代表 Algol 狀態的轉換，而 Algol 狀態是關於各種堆疊、指針以及標識符到值映射狀態的複雜儲存庫。每個語句通過其自身以及其不同部分特有的複雜協議與這個不斷變化的狀態進行通信（例如，與變數 x 相關聯的協議取決於它在指派語句左側還是右側、聲明中、參數中等位置的出現）。就好像 Algol 狀態是一個複雜的「儲存」，通過一個巨大的、多種專用線路的「電纜」與 Algol 程式通信。這個電纜的複雜通信協議是固定的，包括針對每種語句型別的協議。Algol 程式的「意義」必須根據通過電纜及其協議與狀態進行大量通信的總體效果來給出（加上用於識別輸出並將輸入插入狀態的方法）。

與連接 Algol 狀態/儲存的巨大電纜相比，作為電腦 Von Neumann 瓶頸的電纜是一個簡單、優雅的概念。

因此，Algol 語句不是表示狀態到狀態函式的表達式，這些表達式通過使用有序的組合形式從更簡單的狀態到狀態函式構建而來。相反，它們是具有上下文相關部分的複雜消息，這些部分蠶食著狀態。每個部分通過其自身協議在電纜上傳輸信息到狀態並從狀態中獲取信息。沒有規定將通用函式應用於整個狀態，從而對其進行大範圍更改。通過函式應用，對狀態 S 進行大規模、強大轉換的可能性，S → f:S，在 Von Neumann-電纜和協議-上下文下是不可想像的：除非 f 僅限於電纜最初允許的微小更改，否則無法保證新狀態 f:S 會匹配電纜及其固定的協議。

我們希望一個計算系統，其語義不依賴於大量複雜協議來與狀態通信，並且我們希望能夠通過應用通用函式來對狀態進行大規模轉換。AST 系統提供了一種實現這些目標的方法。它們的語義有兩個從狀態獲取信息的協議：（1）從中獲取要應用的函式的定義，以及（2）獲取整個狀態本身。有一個更改狀態的協議：通過函式應用計算新狀態。除了這些與狀態的通信外，AST 語義是應用式的（即 FFP）。它不依賴於狀態更改，因為在計算過程中狀態根本不改變。相反，計算結果是輸出和新狀態。AST 狀態的結構被其一個協議稍微限制：必須能夠在其內部識別一個定義（即單元格）。它的結構——它是一個序列——比 Algol 狀態的結構簡單得多。

因此，AST 系統的結構避免了 Von Neumann 狀態的複雜性和限制（及其通信協議），同時在一個根本不同且更簡單的框架中實現了更大的能力和自由。

14.3 AST System 的結構

AST 系統由三個要素組成：

  1. 一個應用式子系統（如 FFP 系統）。
  2. 一個狀態 D，它是應用式子系統的定義集。
  3. 一組轉換規則，描述輸入如何轉換為輸出以及狀態 D 如何改變。

AST 系統的程式語言就是其應用式子系統的語言。（從現在起，我們將假設後者是一個 FFP 系統。）因此，AST 系統可以使用我們討論過的 FP 程式設計風格。應用式子系統不能更改狀態 D，並且在評估表達式期間它不會改變。一個新狀態與輸出一起計算出來，並在輸出發出時替換舊狀態。（記住，一組定義 D 是一個單元格序列；單元格名稱是定義函式的名稱，其內容是定義表達式。然而，在這裡，一些單元格可能命名數據而不是函式；數據名稱 n 將用於 l'n (fetch n)，而函式名稱將作為運算符本身使用。）

我們在下方給出了我們將用於程式範例的基本 AST 系統的轉換規則。這些規則也許是許多可能轉換規則中最簡單的，這些規則可以決定各種 AST 系統的行為。

14.3.1 基本 AST System 的轉換規則。當系統接收到輸入 x 時，它形成應用 (SYSTEM:x)，然後使用當前狀態 D 作為定義集，在 FFP 子系統中獲取其意義。SYSTEM 是在 D 中定義的函式的特殊名稱（即，它是「系統程式」）。通常結果是一個對

μ(SYSTEM:x) = <o,d>

其中 o 是輸入 x 產生的系統輸出，d 成為系統下一個輸入的新狀態 D。通常 d 將是舊狀態的副本或部分更改的副本。如果 μ(SYSTEM:x) 不是一個對，則輸出是一個錯誤消息，狀態保持不變。

14.3.2 轉換規則：例外條件與啟動。一旦接受了輸入，我們的系統將不會接受另一個輸入（除了 <RESET, x>，見下），直到輸出已發出且新狀態（如果有的話）已安裝。系統隨時可以接受輸入 <RESET, x>。有兩種情況：(a) 如果 SYSTEM 在當前狀態 D 中已定義，則系統中止當前計算，不改變 D，並將 x 視為新的正常輸入；(b) 如果 SYSTEM 在 D 中未定義，則 x 被附加到 D 作為其第一個元素。（這結束了我們基本 AST 系統的轉換規則的完整描述。）

如果 SYSTEM 在 D 中已定義，它總是能阻止其自身定義的任何改變。如果它未定義，普通輸入 x 將產生 μ(SYSTEM:x) = ±，轉換規則將產生「錯誤消息」和未改變的狀態；另一方面，輸入 <RESET, <CELL, SYSTEM, s>> 將定義 SYSTEM 為 s。

14.3.3 程式對狀態的存取；函式 ρDEFS。我們的 FFP 子系統需要有一個新的原始函式 defs，名稱為 DEFS，對於任何物件 x ≠ ±，使得

defs:x = ρDEFS:x = D

其中 D 是 AST 系統的當前狀態和定義集。此函式允許程式為了任何目的存取整個狀態，包括計算後繼狀態的核心目的。

14.4 系統程式範例

上述對我們基本 AST 系統的描述，加上 FFP 子系統以及早期章節的 FP 原始函式和函式形式，指定了一個完整的歷史敏感計算系統。它的輸入和輸出行為受到其簡單轉換規則的限制，但除此之外，一旦配備了合適的定義集，它就是一個強大的系統。作為其用途的一個例子，我們將描述一個小型系統程式、其安裝和操作。

我們的範例系統程式將處理它維護的檔案的查詢和更新，評估 FFP 表達式，運行不損壞檔案或狀態的通用使用者程式，並允許授權使用者更改定義集和系統程式本身。它接受的所有輸入都將是 <key, input> 的形式，其中 key 是一個代碼，它決定輸入類別（系統更改、表達式、程式、查詢、更新）以及使用者身份及其使用系統進行給定輸入類別的權限。我們將不指定 key 的格式。Input 是輸入本身，屬於 key 給定的類別。

14.4.1 系統程式的一般計劃。我們的 AST 系統的狀態 D 將包含系統程式和使用者程式所需的所有非原始函式的定義。（每個定義都在序列 D 的一個單元格中。）此外，D 中將有一個名稱為 FILE 的單元格，其內容為 file，由系統維護。我們將給出函式的 FP 定義，稍後展示如何以其 FFP 形式將它們載入到系統中。轉換規則使輸入成為 SYSTEM 的操作數，但我們的計劃是使用名稱函式來引用數據，所以我們對輸入做的第一件事是創建兩個名稱為 KEY 和 INPUT 的單元格，其內容分別為 key 和 input，並將它們附加到 D。這個單元格序列包含 key、input 和 file 各一個；它將是我們稱為 subsystem 的主函式的操作數。Subsystem 然後可以通過將 l'KEY 應用於其操作數等方式來獲取 key。因此，定義

Def system = pair → subsystemof; [NONPAIR, defs]

其中

f = !INPUTo[2, !KEYo[1, defs]]

使系統在輸入不是對時輸出 NONPAIR 並保持狀態不變。否則，如果輸入是 <key, input>，則

f:<key, input> = <<CELL,INPUT, input>, <CELL,KEY, key>, d1, ..., dn>

其中 D = <d1, ..., dn>。（我們本來可以構造一個與上面不同的操作數，一個只有三個單元格的操作數，用於 key、input 和 file。我們沒有這樣做是因為真實程式不像 subsystem，會包含許多引用狀態中數據的名稱函式，而這種操作數的「標準」構造也足夠用了。）

14.4.2 「子系統」(subsystem) 函式。我們現在給出函式 subsystem 的 FP 定義，隨後簡要解釋其六種情況和輔助函式。

Def subsystem =
  is-system-changeo l'KEY → [report-change, apply]o[l'INPUT, defs];
  is-expression o l'KEY → [l'INPUT, defs];
  is-programo l'KEY → system-check o applyo[l'INPUT, defs];
  is-queryol'KEY → [query-responseo[l'INPUT, l'FILE], defs];
  is-updateo l'KEY → [report-update, !FILEo[update, defs]]
                 o[l'INPUT, l'FILE];
  [report-erroro[l'KEY, l'INPUT], defs].

這個 subsystem 有五個「... → ...;」子句和一個最終的默認函式，總共有六種類型的輸入；每種類型的處理方法如下。回想一下，subsystem 的操作數是一個單元格序列，包含 key、input 和 file，以及 D 中所有定義的函式，並且 subsystem:operand = <output, newstate>。

默認輸入。在這種情況下，當 key 不滿足前面任何子句時，結果由定義的最後一個（默認）函式給出。輸出是 report-error: <key, input>。狀態保持不變，因為它由 defs:operand = D 給出。（我們留給讀者自行想像函式 report-error 將從其操作數生成什麼。）

系統更改輸入。當 is-system-change o l'KEY:operand = is-system-change:key = T 時，key 指定使用者被授權進行系統更改，並且 input = l'INPUT:operand 表示一個函式 f，它將應用於 D 以產生新狀態 f:D。（當然，f:D 可以是一個無用的新狀態；對它沒有施加任何約束。）輸出是一個報告，即 report-change: <input, D>。

表達式輸入。當 is-expression:key = T 時，系統理解輸出將是 FFP 表達式 input 的意義；l'INPUT:operand 產生它，並且像所有表達式一樣被評估。狀態保持不變。

程式輸入和系統自我保護。當 is-program:key = T 時，輸出和新狀態都由 (ρinput):D = <output, newstate> 給出。如果 newstate 包含狀況合適的 file 以及 system 和其他受保護函式的定義，則 system-check: <output, newstate> = <output, newstate>。否則，system-check: <output, newstate> = <error-report, D>。雖然程式輸入在產生 newstate 時可以對狀態進行主要、可能是災難性的更改，system-check 可以使用任何標準來決定是允許其成為實際的新狀態還是保留舊狀態。一個更複雜的 system-check 可能只糾正狀態中的禁止更改。這類函式之所以可能，是因為它們總是能存取舊狀態以與待定的新狀態進行比較，並控制最終允許哪種狀態轉換。

檔案查詢輸入。如果 is-query:key = T，函式 query-response 旨在從其操作數 <input,file> 產生對查詢 input 的輸出 = 答案。

檔案更新輸入。如果 is-update:key = T，input 指定由函式 update 理解的檔案交易，該函式計算 updated-file = update: <input,file>。因此 !FILE 以 <updated-file, D> 作為其操作數，從而在新狀態的單元格 FILE 中儲存更新後的 file。狀態的其餘部分保持不變。函式 report-update 從其操作數 <input,file> 生成輸出。

14.4.3 安裝系統程式。我們已經通過一些 FP 定義描述了稱為 system 的函式（使用了行為僅被暗示的輔助函式）。讓我們假設我們已經有了所需所有非原始函式的 FP 定義。然後，每個定義都可以轉換為 D 中單元格的名稱和內容（當然，這種轉換本身將由一個更好的系統來完成）。轉換是通過將每個 FP 函式名稱更改為其等價的原子（例如，update 變為 UPDATE），並將函式形式替換為其第一個成員是特定形式控制函式的序列。因此，!FILEo[update, defs] 被轉換為

<COMP,<STORE, FILE>, <CONS, UPDATE, DEFS>>,

並且這個 FP 函式與由該 FFP 物件表示的函式相同，前提是 update = ρUPDATE 並且 COMP、STORE 和 CONS 表示組合、儲存和構造的控制函式。

所有我們的系統所需的 FP 定義都可以如上所示轉換為單元格，得到序列 D0。我們假設 AST 系統一開始是空狀態，因此 SYSTEM 未定義。我們希望 SYSTEM 最初被定義為安裝其下一個輸入作為狀態；完成後，我們就可以輸入 D0，並且所有我們的定義都將被安裝，包括我們的程式——system——本身。為了實現這一點，我們輸入第一個輸入

<RESET, <CELL, SYSTEM, loader>>

其中 loader = <CONS, <CONST, DONE>, ID>。然後，根據 RESET 的轉換規則（當 SYSTEM 在 D 中未定義時），輸入中的單元格被放置在 D = φ 的開頭，從而定義了 ρSYSTEM = ρloader = [DONE, id]。我們的第二個輸入是 D0，我們希望它成為狀態的定義集。常規轉換規則導致 AST 系統評估

μ(SYSTEM:D0) = [DONE, id]:D0 = <DONE, D0>.

因此，我們第二個輸入的輸出是 DONE，新狀態是 D0，並且 ρSYSTEM 現在是我們的系統程式（它只接受形式為 <key, input> 的輸入）。

我們的下一個任務是載入檔案（我們給定了一個初始值 file）。為了載入它，我們向新安裝的系統輸入一個程式，該程式包含 file 作為常數並將其儲存在狀態中；輸入是

<program-key, [DONE, store-file]>

其中 ρstore-file = !FILEo[file, id]。 program-key 將 [DONE, store-file] 識別為應用於狀態 D0 的程式，以獲得輸出和新狀態 D1，即：

ρstore-file:D0 = !FILEo[file, id]:D0,

或 D0，其開頭包含 file 的單元格。輸出是 DONE:D0 = DONE。我們假設 system-check 將不改變地通過 <DONE, D1>。在上述中，FP 表達式已代替它們所表示的 FFP 物件使用，例如 DONE 代表 <CONST, DONE>。

14.4.4 使用系統。我們沒有說明系統的檔案、查詢或更新的結構，因此無法給出檔案操作的詳細範例。然而，subsystem 的結構清楚地展示了系統對查詢和更新的響應如何依賴於函式 query-response、update 和 report-update。

假設在 D 中儲存了名稱為 M 和 N 的矩陣 m 和 n，並且在 D 中定義了我們之前描述的函式 MM。那麼輸入

<expression-key, (MMo[!M, !N]o DEFS:#)>

將以兩個矩陣的乘積作為輸出，且狀態不變。expression-key 將應用識別為要評估的表達式，並且由於 defs:# = D 且 [!M, !N]:D = <m,n>，表達式的值是結果 MM:<m,n>，這就是輸出。

我們的小型系統程式沒有提供將控制權交給使用者程式來處理許多輸入的功能，但賦予它此功能並不困難，同時仍然可以使用 system-check 監視使用者程式並有權收回控制權。

14.5 AST Systems 的變體

上述 AST 系統的一個主要擴展將提供組合形式，「系統形式」，用於從更簡單的組件 AST 系統構建新的 AST 系統。也就是說，一個系統形式將以 AST 系統作為參數，並生成一個新的 AST 系統，就像函式形式以函式作為參數並生成新函式一樣。這些系統形式將具有類似於函式形式的屬性，並將成為有用「系統代數」的「運算」，就像函式形式是程式代數的「運算」一樣。然而，找到有用的系統形式的問題要困難得多，因為它們必須處理 RESET、匹配輸入和輸出，並組合歷史敏感系統而不是固定函式。

此外，系統形式的有用性或必要性不如函式形式明確。後者對於從初始原始集合構建各種函式是必不可少的，而即使沒有系統形式，構建 AST 系統的設施已經非常豐富，可以構建幾乎任何系統（具有給定 AST 方案允許的通用輸入和輸出特性）。也許系統形式對於構建具有複雜輸入和輸出安排的系統會很有用。

14.6 關於 AST Systems 的補充說明

正如我上面試圖指出的，AST 系統的組成部分可能有無數種變體——它如何操作、如何處理輸入和輸出、如何以及何時產生新狀態等等。無論如何，許多評論適用於任何合理的 AST 系統： a) 每次主要計算都會發生一次狀態轉換，並且可以具有有用的數學性質。狀態轉換不像傳統語言那樣涉及計算的最微小細節；因此，語言學上的 Von Neumann 瓶頸已經消除。不需要複雜的「電纜」或協議來與狀態通信。 b) 程式以應用式語言編寫，該語言可以容納各種可變換部分，這些部分的能力和靈活性超過迄今為止任何 Von Neumann 語言。逐字元風格被應用式風格取代；程式設計沒有表達式世界和語句世界之分。程式可以通過程式代數進行分析和優化。 c) 由於在計算 system:x 期間狀態無法改變，因此沒有副作用。因此，獨立的應用可以並行評估。 d) 通過定義適當的函式，我相信可以隨時引入主要的新功能，使用相同的框架。這些功能必須構建到 Von Neumann 語言的框架中。我想到的是諸如：具有各種命名系統的「儲存」，型別和型別檢查，通信並行處理，不確定性和 Dijkstra 的「保護命令」結構 [8]，以及改進結構化程式設計的方法。 e) AST 系統的框架包括底層應用式系統的語法和語義以及上述概略的系統框架。按照現行標準，這是語言的一個微小框架，並且是系統中唯一固定的部分。

14.7 AST 與 Von Neumann 模型中的命名系統

在 AST 系統中，命名通過函式完成，如第 13.3.4 節所述。可以定義許多用於更改和存取儲存的有用函式（例如，push, pop, purge, typed fetch 等）。所有這些定義及其相關命名系統都可以在不更改 AST 框架的情況下引入。不同類型的「儲存」（例如，具有「類型化單元格」）及其各自的命名系統可以用在同一個程式中。一個儲存中的單元格可能包含另一個完整的儲存。

關於 AST 命名系統的重要一點是，它們利用了名稱的函式性質（Reynolds 的 GEDANKEN [19] 在 Von Neumann 框架內也在一定程度上做到了這一點）。因此，名稱函式可以通過函式形式與其他函式組合。相比之下，Von Neumann 語言中的函式和名稱通常是分離的概念，名稱的函式性質幾乎完全隱藏且無用，因為 a) 名稱不能作為函式應用；b) 沒有通用的方法將名稱與其他名稱和函式組合；c) 名稱函式應用的對象（儲存）無法作為物件存取。

Von Neumann 語言未能將名稱視為函式可能是其更重要的弱點之一。無論如何，能夠使用名稱作為函式並將儲存視為物件，可能會成為一個有用且重要的程式設計概念，值得深入探索。

15. 關於電腦設計的補充說明

Von Neumann 語言的主導地位使得設計者在實用電腦設計方面幾乎沒有除了 Von Neumann 電腦變體之外的智力模型。資料流模型 [1][7][13] 是歷史敏感模型的一類替代方案。基於 lambda 演算的語言的替換規則給機器設計者帶來了嚴重的問題。Berkling [3] 開發了一種修改過的 lambda 演算，它有三種類型的應用，並且使得變數重新命名變得不必要。他開發了一台機器來評估這種語言的表達式。需要進一步的經驗來證明這種語言作為一種有效程式設計風格的基礎是否健全，以及他的機器能有多高效。

Magó [15] 開發了一台由相同組件（兩種）構建的新穎應用式機器。它直接、由下而上地評估 FP 類和其他應用式表達式。它沒有 Von Neumann 儲存和地址暫存器，因此沒有瓶頸；它能夠並行評估許多應用；其內建運算更類似於 FP 運算符，而不是 Von Neumann 電腦運算。這是我見過的最遠離 Von Neumann 電腦的設計。

有許多跡象表明，應用式程式設計風格可能比 Von Neumann 風格更強大。因此，程式設計師開發一類新的歷史敏感計算系統模型非常重要，這些模型體現這種風格，並避免似乎依附於基於 lambda 演算系統的固有效率問題。只有當這些模型及其應用式語言證明其優於傳統語言時，我們才會有經濟基礎來開發最能實現它們的新型電腦。也許只有那時，我們才能充分利用大型集成電路進行不受 Von Neumann 瓶頸限制的電腦設計。

16. 總結

本文前面的十五節可以總結如下。

第 1 節。傳統程式語言龐大、複雜、僵化。其有限的表達能力不足以證明其規模和成本的合理性。

第 2 節。支撐程式語言的計算系統模型粗略分為三類：(a) 簡單運算模型（例如，圖靈機），(b) 應用式模型（例如，lambda 演算），以及 (c) Von Neumann 模型（例如，傳統電腦和程式語言）。每一類模型都有一個重要的難點：(a) 類程式難以理解；(b) 類模型無法保存從一個程式到下一個程式的信息；(c) 類模型具有無法使用的基礎和概念上無用的程式。

第 3 節。Von Neumann 電腦圍繞著一個瓶頸構建：連接 CPU 和儲存裝置的逐字元管。由於程式必須通過在 Von Neumann 瓶頸來回泵送大量字元來實現其對儲存裝置的整體更改，我們已經養成了一種程式設計風格，它關注的是通過這個瓶頸的逐字元流量，而不是我們問題的更大概念單元。

第 4 節。傳統語言基於 Von Neumann 電腦的程式設計風格。因此，變數=儲存單元；指派語句=讀取、儲存和算術；控制語句=跳轉和測試指令。符號「:=」是語言學上的 Von Neumann 瓶頸。用傳統的 Von Neumann 語言程式設計仍然關注通過這個稍微複雜一些的瓶頸的逐字元流量。Von Neumann 語言還將程式設計分割為表達式世界和語句世界；前者是一個有序的世界，後者是一個無序的世界，結構化程式設計在一定程度上簡化了這個世界，但沒有解決分裂本身和傳統語言逐字元風格的基本問題。

第 5 節。本節比較了 Von Neumann 程式和內積的函式程式。它說明了前者的一些問題和後者的一些優點：例如，Von Neumann 程式是重複的、逐字元的，只適用於長度為 n 的命名為 a 和 b 的兩個向量，只能通過使用具有複雜語義的程序聲明來實現通用性。函式程式是非重複的，將向量作為單元處理，層次結構更強，完全通用，並通過組合高層次的內務處理運算符來創建「內務處理」運算。它不命名其參數，因此不需要程序聲明。

第 6 節。程式語言包含一個框架加上一些可變換部分。Von Neumann 語言的框架要求大多數功能必須內建其中；它只能容納有限的可變換部分（例如，使用者定義的程序），因為「狀態」及其轉換規則中必須有詳細的規定來滿足可變換部分以及內建到框架中的所有功能的需求。Von Neumann 框架如此僵化的原因是其語義與狀態耦合得太緊密：計算的每個細節都改變狀態。

第 7 節。Von Neumann 語言的可變換部分表達能力很弱；這就是為什麼大部分語言必須內建到框架中。表達能力弱的原因是 Von Neumann 語言無法有效地使用組合形式來構建程式，這又是由表達式和語句之間的分裂引起的。組合形式在表達式中發揮最佳作用，但在 Von Neumann 語言中，表達式只能產生一個單字元；因此表達式世界中的表達能力大部分喪失了。使用組合形式的另一個障礙是命名約定的繁複使用。

第 8 節。APL 是第一個不基於 lambda 演算、不是逐字元且使用函式組合形式的語言。但它仍然保留了 Von Neumann 語言的許多問題。

第 9 節。Von Neumann 語言沒有用於程式推理的有用屬性。公理語義和指稱語義是描述和理解傳統程式的精確工具，但它們只談論程式，不能改變其笨拙的屬性。與 Von Neumann 語言不同，普通代數語言既適用於陳述其法則，也適用於將方程轉換為其解，所有這些都在「語言」內部進行。

第 10 節。在歷史敏感語言中，程式可以通過更改系統保存的某些儲存來影響後續程式的行為。任何這種語言都需要某種狀態轉換語義。但它不需要語義與狀態緊密耦合，其中狀態隨計算的每個細節而變化。提出「應用式狀態轉換」(AST) 系統作為 Von Neumann 系統的歷史敏感替代方案。這些系統具有：(a) 鬆散耦合的狀態轉換語義，其中轉換在每次主要計算中發生一次；(b) 簡單的狀態和轉換規則；(c) 一個具有簡單「化簡」語義的底層應用式系統；以及 (d) 基於底層應用式系統及其語義的程式語言和狀態轉換規則。接下來的四節描述了這種非 Von Neumann 語言和系統設計方法的要素。

第 11 節。描述了一類不使用變數的非正式函式程式設計 (FP) 系統。每個系統都由物件、函式、函式形式和定義構成。函式將物件映射到物件。函式形式組合現有函式以形成新函式。本節列出了原始函式和函式形式的範例，並提供了範例程式。它討論了 FP 系統的局限性和優點。

第 12 節。描述了一個「程式代數」，其變數範圍涵蓋 FP 系統的函式，其「運算」是系統的函式形式。列出約二十四個代數法則後，接著是一個證明非重複矩陣乘法程式與遞迴程式等價性的範例。下一小節陳述了兩個「展開定理」的結果，這些定理「求解」了兩類方程。這些解將這些方程中的「未知」函式表示為無限條件展開式，構成了其行為的分情況描述，並立即給出了終止的充要條件。這些結果用於推導一個「遞迴定理」和一個「迭代定理」，這些定理為一些中等通用且有用的「線性」方程類別提供了現成的展開式。這些定理的使用範例包括：(a) 遞迴和迭代階乘函式的正確性證明，以及 (b) 兩個迭代程式等價性的證明。最後一個範例處理「二次」方程，並證明其解是一個冪等函式。下一小節給出了兩個展開定理的證明。

將與 FP 系統相關聯的代數與 lambda 演算和其他應用式系統的相應代數進行比較。比較顯示，與更強大的古典系統相比，受嚴格限制的 FP 系統有一些優勢。提出了關於將函式演算法化簡為無限展開式以及在各種「延遲評估」方案中使用代數的問題。

第 13 節。本節描述了形式化函式程式設計 (FFP) 系統，這些系統擴展並精確定義了 FP 系統的行為。它們的語義比古典系統更簡單，並且可以通過簡單的不動點論證來證明其一致性。

第 14 節。本節比較了 Algol 的結構與應用式狀態轉換 (AST) 系統的結構。它描述了一個使用 FFP 系統作為其應用式子系統的 AST 系統。它描述了系統的簡單狀態和轉換規則。描述了一個用於 AST 系統的小型自我保護系統程式，以及如何安裝和使用它進行檔案維護和運行使用者程式。本節簡要討論了 AST 系統的變體以及可以在 AST 系統中定義和使用的函式命名系統。

第 15 節。本節簡要討論了應用式電腦設計方面的工作，以及開發和測試更實用應用式系統模型以作為未來設計基礎的必要性。

致謝。在與本文相關的早期工作中，我從 Paul R. McJones 和 Barry K. Rosen 那裡獲得了許多寶貴的幫助和建議。在準備本文過程中，我獲得了大量寶貴的幫助和回饋。James N. Gray 非常慷慨地花費時間和知識審閱了初稿。Stephen N. Zilles 也仔細閱讀了它。在這個困難的階段，兩人都提出了許多寶貴的建議和批評。我很榮幸向他們表示我的感謝。我還與 Ronald Fagin, Paul R. McJones, 和 James H. Morris, Jr. 就初稿進行了有益的討論。Fagin 建議了對定理證明的一些改進。

由於本文大部分內容是技術性的，我邀請了兩位傑出的電腦科學家審稿第三稿。David J. Giles 和 John C. Reynolds 慷慨地接受了這項繁重的工作。兩人為我提供了大量詳細的修改建議和整體評論，這使得最終版本（他們沒有機會審閱）有了許多大大小小的改進。我真誠感謝他們投入寶貴的時間和精力來審閱本文。

最後，我還將第三稿的副本發送給 Gyula A. Magó, Peter Naur, 和 John H. Williams。他們慷慨地回覆了許多非常有幫助的評論和修改。北卡羅來納大學的 Geoffrey A. Frank 和 Dave Tolle 審閱了 Magó 的副本，並指出了 FFP 系統語義函數定義中的一個重要錯誤。我衷心感謝所有這些善良的人提供的幫助。

參考文獻

  1. Arvind, and Gostelow, K.P. A new interpreter for data flow schemas and its implications for computer architecture. Tech. Rep. No. 72, Dept. Comptr. Sci., U. of California, Irvine, Oct. 1975.
  2. Backus, J. Programming language semantics and closed applicative languages. Conf. Record ACM Symp. on Principles of Programming Languages, Boston, Oct. 1973, 71-86.
  3. Berkling, K.J. Reduction languages for reduction machines. Interner Bericht ISF-76-8, Gesellschaft for Mathematik und Datenverarbeitung MBH, Bonn, Sept. 1976.
  4. Burge, W.H. Recursive Programming Techniques, Addison-Wesley, Reading, Mass., 1975.
  5. Church, A. The Calculi of Lambda-Conversion. Princeton U. Press, Princeton, N.J., 1941.
  6. Curry, H.B., and Feys, R. Combinatory Logic, Vol. 1. North-Holland Pub. Co., Amsterdam, 1958.
  7. Dennis, J.B. First version of a data flow procedure language. Tech. Mere. No. 61, Lab. for Comptr. Sci., M.I.T., Cambridge, Mass., May 1973.
  8. Dijkstra, E.W. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J., 1976.
  9. Friedman, D.P., and Wise, D.S. CONS should not evaluate its arguments. In Automata, Languages and Programming, S. Michaelson and R. Milner, Eds., Edinburgh U. Press, Edinburgh, 1976, pp. 257-284.
  10. Henderson, P., and Morris, J.H. Jr. A lazy evaluator. Conf. Record Third ACM Symp. on Principles of Programming Languages, Atlanta, Ga., Jan. 1976, pp. 95-103.
  11. Hoare, C.A.R. An axiomatic basis for computer programming. Comm. ACM 12, 10 (Oct. 1969), 576-583.
  12. Iverson, K. A Programming Language. Wiley, New York, 1962.
  13. Kosinski, P. A data flow programming language. Rep. RC 4264, IBM T.J. Watson Research Ctr., Yorktown Heights, N.Y., March 1973.
  14. Landin, P.J. The mechanical evaluation of expressions. Computer J. 6, 4 (1964), 308-320.
  15. Magó, G.A. A network of microprocessors to execute reduction languages. To appear in Int. J. Comptr. and Inform. Sci.
  16. Manna, Z., Ness, S., and Vuillemin, J. Inductive methods for proving properties of programs. Comm. ACM 16, 8 (Aug. 1973) 491-502.
  17. McCarthy, J. Recursive functions of symbolic expressions and their computation by machine, Pt. 1. Comm. ACM 3, 4 (April 1960), 184-195.
  18. McJones, P. A Church-Rosser property of closed applicative languages. Rep. RJ 1589, IBM Res. Lab., San Jose, Calif., May 1975.
  19. Reynolds, J.C. GEDANEN—a simple typeless language based on the principle of completeness and the reference concept. Comm. ACM 13, 5 (May 1970), 308-318.
  20. Reynolds, J..C. Notes on a lattice-theoretic approach to the theory of computation. Dept. Syst. and Inform, Sci., Syracuse U., Syracuse, N.Y., 1972.
  21. Scott, D. Outline of a mathematical theory of computation. Proc. 4th Princeton Conf. on Inform. Sci. and Syst., 1970.
  22. Scott, D. Lattice-theoretic models for various type-free calculi. Proc. Fourth Int. Congress for Logic, Methodology, and the Philosophy of Science, Bucharest, 1972.
  23. Scott, D., and Strachey, C. Towards a mathematical semantics for computer languages. Proc. Syrup. on Comptrs. and Automata, Polytechnic Inst. of Brooklyn, 1971.