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

內(nèi)容概要

　　《程序設(shè)計(jì)語言理論（第2版）》給出分析程序設(shè)計(jì)語言語法性質(zhì)、操作性質(zhì)和語義性質(zhì)的一個(gè)框架，該框架基于λ演算系統(tǒng)。全書主要圍繞著一系列的λ演算來組織，該系列中λ演算的類型系統(tǒng)依次變得越來越復(fù)雜，這些λ演算用來分析和討論相應(yīng)的程序設(shè)計(jì)語言概念，如多態(tài)性、抽象數(shù)據(jù)類型、依賴類型、子定型等。以類型系統(tǒng)為中心對(duì)程序設(shè)計(jì)語言進(jìn)行的這種研究，在軟件工程、語言設(shè)計(jì)、高性能編譯器、高可信軟件和形式程序驗(yàn)證等方面有著重要應(yīng)用?！　　冻绦蛟O(shè)計(jì)語言理論（第2版）》可作為高等院校計(jì)算機(jī)科學(xué)及相關(guān)專業(yè)的研究生教材，也可供計(jì)算機(jī)軟件工程高級(jí)技術(shù)人員參考。

書籍目錄

第1章　引言1.1　基本概念1.1.1　程序設(shè)計(jì)語言的建模1.1.2　λ表示法1.1.3　符號(hào)和約定1.2　等式、歸約和語義1.2.1　公理語義1.2.2　操作語義1.2.3　指稱語義1.3　類型和類型系統(tǒng)1.3.1　類型和類型系統(tǒng)1.3.2　類型化語言的優(yōu)點(diǎn)1.4　歸納法1.4.1　表達(dá)式上的歸納1.4.2　證明上的歸納1.4.3　良基歸納習(xí)題第2章　泛代數(shù)和代數(shù)數(shù)據(jù)類型2.1　引言2.2　代數(shù)、基調(diào)和項(xiàng)2.2.1　代數(shù)2.2.2　代數(shù)項(xiàng)的語法2.2.3　代數(shù)以及項(xiàng)在代數(shù)中的解釋2.2.4　代換引理2.3　等式、可靠性和完備性2.3.1　等式2.3.2　項(xiàng)代數(shù)2.3.3　語義蘊(yùn)涵和等式證明系統(tǒng)2.3.4　完備性的形式2.3.5　同余、商和演繹完備性2.3.6　非空類別和最小模型完備性2.4　同態(tài)和初始性2.4.1　同態(tài)和同構(gòu)2.4.2　初始代數(shù)2.5　代數(shù)數(shù)據(jù)類型2.5.1　代數(shù)數(shù)據(jù)類型2.5.2　初始代數(shù)語義和數(shù)據(jù)類型歸納2.5.3　解釋沒有意義的項(xiàng)2.5.4　錯(cuò)誤值的其他解決方法2.6　重寫系統(tǒng)2.6.1　基本定義2.6.2　合流性和可證的相等性2.6.3　終止性2.6.4　臨界對(duì)2.6.5　左線性無重疊重寫系統(tǒng)2.6.6　局部合流、終止和合流之間的聯(lián)系2.6.7　代數(shù)數(shù)據(jù)類型的應(yīng)用習(xí)題第3章　簡(jiǎn)單類型化λ演算3.1　引言3.2　類型和項(xiàng)3.2.1　類型的語法3.2.2　上下文有關(guān)語法3.2.3　λ→項(xiàng)的語法3，2.4　帶積、和及其他類型的項(xiàng)3.2.5　定型算法3.3　證明系統(tǒng)3.3.1　等式和理論3.3.2　歸約規(guī)則3.3.3　有其他規(guī)則的歸約3.4　通用模型、可靠性和完備性3.4.1　通用模型和項(xiàng)的含義3.4.2　應(yīng)用結(jié)構(gòu)、外延性和框架3.4.3　環(huán)境條件3.4.4　類型可靠性和等式可靠性3.4.5　沒有空類型的完備性3.4.6　有空類型的完備性3.4.7　其他類型的通用模型3.5　可計(jì)算函數(shù)編程語言3.5.1　概述3.5.2　PCF的語法3.5.3　聲明和語法美化3.5.4　程序和結(jié)果3.5.5　公理語義3.5.6　操作語義3.5.7　由各種形式的語義定義的等價(jià)關(guān)系3.5.8　記錄和n元組3.6　各種歸約策略3.6.1　歸約策略3.6.2　最左歸約和惰性歸約3.6.3　并行歸約3.6.4　急切歸約習(xí)題第4章　類型化λ演算的模型4.1　引言4.2　遞歸函數(shù)和不動(dòng)點(diǎn)算子4.2.1　遞歸函數(shù)和不動(dòng)點(diǎn)算子4.2.2　有不動(dòng)點(diǎn)算子的急切歸約4.2.3　PCF語言的編程實(shí)例4.3　論域理論模型和不動(dòng)點(diǎn)4.3.1　遞歸定義和不動(dòng)點(diǎn)算子4.3.2　完全偏序集合、提升和笛卡兒積4.3.3　連續(xù)函數(shù)4.3.4　不動(dòng)點(diǎn)和完備連續(xù)層級(jí)4.3.5　PCF的CPO模型4.4　不動(dòng)點(diǎn)歸納習(xí)題第5章　命令式程序的語義5.1　引言5.2　Kernel語言5.2.1　存儲(chǔ)單元5.2.2　表達(dá)式的解釋5.2.3　程序狀態(tài)5.3　操作語義5.3.1　表達(dá)式的求值5.3.2　命令的執(zhí)行5.4　指稱語義5.4.1　帶狀態(tài)的類型化λ演算5.4.2　語義函數(shù)5.4.3　操作語義和指稱語義的等價(jià)5.5　Kernel語言的Hoare邏輯5.5.1　一階斷言5.5.2　證明規(guī)則5.5.3　可靠性5.5.4　小結(jié)習(xí)題第6章　遞歸類型6.1　引言6.2　歸納和余歸納6.2.1　余歸納現(xiàn)象6.2.2　歸納和余歸納指南6.2.3　代數(shù)和余代數(shù)6.3　遞歸類型6.3.1　遞歸類型總覽6.3.2　遞歸的數(shù)據(jù)結(jié)構(gòu)6.4　歸納類型和余歸納類型6.4.1　歸納類型和余歸納類型總覽6.4.2　幫助理解的實(shí)例習(xí)題第7章　多態(tài)性7.1　引言7.1.1　概述7.1.2　類型作為函數(shù)變?cè)?.2　直謂式多態(tài)演算7.2.1　類型和項(xiàng)的語法7.2.2　和其他形式多態(tài)性的比較7.2.3　等式證明和歸約7.2.4　ML風(fēng)格的多態(tài)聲明7.3　非直謂式多態(tài)演算7.3.1　引言7.3.2　非直謂式多態(tài)λ演算的表達(dá)力7.3.3　歸約的終止性7.4　數(shù)據(jù)抽象和存在類型7.5　類型表達(dá)式的分類7.5.1　類型表達(dá)式的種類7.5.2　類型表達(dá)式的定類與相等7.5.3　項(xiàng)的定型習(xí)題第8章　依賴類型8.1　引言8.2　帶依賴類型的演算8.2.1　依賴積類型8.2.2　依賴和類型8.3　帶依賴類型的程序設(shè)計(jì)8.3.1　簡(jiǎn)化DML的實(shí)例8.3.2　簡(jiǎn)化DML的定義8.4　廣義積與廣義和8.4.1　廣義積與廣義和概念8.4.2　帶廣義積與廣義和的直謂式演算8.4.3　ML模塊語言8.4.4　用積與和來表示模塊8.4.5　直謂性以及兩個(gè)全域之間的聯(lián)系習(xí)題第9章　命題和類型9.1　引言9.2　構(gòu)造邏輯9.2.1　構(gòu)造語義9.2.2　構(gòu)造邏輯9.2.3　命題當(dāng)作類型9.3　經(jīng)典邏輯9.3.1　經(jīng)典邏輯和構(gòu)造邏輯的區(qū)別與聯(lián)系9.3.2　經(jīng)典邏輯的規(guī)則9.3.3　推導(dǎo)消去形式9.3.4　證明的動(dòng)態(tài)性習(xí)題第10章　子定型10.1　引言10.2　有子定型的簡(jiǎn)單類型化λ演算10.3　記錄10.3.1　記錄子定型的一般性質(zhì)10.3.2　帶記錄和子定型的類型化演算10.4　子定型的語義模型10.4.1　概述10.4.2　子定型的轉(zhuǎn)換解釋10.4.3　類型的子集解釋10.5　對(duì)象的遞歸記錄模型10.5.1　遞歸記錄類型10.5.2　遞歸類型的子定型習(xí)題第11章　類型推斷11.1　引言11.2　帶類型變量的λ→類型推斷11.2.1　語言λt→11.2.2　代換、實(shí)例與合一11.2.3　主定型算法11.2.4　隱式定型11.2.5　定型和合一的等價(jià)11.3　帶多態(tài)聲明的類型推斷11.3.1　ML類型推斷和多態(tài)變量11.3.2　兩組隱式定型規(guī)則11.3.3　類型推斷算法習(xí)題參考文獻(xiàn)

圖書封面

圖書標(biāo)簽Tags

無

評(píng)論、評(píng)分、閱讀與下載

---

    程序設(shè)計(jì)語言理論 PDF格式下載

---