程序設計語言理論

1、程序設計語言理論程序設計語言理論計算機科學與技術學院計算機科學與技術學院陳意云，陳意云，3607043http:/ 程程 簡簡 介介計算機科學的理論體系計算機科學的理論體系1、模型理論、模型理論 關心的問題關心的問題 給定模型給定模型M，哪些問題可以由模型，哪些問題可以由模型M解決解決 如何比較模型的表達能力如何比較模型的表達能力 經(jīng)典計算經(jīng)典計算 確定的圖靈機，可計算性理論屬于模型理論確定的圖靈機，可計算性理論屬于模型理論 新型計算新型計算 本質特點是交互本質特點是交互( 并發(fā)、分布、網(wǎng)絡、網(wǎng)格、云并發(fā)、分布、網(wǎng)絡、網(wǎng)格、云 ) 計算和交互的統(tǒng)一模型理論尚未出現(xiàn)計算和交互的統(tǒng)一模型理論尚未出

2、現(xiàn)課課 程程 簡簡 介介計算機科學的理論體系計算機科學的理論體系2、程序理論、程序理論 關心的問題關心的問題 給定模型給定模型M，如何用模型，如何用模型M解決問題解決問題 包括的領域包括的領域 程序設計范型、程序設計語言、程序設計、形式程序設計范型、程序設計語言、程序設計、形式語義、類型論、程序驗證、程序分析等語義、類型論、程序驗證、程序分析等課課 程程 簡簡 介介計算機科學的理論體系計算機科學的理論體系3、計算理論、計算理論 關心的問題關心的問題 給定模型給定模型M和一類問題，解決該類問題需要多少和一類問題，解決該類問題需要多少資源資源 包括的領域包括的領域 計算復雜性理論計算復雜性理論課課

3、 程程 簡簡 介介圍繞程序設計語言的研究（課程涉及內容用圍繞程序設計語言的研究（課程涉及內容用綠色綠色表示）表示） 語法：形式語言和自動機理論，語法分析的實現(xiàn)語法：形式語言和自動機理論，語法分析的實現(xiàn)技術技術 語義：語義：公理語義、操作語義、指稱語義公理語義、操作語義、指稱語義 形式描述技術還有：形式描述技術還有：代數(shù)規(guī)范代數(shù)規(guī)范、范疇論范疇論、屬性、屬性文法文法 程序設計的范型程序設計的范型：命令式語言、函數(shù)式語言命令式語言、函數(shù)式語言、邏、邏輯程序設計語言、輯程序設計語言、面向對象程序設計語言面向對象程序設計語言、并行、并行程序設計語言程序設計語言課課 程程 簡簡 介介圍繞程序設計語言的研

4、究（課程涉及內容用圍繞程序設計語言的研究（課程涉及內容用綠色綠色表示）表示） 類型論與類型系統(tǒng)：多態(tài)類型、子類型、存在類類型論與類型系統(tǒng)：多態(tài)類型、子類型、存在類型型 程序驗證：程序驗證：程序正確性證明程序正確性證明 程序分析技術：數(shù)據(jù)流分析、控制流分析、模型程序分析技術：數(shù)據(jù)流分析、控制流分析、模型檢查、抽象解釋檢查、抽象解釋 程序的自動生成技術：程序變換程序的自動生成技術：程序變換課課 程程 簡簡 介介學習的意義學習的意義 掌握與程序設計語言有關的理論，為從事有關的掌握與程序設計語言有關的理論，為從事有關的研究起一個奠基的作用研究起一個奠基的作用應用：應用： 程序設計語言的設計和實現(xiàn)程序設

5、計語言的設計和實現(xiàn) 程序的自動生成程序的自動生成 程序分析與程序驗證程序分析與程序驗證 提高軟件的可信程度提高軟件的可信程度 協(xié)議的形式描述和驗證協(xié)議的形式描述和驗證課課 程程 簡簡 介介教材和參考書教材和參考書 陳意云、張昱，程序設計語言理論（第二版），陳意云、張昱，程序設計語言理論（第二版），高等教育出版社，高等教育出版社，2010.2 教學資源網(wǎng)頁：教學資源網(wǎng)頁：http:/ 馬世龍、眭躍飛等譯，類型和程序設計語言，電馬世龍、眭躍飛等譯，類型和程序設計語言，電子工業(yè)出版社，子工業(yè)出版社，2005.5 許滿武譯，程序設計語言理論基礎，電子工業(yè)出許滿武譯，程序設計語言理論基礎，電子工業(yè)出版社

6、，版社，2006.11 陳意云、張昱，編譯原理（第二版），高等教育陳意云、張昱，編譯原理（第二版），高等教育出版社，出版社，2008.6課課 程程 簡簡 介介教材和參考書教材和參考書 John C. Mitchell, Foundations For Programming Languages, MIT Press, 1996. Banjamin C. Pierce, Types and Programming Laungages, MIT Press, 2002. Robert Harper, Practical Foundations for Programming Languages,

7、working draft, 2009. John C. Reynolds, Theories of Programming Languages , Cambridge University Press, 1998. Glynn Winskel, The Formal Semantics of Programming Languages: An Introduction , MIT Press, 1993. 課課 程程 簡簡 介介課程要求課程要求 講課進展較快，平時不復習不加深理解，后面將講課進展較快，平時不復習不加深理解，后面將聽不懂聽不懂 作業(yè)較多，要求獨立完成作業(yè)較多，要求獨立完成 沒有

8、上機實驗沒有上機實驗 考試開卷考試開卷 成績：考試成績成績：考試成績占占70%，作業(yè)占，作業(yè)占30% 第第1章章 引引 言言 介紹一個非常簡單的、以自然數(shù)和布爾值作介紹一個非常簡單的、以自然數(shù)和布爾值作為基本類型的、基于類型化為基本類型的、基于類型化 演算的語言演算的語言 介紹該語言的語法、公理語義和操作語義介紹該語言的語法、公理語義和操作語義 主要議題如下：主要議題如下： 表示法和表示法和 演算系統(tǒng)概述演算系統(tǒng)概述 類型和類型系統(tǒng)的扼要討論類型和類型系統(tǒng)的扼要討論 基于表達式的歸納、基于證明的歸納和良基歸納基于表達式的歸納、基于證明的歸納和良基歸納1.1 基基 本本 概概 念念1.1.1 模

9、型語言模型語言 對程序設計語言進行數(shù)學分析對程序設計語言進行數(shù)學分析 從設計模型語言開始從設計模型語言開始 突出感興趣的程序構造，忽略無關的細節(jié)突出感興趣的程序構造，忽略無關的細節(jié) 語言的形式化分為兩部分語言的形式化分為兩部分 能抓住語言本質機制的非常小的核心：能抓住語言本質機制的非常小的核心： 演算演算 導出部分：它們可以翻譯成核心的導出部分：它們可以翻譯成核心的 演算演算 用類型化用類型化 演算的框架來研究程序設計語言的演算的框架來研究程序設計語言的各種概念各種概念1.1 基基 本本 概概 念念1.1.2 表示法表示法 表示法的主要特征表示法的主要特征 抽象：抽象：用于定義函數(shù)用于定義函數(shù)

10、 應用：應用：將所定義的函數(shù)作用于變元將所定義的函數(shù)作用于變元 抽象的例子抽象的例子 （自然數(shù)類型上的幾個例子自然數(shù)類型上的幾個例子） 恒等函數(shù)：恒等函數(shù)： x : nat.x / 命令式表示命令式表示Id(x : nat) = x 后繼函數(shù)：后繼函數(shù)： x : nat.x 1 / 函數(shù)式無需給函數(shù)命名函數(shù)式無需給函數(shù)命名 常函數(shù)：常函數(shù)： x : nat.10 x : nat. .x true 不是良形的表達式不是良形的表達式 表示法寫出的表達式叫做表示法寫出的表達式叫做 表達式表達式或或 項項1.1 基基 本本 概概 念念 項項 x: . .M 和謂詞演算公式和謂詞演算公式 x :A. .

11、 的比較的比較 是一個約束算子是一個約束算子 x是一個占位符是一個占位符，約束變元，可，約束變元，可以重新命名以重新命名 約束約束變元變元而不改變表達式的含義而不改變表達式的含義 在在 x: . .x + y中，中，x的出現(xiàn)是的出現(xiàn)是約束的，約束的， y的出現(xiàn)是的出現(xiàn)是自由的自由的 不含自由變元的表達式稱為閉表達式不含自由變元的表達式稱為閉表達式 應用：應用：用項的并置來表示函數(shù)應用，例：用項的并置來表示函數(shù)應用，例： ( x : nat. .x) 5 ( x : nat. .x) 5 5 / 應用后面介紹的應用后面介紹的 公理公理1.1 基基 本本 概概 念念 一個簡單的例子一個簡單的例子

12、( x : nat. ( y : nat. z : nat. ( x + y ) + z ) 3 ) 4 5= ( x : nat. z : nat. ( x + 3 ) + z ) 4 5= ( z : nat. ( 4 + 3 ) + z ) 5= ( 4 + 3 ) + 5= 121.1 基基 本本 概概 念念 表示法中有兩個約定表示法中有兩個約定 函數(shù)應用是左結合的：函數(shù)應用是左結合的： MNP 應看成應看成 (MN)P 每個每個 的約束范圍盡可能地大的約束范圍盡可能地大：一直到表達式的結束，或一直到表達式的結束，或碰到不能配對的右括號為止碰到不能配對的右括號為止 例例 x: . .M

13、N解釋為解釋為 x: . .(MN)，而不是而不是( x: . .M)N x: . . y: . .MN是是 x: . .( y: . .(MN)的簡寫的簡寫 ( x: . .( y: . .( z: . .M)N)P)Q可以簡寫為可以簡寫為( x: . . y: . . z: . .M)NPQ 1.2 等式、歸約和語義等式、歸約和語義 表示法是表示法是 演算演算的一部分，的一部分， 演算是關于演算是關于 表表達式的一個推理系統(tǒng)達式的一個推理系統(tǒng) 除了語法外，該形式系統(tǒng)有三個主要部分除了語法外，該形式系統(tǒng)有三個主要部分 公理語義：公理語義：推導表達式相等的一個形式系統(tǒng)推導表達式相等的一個形式系

14、統(tǒng) 操作語義：操作語義：基于單方向的等式推理基于單方向的等式推理（歸約、符號（歸約、符號計算）計算）上述兩者都稱為證明系統(tǒng)上述兩者都稱為證明系統(tǒng) 指稱語義：形式系統(tǒng)的模型指稱語義：形式系統(tǒng)的模型1.2 等式、歸約和語義等式、歸約和語義1.2.1 公理語義公理語義一個等式公理系統(tǒng)一個等式公理系統(tǒng) 約束變元改名公理約束變元改名公理（ 公理公理） x: . .M y: . . y x M，M中無自由出現(xiàn)的中無自由出現(xiàn)的y其中其中 N x M表示表示M中的中的x用表達式用表達式N代換的結果代換的結果 例如例如 x: .x y: .y 函數(shù)應用公理函數(shù)應用公理（ 公理公理） ( x: . .M)N N/

15、xM 例如例如 ( x:nat.x+4) 4 4/x(x+4) 4 + 41.2 等式、歸約和語義等式、歸約和語義 自反公理、對稱性規(guī)則、傳遞性規(guī)則自反公理、對稱性規(guī)則、傳遞性規(guī)則 同余規(guī)則同余規(guī)則 相等的函數(shù)應用于相等的變元產(chǎn)生相等的結果相等的函數(shù)應用于相等的變元產(chǎn)生相等的結果 等式證明規(guī)則允許推導任何一組等式前提的等式證明規(guī)則允許推導任何一組等式前提的邏輯推論邏輯推論M1 = M2 N1 = N2 M1 N1 = M2 N21.2 等式、歸約和語義等式、歸約和語義1.2.2 操作語義操作語義語言的操作語義可用不同的方式給出語言的操作語義可用不同的方式給出 定義一個抽象機定義一個抽象機, ,

16、通過一系列的機器狀態(tài)變換通過一系列的機器狀態(tài)變換來計算程序來計算程序 演繹出最終結果的證明系統(tǒng)演繹出最終結果的證明系統(tǒng) 前面所列的等式公理的單向形式給出了歸約規(guī)則前面所列的等式公理的單向形式給出了歸約規(guī)則 最核心的歸約規(guī)則是最核心的歸約規(guī)則是( )的單向形式的單向形式( x: .M)N N/xM 通常沒有通常沒有 歸約規(guī)則：歸約規(guī)則： x: .M y: . y x M1.2 等式、歸約和語義等式、歸約和語義1.2.3 指稱語義指稱語義 確定語言構造（程序、語句、表達式等）到確定語言構造（程序、語句、表達式等）到指稱物（各種集合）的語義映射，滿足：指稱物（各種集合）的語義映射，滿足： 各種語言構

17、造的實例都有對應的指稱物各種語言構造的實例都有對應的指稱物 復合構造的指稱只依賴于它的子構造的指稱復合構造的指稱只依賴于它的子構造的指稱 類型化類型化 演算的指稱語義演算的指稱語義 每個類型表達式對應到一個集合每個類型表達式對應到一個集合 類型類型 的項解釋為其值集上的一個元素的項解釋為其值集上的一個元素 類型類型 的值集是函數(shù)集合，項的值集是函數(shù)集合，項 x: .M解釋為解釋為一個數(shù)學函數(shù)一個數(shù)學函數(shù)1.3 類型和類型系統(tǒng)類型和類型系統(tǒng) 類型論類型論 為避免集合論悖論而建立起來的數(shù)學理論為避免集合論悖論而建立起來的數(shù)學理論 主要研究集合的分層、分類方法主要研究集合的分層、分類方法 在程序設計

18、語言理論中，類型論是指類型系統(tǒng)的在程序設計語言理論中，類型論是指類型系統(tǒng)的設計、分析和研究設計、分析和研究 類型提供了所有可能值的一種劃分類型提供了所有可能值的一種劃分 一個類型是一群有某些公共性質的值一個類型是一群有某些公共性質的值 對于不同的類型系統(tǒng)，類型的多少和值所屬對于不同的類型系統(tǒng)，類型的多少和值所屬的類型可能不同的類型可能不同1.3 類型和類型系統(tǒng)類型和類型系統(tǒng)1.3.1 類型和類型系統(tǒng)類型和類型系統(tǒng) 類型語言類型語言：變量都被給定類型：變量都被給定類型 未未類類型化的型化的語語言言：不限制變量值的范圍：不限制變量值的范圍 類型系統(tǒng)類型系統(tǒng) 語言的一個組成部分語言的一個組成部分 由

19、一組定型規(guī)則構成由一組定型規(guī)則構成 類型系統(tǒng)的研究有兩個分支類型系統(tǒng)的研究有兩個分支 類型系統(tǒng)在程序設計語言中的應用類型系統(tǒng)在程序設計語言中的應用 “純類型化純類型化 演算演算”和各種邏輯之間的對應關系和各種邏輯之間的對應關系1.3 類型和類型系統(tǒng)類型和類型系統(tǒng)設計類型系統(tǒng)的目的設計類型系統(tǒng)的目的 用來證明程序不會出現(xiàn)不良行為用來證明程序不會出現(xiàn)不良行為 類型可靠的語言（安全語言）類型可靠的語言（安全語言） 所有程序運行時都沒有不良行為出現(xiàn)所有程序運行時都沒有不良行為出現(xiàn) 類型系統(tǒng)的研究也需要形式化的方法類型系統(tǒng)的研究也需要形式化的方法 許多語言定義被發(fā)現(xiàn)不是類型可靠的，甚至經(jīng)過許多語言定義被

20、發(fā)現(xiàn)不是類型可靠的，甚至經(jīng)過類型檢查后接受的程序也會崩潰類型檢查后接受的程序也會崩潰 顯式類型化的語言：顯式類型化的語言：類型是語法的一部分類型是語法的一部分 隱式類型化的語言隱式類型化的語言1.3 類型和類型系統(tǒng)類型和類型系統(tǒng)1.3.2 類型語言的優(yōu)點類型語言的優(yōu)點 開發(fā)時的實惠開發(fā)時的實惠 可以較早發(fā)現(xiàn)錯誤可以較早發(fā)現(xiàn)錯誤 類型信息具有文檔作用（比程序注解精確，比形類型信息具有文檔作用（比程序注解精確，比形式規(guī)范容易理解）式規(guī)范容易理解） 編譯時的實惠編譯時的實惠 程序模塊可以相互獨立地編譯程序模塊可以相互獨立地編譯 運行時的實惠運行時的實惠 更有效的空間安排和訪問方式，提高了目標代碼更有

21、效的空間安排和訪問方式，提高了目標代碼的運行效率的運行效率1.3 類型和類型系統(tǒng)類型和類型系統(tǒng)類型系統(tǒng)的其他應用類型系統(tǒng)的其他應用 許多程序分析工具使用類型檢查或類型推斷許多程序分析工具使用類型檢查或類型推斷算法算法 類型系統(tǒng)用來表示邏輯命題和證明類型系統(tǒng)用來表示邏輯命題和證明1.4 歸歸 納納 法法本節(jié)介紹本書常用的歸納法本節(jié)介紹本書常用的歸納法 自然數(shù)歸納法（有兩種形式，不專門介紹）自然數(shù)歸納法（有兩種形式，不專門介紹） 結構歸納（介紹表達式上的歸納，有兩種形結構歸納（介紹表達式上的歸納，有兩種形式）式） 證明上的歸納證明上的歸納 良基歸納法（重點介紹）良基歸納法（重點介紹）1.4 歸歸

22、納納 法法1.4.1 表達式上的歸納表達式上的歸納 表達式文法表達式文法 e := 0 | 1 | v | e + e | e e 每個表達式都有各自的語法樹每個表達式都有各自的語法樹 如果如果P是表達式的性質，是表達式的性質，Q是是自然數(shù)的性質自然數(shù)的性質 Q(n) 語言語言樹樹t. .如果如果height(t) = n 并且并且t是是e的的語法樹，那么語法樹，那么P(e)為真為真 首先必須為高度是首先必須為高度是0的語法樹直接證明的語法樹直接證明P 然后，對于語法樹高度至少為然后，對于語法樹高度至少為1的表達式的表達式e，假定，假定對于語法樹高度較小的表達式，對于語法樹高度較小的表達式，P

23、都為真，證明都為真，證明P(e)為真為真1.4 歸歸 納納 法法 結構歸納結構歸納（形式（形式1） 對每個原子表達式對每個原子表達式e，證明證明P(e) 對直接子表達式為對直接子表達式為e1, ek的任何復合表達式的任何復合表達式e，證明，如果證明，如果P(ei)（i=1, k）都為真，那么都為真，那么P(e) 也為真也為真 結構歸納結構歸納（形式（形式2） 證明：對任何表達式證明：對任何表達式e，如果如果P(e )對對e的任何子表的任何子表達式達式e 都成立，那么都成立，那么P(e)也成立也成立 形式形式2的歸納假設包含了所有的子表達式，并的歸納假設包含了所有的子表達式，并非只是直接子表達式

24、非只是直接子表達式1.4 歸歸 納納 法法1.4.2 證明上的歸納證明上的歸納 證明系統(tǒng)證明系統(tǒng)由公理和推理規(guī)則組成由公理和推理規(guī)則組成 證明是一個公式序列，該序列中的每個公式證明是一個公式序列，該序列中的每個公式都是公理或者是由前面的公式通過一個推理都是公理或者是由前面的公式通過一個推理規(guī)則得到的結論規(guī)則得到的結論 基于證明的長度，用自然數(shù)歸納法來討論證基于證明的長度，用自然數(shù)歸納法來討論證明的性質明的性質 另一種觀點把證明看成是某種形式的樹另一種觀點把證明看成是某種形式的樹1.4 歸歸 納納 法法 證明上的結構歸納證明上的結構歸納 對該證明系統(tǒng)中的每個公理，證明對該證明系統(tǒng)中的每個公理，證

25、明P成立成立 假定對證明假定對證明 1, , k，P成立，證明成立，證明P( )也為真也為真 是這樣的證明，它結束于用一個推理規(guī)則，并是這樣的證明，它結束于用一個推理規(guī)則，并且是從證明且是從證明 1, , k延伸出來的一個證明延伸出來的一個證明BAn- - -A1證明樹示意圖證明樹示意圖1.4 歸歸 納納 法法1.4.3 良基歸納良基歸納 集合集合A的二元關系被稱為是良基的的二元關系被稱為是良基的 ：若：若A上上不存在無窮遞減序列不存在無窮遞減序列a0 a1 a2 例：在自然數(shù)上，如果例：在自然數(shù)上，如果j i +1，則則i j。這個。這個關系是良基關系關系是良基關系 良基關系的一些特點良基關

26、系的一些特點 良基關系不一定有傳遞性良基關系不一定有傳遞性 良基關系都是非自反的，即對任何良基關系都是非自反的，即對任何a A，a a不不成立；否則會出現(xiàn)無窮遞減序列成立；否則會出現(xiàn)無窮遞減序列a a a 1.4 歸歸 納納 法法 引理引理1.1 若若 是集合是集合A上的二元關系，上的二元關系， 是良基是良基的，的，當且僅當當且僅當A的每個非空子集都有極小元的每個非空子集都有極小元 證明證明 假定假定 是良基的，是良基的，證明非空子集證明非空子集B(B A)有極小元有極小元 用反證法。如果用反證法。如果B無極小元，那么對每個無極小元，那么對每個a B，可以找到某個可以找到某個aB使得使得a a

27、。則可以從任意的則可以從任意的a0 B開始，構造一個無窮遞減序列開始，構造一個無窮遞減序列a0 a1 a2 假定每個子集都有極小元假定每個子集都有極小元 則不可能存在則不可能存在a0 a1 a2 ，因該序列給出了因該序列給出了無極小元的集合無極小元的集合a0, a1, a2, 。故。故 是良基的是良基的1.4 歸歸 納納 法法 命題命題1.2（良基歸納）（良基歸納）令令 是集合是集合A上的良基關系，上的良基關系，令令P是是A上某個性質，上某個性質，若每當所有的若每當所有的P(b) (b a)為真，則為真，則P(a)為真，即為真，即 a.( b.(b a P(b) P(a)那么，對所有的那么，對所有的a A，P(a)為真為真1.4 歸歸 納納 法法 命題命題1.2（良基歸納）（良基歸納）若若 a.( b.(b a P(b) P(a)，則，則 a.P(a) 證明證明 若存在某個若存在某個x A使得使得 P(x)成立，則下面集合非空成立，則下面集合非空B a A | P(a) 由引理由引理1.1，B一定有極小元一定有極小元a B 但是，對所有的但是，對所有的b a，P(b)一定成立（否則一定成立（否則a不是