程序設(shè)計(jì)語言理論-01

1、程序設(shè)計(jì)語言理論計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院陳意云，3607043 /yiyun 課 程 簡 介計(jì)算機(jī)科學(xué)的理論體系1、模型理論 關(guān)心的問題 給定模型 M，哪些問題可以由模型 M解決 如何比較模型的表達(dá)能力 經(jīng)典計(jì)算 確定的圖靈機(jī)，可計(jì)算性理論屬于模型理論 新型計(jì)算 本質(zhì)特點(diǎn)是交互( 并發(fā)、分布、網(wǎng)絡(luò)、網(wǎng)格、云 ) 計(jì)算和交互的統(tǒng)一模型理論尚未出現(xiàn)課 程 簡 介計(jì)算機(jī)科學(xué)的理論體系2、程序理論 關(guān)心的問題 給定模型 M，如何用模型 M解決問題 包括的領(lǐng)域 程序設(shè)計(jì)范型、程序設(shè)計(jì)語言、程序設(shè)計(jì)、形式語義、類型論、程序驗(yàn)證、程序

2、分析等課 程 簡 介計(jì)算機(jī)科學(xué)的理論體系3、計(jì)算理論 關(guān)心的問題 給定模型 M和一類問題，解決該類問題需要多少資源 包括的領(lǐng)域 計(jì)算復(fù)雜性理論課 程 簡 介圍繞程序設(shè)計(jì)語言的研究（課程涉及內(nèi)容用綠色表示） 語法：形式語言和自動(dòng)機(jī)理論，語法分析的實(shí)現(xiàn)技術(shù) 語義：公理語義、操作語義、指稱語義形式描述技術(shù)還有：代數(shù)規(guī)范、范疇論、屬性文法 程序設(shè)計(jì)的范型：命令式語言、函數(shù)式語言、邏輯程序設(shè)計(jì)語言、面向?qū)ο蟪绦蛟O(shè)計(jì)語言、并行程序設(shè)計(jì)語言課 程 簡 介圍繞程序設(shè)計(jì)語言的研究（課程涉及內(nèi)容用綠色表示） 類型論與類型系統(tǒng)：多態(tài)類型、子類型、存在類型 程序驗(yàn)證：程序正確性證明 程序分析技術(shù)：數(shù)據(jù)流分析、控制流分

3、析、模型檢查、抽象解釋 程序的自動(dòng)生成技術(shù)：程序變換課 程 簡 介學(xué)習(xí)的意義 掌握與程序設(shè)計(jì)語言有關(guān)的理論，為從事有關(guān)的研究起一個(gè)奠基的作用應(yīng)用： 程序設(shè)計(jì)語言的設(shè)計(jì)和實(shí)現(xiàn) 程序的自動(dòng)生成 程序分析與程序驗(yàn)證 提高軟件的可信程度 協(xié)議的形式描述和驗(yàn)證課 程 簡 介教材和參考書 陳意云、張昱，程序設(shè)計(jì)語言理論（第二版），高等教育出版社，2010.2 教學(xué)資源網(wǎng)頁：/yiyun 馬世龍、眭躍飛等譯，類型和程序設(shè)計(jì)語言，電子工業(yè)出版社，2005.5 許滿武譯，程序設(shè)計(jì)語言理論基礎(chǔ)，電子工業(yè)出版社，2006.11 陳意云、張昱，編譯原理（第二版），高等教育

4、出版社，2008.6課 程 簡 介教材和參考書 John C. Mitchell, Foundations For ProgrammingLanguages, MIT Press, 1996. Banjamin C. Pierce, Types and ProgrammingLaungages, MIT Press, 2002. Robert Harper, Practical Foundations forProgramming Languages, working draft, 2009. John C. Reynolds, Theories of ProgrammingLanguages

5、 , Cambridge University Press, 1998. Glynn Winskel, The Formal Semantics ofProgramming Languages: An Introduction , MIT Press, 1993.課 程 簡 介課程要求 講課進(jìn)展較快，平時(shí)不復(fù)習(xí)不加深理解，后面將聽不懂 作業(yè)較多，要求獨(dú)立完成 沒有上機(jī)實(shí)驗(yàn) 考試開卷 成績：考試成績占70%，作業(yè)占30%第1章引言 介紹一個(gè)非常簡單的、以自然數(shù)和布爾值作為基本類型的、基于類型化演算的語言 介紹該語言的語法、公理語義和操作語義 主要議題如下： 表示法和演算系統(tǒng)概述 類型和類型系統(tǒng)的

6、扼要討論 基于表達(dá)式的歸納、基于證明的歸納和良基歸納1.1 基 本 概 念1.1.1 模型語言 對程序設(shè)計(jì)語言進(jìn)行數(shù)學(xué)分析 從設(shè)計(jì)模型語言開始 突出感興趣的程序構(gòu)造，忽略無關(guān)的細(xì)節(jié) 語言的形式化分為兩部分 能抓住語言本質(zhì)機(jī)制的非常小的核心：演算 導(dǎo)出部分：它們可以翻譯成核心的演算 用類型化演算的框架來研究程序設(shè)計(jì)語言的各種概念1.1 基 本 概 念1.1.2 表示法 表示法的主要特征 抽象：用于定義函數(shù) 應(yīng)用：將所定義的函數(shù)作用于變元 抽象的例子 （自然數(shù)類型上的幾個(gè)例子） 恒等函數(shù)：x : nat. x / 命令式表示 Id( x : nat) = x 后繼函數(shù)：x : nat. x + 1

7、 / 函數(shù)式無需給函數(shù)命名 常函數(shù)：x : nat.10 x : nat. x + true 不是良形的表達(dá)式 表示法寫出的表達(dá)式叫做表達(dá)式或項(xiàng)1.1 基 本 概 念 項(xiàng) x: . M 和謂詞演算公式 x : A. 的比較 是一個(gè)約束算子 x是一個(gè)占位符，約束變元，可以重新命名約束變元而不改變表達(dá)式的含義 在x: . x + y中， x的出現(xiàn)是約束的， y的出現(xiàn)是自由的 不含自由變元的表達(dá)式稱為閉表達(dá)式 應(yīng)用：用項(xiàng)的并置來表示函數(shù)應(yīng)用，例： (x : nat. x) 5 (x : nat. x) 5 = 5/ 應(yīng)用后面介紹的 公理1.1 基 本 概 念 一個(gè)簡單的例子( x : nat. (

8、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 基 本 概 念 表示法中有兩個(gè)約定 函數(shù)應(yīng)用是左結(jié)合的： MNP 應(yīng)看成 ( MN) P 每個(gè)的約束范圍盡可能地大：一直到表達(dá)式的結(jié)束，或碰到不能配對的右括號(hào)為止 例 x: . MN解釋為x: .( MN)，而不是(x: . M) N x: . y: . MN是x: .( y: .( MN)的簡寫 (x: .(y: .(z: .

9、 M) N) P) Q可以簡寫為( x: .y: .z: . M) NPQ1.2 等式、歸約和語義 表示法是演算的一部分，演算是關(guān)于表達(dá)式的一個(gè)推理系統(tǒng) 除了語法外，該形式系統(tǒng)有三個(gè)主要部分 公理語義：推導(dǎo)表達(dá)式相等的一個(gè)形式系統(tǒng) 操作語義：基于單方向的等式推理（歸約、符號(hào)計(jì)算）上述兩者都稱為證明系統(tǒng) 指稱語義：形式系統(tǒng)的模型1.2 等式、歸約和語義1.2.1 公理語義一個(gè)等式公理系統(tǒng) 約束變元改名公理（公理） x: . M = y: .y/xM， M中無自由出現(xiàn)的 y其中 N/ xM表示 M中的 x用表達(dá)式 N代換的結(jié)果 例如 x:.x = y:.y 函數(shù)應(yīng)用公理（ 公理） (x: . M)

10、 N = N/ x M 例如 ( x: nat. x+4) 4 = 4/ x( x+4) = 4 + 41.2 等式、歸約和語義 自反公理、對稱性規(guī)則、傳遞性規(guī)則 同余規(guī)則 相等的函數(shù)應(yīng)用于相等的變元產(chǎn)生相等的結(jié)果M1 = M2 N1= N2M1 N1 = M2N2 等式證明規(guī)則允許推導(dǎo)任何一組等式前提的邏輯推論1.2 等式、歸約和語義1.2.2 操作語義語言的操作語義可用不同的方式給出 定義一個(gè)抽象機(jī),通過一系列的機(jī)器狀態(tài)變換來計(jì)算程序 演繹出最終結(jié)果的證明系統(tǒng) 前面所列的等式公理的單向形式給出了歸約規(guī)則 最核心的歸約規(guī)則是( )的單向形式( x: . M) N N/ x M 通常沒有 歸約

11、規(guī)則：x: . M y: . y/ xM1.2 等式、歸約和語義1.2.3 指稱語義 確定語言構(gòu)造（程序、語句、表達(dá)式等）到指稱物（各種集合）的語義映射，滿足： 各種語言構(gòu)造的實(shí)例都有對應(yīng)的指稱物 復(fù)合構(gòu)造的指稱只依賴于它的子構(gòu)造的指稱 類型化演算的指稱語義 每個(gè)類型表達(dá)式對應(yīng)到一個(gè)集合 類型 的項(xiàng)解釋為其值集上的一個(gè)元素 類型 的值集是函數(shù)集合，項(xiàng) x: . M解釋為一個(gè)數(shù)學(xué)函數(shù)1.3 類型和類型系統(tǒng) 類型論 為避免集合論悖論而建立起來的數(shù)學(xué)理論 主要研究集合的分層、分類方法 在程序設(shè)計(jì)語言理論中，類型論是指類型系統(tǒng)的設(shè)計(jì)、分析和研究 類型提供了所有可能值的一種劃分 一個(gè)類型是一群有某些公共

12、性質(zhì)的值 對于不同的類型系統(tǒng)，類型的多少和值所屬的類型可能不同1.3 類型和類型系統(tǒng)1.3.1 類型和類型系統(tǒng) 類型語言：變量都被給定類型 未類型化的語言：不限制變量值的范圍 類型系統(tǒng) 語言的一個(gè)組成部分 由一組定型規(guī)則構(gòu)成 類型系統(tǒng)的研究有兩個(gè)分支 類型系統(tǒng)在程序設(shè)計(jì)語言中的應(yīng)用 “純類型化演算”和各種邏輯之間的對應(yīng)關(guān)系1.3 類型和類型系統(tǒng)設(shè)計(jì)類型系統(tǒng)的目的 用來證明程序不會(huì)出現(xiàn)不良行為 類型可靠的語言（安全語言） 所有程序運(yùn)行時(shí)都沒有不良行為出現(xiàn) 類型系統(tǒng)的研究也需要形式化的方法 許多語言定義被發(fā)現(xiàn)不是類型可靠的，甚至經(jīng)過類型檢查后接受的程序也會(huì)崩潰 顯式類型化的語言：類型是語法的一部分

13、 隱式類型化的語言1.3 類型和類型系統(tǒng)1.3.2 類型語言的優(yōu)點(diǎn) 開發(fā)時(shí)的實(shí)惠 可以較早發(fā)現(xiàn)錯(cuò)誤 類型信息具有文檔作用（比程序注解精確，比形式規(guī)范容易理解） 編譯時(shí)的實(shí)惠 程序模塊可以相互獨(dú)立地編譯 運(yùn)行時(shí)的實(shí)惠 更有效的空間安排和訪問方式，提高了目標(biāo)代碼的運(yùn)行效率1.3 類型和類型系統(tǒng)類型系統(tǒng)的其他應(yīng)用 許多程序分析工具使用類型檢查或類型推斷算法 類型系統(tǒng)用來表示邏輯命題和證明1.4 歸 納 法本節(jié)介紹本書常用的歸納法 自然數(shù)歸納法（有兩種形式，不專門介紹） 結(jié)構(gòu)歸納（介紹表達(dá)式上的歸納，有兩種形式） 證明上的歸納 良基歸納法（重點(diǎn)介紹）1.4 歸 納 法1.4.1 表達(dá)式上的歸納 表達(dá)式

14、文法 e := 0 | 1 | v | e + e | e e 每個(gè)表達(dá)式都有各自的語法樹 如果 P是表達(dá)式的性質(zhì)， Q是自然數(shù)的性質(zhì) Q( n) 語言樹 t.如果 height( t) = n 并且 t是 e的語法樹，那么 P( e)為真 首先必須為高度是0的語法樹直接證明 P 然后，對于語法樹高度至少為1的表達(dá)式 e，假定對于語法樹高度較小的表達(dá)式， P都為真，證明P( e)為真1.4 歸 納 法 結(jié)構(gòu)歸納（形式1） 對每個(gè)原子表達(dá)式 e，證明 P( e) 對直接子表達(dá)式為 e1, ek的任何復(fù)合表達(dá)式 e，證明，如果 P( ei)（ i=1, k）都為真，那么 P( e) 也為真 結(jié)構(gòu)歸

15、納（形式2） 證明：對任何表達(dá)式 e，如果 P( e)對 e的任何子表達(dá)式 e都成立，那么 P( e)也成立 形式2的歸納假設(shè)包含了所有的子表達(dá)式，并非只是直接子表達(dá)式1.4 歸 納 法1.4.2 證明上的歸納 證明系統(tǒng)由公理和推理規(guī)則組成 證明是一個(gè)公式序列，該序列中的每個(gè)公式都是公理或者是由前面的公式通過一個(gè)推理規(guī)則得到的結(jié)論 基于證明的長度，用自然數(shù)歸納法來討論證明的性質(zhì) 另一種觀點(diǎn)把證明看成是某種形式的樹1.4 歸 納 法A1- - -AnB證明樹示意圖 證明上的結(jié)構(gòu)歸納 對該證明系統(tǒng)中的每個(gè)公理，證明 P成立 假定對證明 1, , k， P成立，證明 P( )也為真 是這樣的證明，它

16、結(jié)束于用一個(gè)推理規(guī)則，并且是從證明 1, , k延伸出來的一個(gè)證明1.4 歸 納 法1.4.3 良基歸納 集合 A的二元關(guān)系被稱為是良基的p：若 A上不存在無窮遞減序列 a0 f a1 f a2 f 例：在自然數(shù)上，如果 j = i +1，則 i p j。這個(gè)關(guān)系是良基關(guān)系 良基關(guān)系的一些特點(diǎn) 良基關(guān)系不一定有傳遞性 良基關(guān)系都是非自反的，即對任何 a A， a p a不成立；否則會(huì)出現(xiàn)無窮遞減序列 af a f a f 1.4 歸 納 法 引理1.1 若p是集合 A上的二元關(guān)系，p是良基的，當(dāng)且僅當(dāng) A的每個(gè)非空子集都有極小元 證明 假定p是良基的，證明非空子集 B( BA)有極小元用反證法

17、。如果 B無極小元，那么對每個(gè) a B，可以找到某個(gè) a B使得 apa。則可以從任意的a0 B開始，構(gòu)造一個(gè)無窮遞減序列 a0 f a1 f a2 f 假定每個(gè)子集都有極小元?jiǎng)t不可能存在 a0 f a1 f a2 f ，因該序列給出了無極小元的集合 a0, a1, a2, 。故p是良基的1.4 歸 納 法 命題1.2（良基歸納）令p是集合 A上的良基關(guān)系，令 P是 A上某個(gè)性質(zhì)，若每當(dāng)所有的 P( b) ( b p a)為真，則 P( a)為真，即a.( b.( b p a P( b) P( a)那么，對所有的 a A， P( a)為真1.4 歸 納 法 命題1.2（良基歸納）若 a.( b

18、.( b p a P( b) P( a)，則 a. P( a) 證明 若存在某個(gè) xA使得 P( x)成立，則下面集合非空B = aA | P( a) 由引理1.1， B一定有極小元 aB 但是，對所有的 b p a， P( b)一定成立（否則 a不是B的極小元） 這就和假定 b.( b p a P( b) P( a)矛盾1.4 歸 納 法 良基歸納法的使用如何理解：若每當(dāng)所有的 P( b) ( b p a)為真，則 P( a)為真，即： ( b.( b p a P( b) P( a) 對某些 a，不存在 b，使得 b p a，則 b.( b p a P( b) P( a) 等價(jià)于 P( a)（因?yàn)?b: . P( b)為真，其中表示空集） 對另一些 a，存在 b，使得 b p a，則 b.( b p a P( b) P( a)的證明是基于 b.( b p a P( b) 為真來推導(dǎo) P( a)為真1.4 歸 納 法表1.1常用歸納形式的良基關(guān)系歸納形式良基關(guān)系自然數(shù)歸納(1)m p n，如果 m +1 = n自然數(shù)歸納(2)mp ，如果mnn結(jié)構(gòu)歸納(1)ep ，如果 是 的直接子表達(dá)式eee結(jié)構(gòu)歸納(2)e p e，如果 e是 e的子表達(dá)式基