標籤:

Emacs之魂(五):變數的「指針」語義

1. 語義學

在計算理論中,形式語義學是關注計算模式和程序設計語言含義的嚴格的數學研究領域。

語言的形式語義是用數學模型去表達該語言描述的可能計算來給出的。

提供程序設計語言形式語義的方法很多,其中主要類別有:

操作語義(operational Semantics),指稱語義(denotational semantics),

公理語義(axiomatic semantics),代數語義(algebraic semantics)。

1.1 操作語義

將語言成分所對應的計算機系統的操作,作為該語言成分的語義,這樣的建模方式稱為操作語義學,

語言的操作語義應該是標準的,不應該依附於一個特定的計算機系統,

因此,人們使用抽象的機器和抽象的解釋程序來定義語言的操作語義。

操作語義學的基本思想來源於編譯器和解釋器,編譯器或者解釋器描述了程序語言的具體實現。

操作語義最早被用於定義Algol 68的語義,

1964年Peter Landin使用了SECD machine這種抽象機器,定義了表達式的操作語義。

1980年,Gordon Plotkin提出了結構操作語義(structured operational semantics),它在更一般的數學結構上用歸約關係(reduction relation)建立了語義的解釋系統,

這種語義學具有結構化的特徵,語言中複合成分的語義是由其子成分的語義複合而成的,

結構操作語義,對軟體工程中結構化編程具有重要的指導意義。

1.2 指稱語義

人們用程序設計語言編程,計算機系統用於加工數據,

不同的計算機系統有不同的結構,因此對同一條命令的執行過程可能不同,但是最終結果應該是相同的。

指稱語義學認為語言成分的含義是語言成分本身固有的,與計算機系統無關,

所以,不應該將語言成分的執行過程看做它的語義,語言成分的語義應該是它的執行結果。

這種將最終結果看做語言成分語義的建模方式,稱為指稱語義學,這個最終結果稱為該語言成分的指稱。

語言成分的指稱一般是一個數學對象,如整數,集合等等。

指稱語義學是Christopher Strachey於1964年提出的,

後來Dana Scott創建了論域理論(domain theory)為指稱語義學奠定了數學基礎。

指稱語義學方法在定義語言的語義時,先確定語言成分的指稱,然後給出語言成分與其指稱之間的映射關係,

而且確定複合語言成分指稱的過程是語法制導的(syntax-directed),也稱為結構化的(structural),

即語言成分的指稱只依賴於它的子成分的指稱。

1.3 公理語義

公理語義在定義語義的時候,採用了數學中的公理化方法,

語言的公理語義構成了一個由「公理」和「定理」組成的邏輯證明系統,

它認為語言的語義,是由這個證明系統所能反映出來的一切性質。

操作語義可以看做公理語義的一種有向形式。

1967年,Robert W. Floyd提出了論證一個程序是否具有某種性質的數學方法,

1969年,Tony Hoare第一次用公理系統(Hoare logic)定義了一類程序設計語言的語義。

Hoare logic使用帶有前置條件和後置條件的歸納命題(inductive proposition),作為描述語義的形式化工具。

1.4 代數語義

指稱語義的研究方法建立在遞歸函數論基礎之上,公理語義的研究方法建立在謂詞邏輯基礎之上,

代數語義學用代數方法研究計算機語言的語義,它建立在抽象代數的基礎之上。

代數語義學描述了程序中不同種類(sort)的數學對象(object),以及這些對象之間的運算,它們構成了一種代數結構,

代數語義學,通過分析這種代數結構的性質,來描述程序的語義。

代數語義學源於人們對抽象數據類型(abstract data type)的研究,

泛代數(universal algebra)是一個用於研究抽象數據類型的數學框架。

在泛代數中,抽象數據類型的語法由代數項(algebraic term)描述,公理語義用項之間的等式集(a set of equations)描述,而指稱語義對應於一個Σ代數,操作語義通過給等式設定方向來表示。

2. Lisp的Pointer semantics

2.1 Conceptual pointer

Lisp語言提供了一個簡潔的計算模型,是因為它在語義上的簡潔性,

Lisp語言中所有的值都可以「看做」指針,所有的內存都可以「看做」在堆(heap)中分配。

(defvar foo 5)

Lisp會在堆中為x分配內存,讓它包含一個指針,指向另一塊初始化為5的內存,

即,Lisp中的值總是可以「看做」指向堆內存的指針。

我們可以用下圖表示:

+-------+ foo | *---+--->5 +-------+

Lisp語言的具體實現中,會採用不同的策略避免頻繁分配內存的開銷,

但是在語言層面對用戶是不可見的。

2.2 pointer semantics & value semantics

和C語言不同的是,Lisp用戶不用顯式的釋放內存,這使得心智負擔大大降低了,

Lisp用戶不用對指針解引用(dereference),因為默認每次都會這麼做。

例如,算術加法函數+,接受兩個指針作為參數,

它會在進行加法操作之前,自動對參數進行解引用,並且返回一個指向加法結果的指針。

(+ 1 2)

當我們對上述表達式求值的時候,加法函數會得到兩個指針,分別指向12

求值結果會返回一個指向3的指針。

大部分編程語言除了具有pointer semantics之外,還具有value semantics。

例如,它們會把12看做值,12的每次出現,都是不同的一份拷貝。

Lisp語言只有pointer semantics,12的每次出現都表示對唯一的數字對象的不同引用。

由於效率方面的考慮,具體實現可以做出任何調整,只要不影響pointer semantics。

人們常說Lisp,Smalltalk,Java等這些語言沒有指針,其實不太合理,

而是應該說,所有的東西都是指針。(pointer semantics

把所有東西都實現為一個指針,代價是高昂的,

我們必須把所有的指針,以及它指向的對象,全都分配在堆中。

還必須使用額外的操作訪問這些內存。

幸運的是,Lisp的具體實現中,並不會這樣表示它們,會對多種情況進行優化。

例如,變數中會直接保存數字的二進位形式,而不是一個指向堆內存的指針。

使用標籤(tag)與那些具有相同二進位模式的指針進行區分。

2.3 例子

在Lisp語言中,一個pair(又稱為cons cell),是一個在堆中分配的對象,

它包含兩個欄位,每個欄位都可以包含任意種類的值,

例如,數字,字元,布爾值,或者一個指向其他堆內存的指針。

由於歷史原因,第一個欄位稱為car,第二個欄位稱為cdr

pair可以通過cons函數來創建。

(cons 22 15)

以上表達式創建了一個pair,它包含了兩個欄位,

其中car欄位為22cdr欄位為15

我們可以用下圖來表示:

+-----------+ header| <PAIR-ID> | +===========+ car| *-----+----->22 +-----------+ cdr| *-----+----->15 +-----------+

其中,header用於保存類型信息,用於表明在堆中分配了什麼類型的對象,Lisp用戶不必關心header的值。

car欄位包含了一個指針,指向了22cdr欄位包含了另外一個指針,指向了15

(defvar foo (cons 22 15))

假設我們定義了一個全局變數,讓它的值為一個pair,於是我們可以用下圖來表示:

+---------+ +---------+ header| <PAIR> | foo | *----+------------->+=========+ +---------+ car| *----+---->22 +---------+ cdr| *----+---->15 +---------+

變數foo指向了一個pair,pair中的兩個欄位分別指向了2215

使用car函數和cdr函數可以得到pair中保存的兩個欄位的值,

(car foo)> 22(cdr foo)> 15


參考

形式語義學引論 - 周巢塵

程序設計語言理論基礎

Syntax and Semantics of Programming Languages

An Introduction to Scheme and its Implementation


下一篇:Emacs之魂(六):宏與元編程


推薦閱讀:

從C語言的函數傳參談指針
從C語言的數組參數退化為指針談起

TAG:語義 | Lisp | 指針 |