深入理解運算原理｜從簡單的機器到無所不能的程式

程式的意義

|

59

形式

我們的形式語意旅程並非很具形式。我們並未重視數學符號，而且若將 Ruby 當作元語

言來用，也意謂相較於瞭解程式的方式，其實我們更注意執行程式的不同方式。正確的

指稱語意涉及到藉著將它們轉換成定義明確的數學物件來達到程式意義的核心，也與能

明確的以 Ruby

while

迴圈表示 SIMPLE

«while»

迴圈有關。

領域理論

（

domain theory

）這種數學分支專門是發展來提供指稱語意實

用的定義和物件，允許以部分有序集合的單調函式的定點為基礎的運算模

型。將程式『編譯』成數學函式可以瞭解程式，而領域理論的技巧可以用

來證明這些函式有趣的屬性。

另一方面，雖然我們只在 Ruby 模糊的描繪指稱語意，但我們操作語意的作法在精神上

更接近它的形式表示：我們

#reduce

和

#evaluate

方法的定義實際上只是數學推理規則

的 Ruby 轉譯。

找出含義

形式語意的重要應用就是提供程式語言含義的明確規範，而不是依賴更非正式的作法，

像是自然語言規格文件和『源自實作物的規格』。形式的規格也有其他用途，例如通常

用來證明語言的屬性，尤其是特定程式的屬性，證明語言的程式之間的相同意義，以及

安全轉譯程式的研究方式，在不改變其行為的情況下，讓它們更有效率。

舉例來說，由於操作語意非常接近直釋器的實作物，電腦科學家可以將適當的直釋器視

為語言的操作語意，然後證明那個語言的指稱語意的正確性，這意謂著證明直釋器和指

稱語意所提供的含義之間存在明顯的關係。

指稱語意的優點是操作語意更為抽象，藉由忽略程式如何執行的細節，並集中在改成如 ...