基本介紹
- 中文名：指稱語義學
- 外文名：denotational semantics
- 性質：形式語義學的一個分支
- 對象：傳統的數學對象
簡介,定義,套用,歷史情況,基本方法,指稱語義映象D可定義如下：,[ 指稱語義綜合產生程式結構的意義 ],
簡介
定義
指稱語義學 （denotational semantics）
套用
歷史情況
指稱語義學的主要思想是英國牛津大學C.斯特拉切於1964年前後提出的。美國D.斯高特創建的論域理論為指稱語義學奠定了數學基礎。論域理論是討論各種語言成分指稱物的數學結構，以及提供在這種數學結構上定義語言成分的語義和推導語言成分特性所必需的數學工具。。。。
1976年英國一些學者發展了論域理論，提出冪論域理論，從而為定義非決定性程式的指稱語義奠定了理論基礎。
基本方法
1976年英國一些學者發展了論域理論，提出冪論域理論，從而為定義非確定性程式的指稱語義奠定了理論基礎。指稱語義方法定義語言的語義基本思想是：先確定指稱物，然後給出語言成分至指稱物的語義映象。這個映象要求滿足：
(1)每個成分都對應有指稱物；
(2)複合成分的指稱只依賴於它的子成分的指稱。。
算術表達式的效果就是根據程式變數當前值計算表達式的值。程式變數的當前值可以用一個數值向量來表示。如果有k個程式變數,,…,，則k維數值向量(,,…,)表示的值為,的值為,…，的值為。程式變數的一種取值稱為程式的一個狀態。狀態的全體集合稱為狀態空間，記作State。算術表達式的值的範圍記作Num。算術表達式的指稱物就是State至Num的一個映象，也就是根據State中的任意一個元素(即程式變數的一組取值)可求得Num中對應的一個元素(即表達式在變數的這組取值下的值)。數學中的映象只反映集合間元素的對應，用映象作為語言成分的指稱物在語義的定義中就避免了涉及語言成分的執行過程。State至Num的全體映象，即全體表達式的指稱物，記作State→Num。不同表達式的指稱物是不同的，對算術表達式的語義下定義，就是要對每個算術表達式至其指稱物的一個對應下定義，故也可表示為一種映象。。
E∷=n|x|e+e|e×e|…
指稱語義映象D可定義如下：
第一個公式表示，無論程式處於何種狀態S，常量n的值不變，為數學中相應的量n。為了區分元語言和程式設計語言，指稱語義定義中將程式設計語言中的成分用[ |及| ]及括起來。第二個公式表示，變數在狀態S時的值為數值向量S的第i個分量。
第三、四個公式表示，表達式(+)和×在狀態S時的值分別為子表達式和在狀態S時的值的和與積。
表達式的抽象語法規定如何用最簡單的表達式常量和變數構成其他表達式。而表達式的語義定義也是先給出最簡單的表達式的語義，然後按照語法的構造過程去定義其他表達式的語義，使得複合成分的語義由各成分語義複合而成。這種定義語義的方法叫作結構式方法，或叫語法引導方法。指稱語義學就是一種結構式形式語義學。執行程式設計語言中的語句導致程式狀態的改變(即程式變數取值的改變)，故語句的指稱物應是State至State的映象：State→State。定義語句的語義就相當於定義映象D：
這表示順序執行語句和，即先執行，並將執行後形成的新狀態，作為當前狀態再執行。
實際的程式設計語言非常複雜，所定義的語義映象比之上文列舉的遠為複雜。為了允許同名變數在不同過程體中表示的值不同，指稱語義中引進環境的概念；為了刻畫程式控制的轉移又引進後續的概念，這些概念在描述和簡化語義定義中有重要的作用。
[ 指稱語義綜合產生程式結構的意義 ]
術語 " 指稱的 "(denotational) 來自其同根的動詞 " 指示 "(denote ) 。在指稱方法 中語言的結構指稱 ( 或者說表示 ) 了有關的意義 , 而這種意義通常是一些函式。表達式 a +b的意義就是一個從環境到值的函式 。
一個指稱語義由兩部分組成 :
1)
域 , 有些像類型。它們標識出與一個語言相關的語法和語義對象。對前綴表達式語言而言 , 語義對象就是值和環境 ; 語法對象則是表達式、變數、常量以及運算符等。
2)
語義規則 , 從結構成分的語義綜合產生出該結構的語義。。。
在指稱語義方面奠基性的貢獻是有關域和語義規則的嚴格的數學基礎。。
我們現在就來設計有關 let 表達式的語義規則。
表達式 E 的語義 , 記作[|E|], 是一個從環境到值的函式（一般來說 , 相對一個結構可以存在多種與之關聯的意義。如表達式有類型 , 也可以有值。草草 的前面加一個類似 vaI 或 type 的標記 , 就可以標識出該結構的各種不同語義類別 , 例如 var [|E|]，type[|E|] 等等）。函式套用的方式就是將函式的參數寫在函式右邊。進而令 f a b 等價於 (fa)b,f a 在b 上的套用。因此 , 表達式 E 在環境 env下的值為
[|E|] env
在這種記述方式下 , 變數 x 在環境 env 里的值就是
[|x|] env =lookup(x env) 這個規則可以讀作 : “ 將表達式的 x 的意義 ( 作為函式 ) 套用於環境 env, 我們將得到值 lookup(x,env) 。”
有關求和、乘積的語義規則為
[| plus E1 E2 |] env=[| E1|] env+[| E2|] env
[|times E1 E2|] env=[| E1|] env*[| E2|] env
在這兩種情形下 , 表達式和它的子表達式使用的都是同一個環境。
在有關 1et 表達式的規則里 , 應該注意的是 , 表達式 El 用的是環境 env, 而表達式 E2則使用一個修改過的環境 ( 不同於 env):
[|let x=E1 in E2|] env=[|E2|] bind (x,[|E1|]env,env)
一個let表達式在環境 env 里的值就是其子表達式在一個新環境裡的值 , 新環境中將 x 約束到表達式E1環境env里的值 [|E1|]env。。
