程序設(shè)計(jì)語言理論(文件)
【正文】 ： 一直到表達(dá)式的結(jié)束，或 碰到不能配對(duì)的右括號(hào)為止 ? 例 – ?x:?.MN解釋為 ?x:?.(MN)， 而不是 (?x:?.M)N – ?x:?.?y:?.MN是 ?x:?.(?y:?.(MN))的簡寫 – (((?x:?.(?y:?.(?z:?.M)))N)P)Q可以簡寫為 (?x:?.?y:?.?z:?.M)NPQ 等式、歸約和語義 ? ?表示法是 ?演算 的一部分， ?演算是關(guān)于 ?表達(dá)式的一個(gè)推理系統(tǒng) ? 除了語法外，該形式系統(tǒng)有三個(gè)主要部分 – 公理語義： 推導(dǎo)表達(dá)式相等的一個(gè)形式系統(tǒng) – 操作語義： 基于單方向的等式推理 （歸約、符號(hào)計(jì)算） 上述兩者都稱為證明系統(tǒng) – 指稱語義：形式系統(tǒng)的模型 等式、歸約和語義 公理語義 一個(gè)等式公理系統(tǒng) ? 約束變元改名公理 （ ?公理 ） – ?x:?.M ? ?y:?.?y?x?M， M中無自由出現(xiàn)的 y 其中 ?N?x?M表示 M中的 x用表達(dá)式 N代換的結(jié)果 – 例如 ?x:?.x ? ?y:?.y ? 函數(shù)應(yīng)用公理 （ ?公理 ） – (?x:?.M)N ? [N/x]M – 例如 (?x:+4) 4 ? [4/x](x+4) ? 4 + 4 等式、歸約和語義 ? 自反公理、對(duì)稱性規(guī)則、傳遞性規(guī)則 ? 同余規(guī)則 – 相等的函數(shù)應(yīng)用于相等的變元產(chǎn)生相等的結(jié)果 ? 等式證明規(guī)則允許推導(dǎo)任何一組等式前提的邏輯推論 M1 = M2 N1 = N2 M1 N1 = M2 N2 等式、歸約和語義 操作語義 語言的操作語義可用不同的方式給出 ? 定義一個(gè)抽象機(jī) ,通過一系列的機(jī)器狀態(tài)變換來計(jì)算程序 ? 演繹出最終結(jié)果的證明系統(tǒng) – 前面所列的等式公理的單向形式給出了歸約規(guī)則 – 最核心的歸約規(guī)則是 (?)的單向形式 (?x:?.M)N ?? [N/x]M – 通常沒有 ? 歸約規(guī)則： ?x:?.M ?? ?y:?.?y?x?M 等式、歸約和語義 指稱語義 ? 確定語言構(gòu)造 （ 程序 、 語句 、 表達(dá)式等 ） 到指稱物 （ 各種集合 ） 的語義映射 ， 滿足： – 各種語言構(gòu)造的實(shí)例都有對(duì)應(yīng)的指稱物 – 復(fù)合構(gòu)造的指稱只依賴于它的子構(gòu)造的指稱 ? 類型化 ?演算的指稱語義 – 每個(gè)類型表達(dá)式對(duì)應(yīng)到一個(gè)集合 – 類型 ? 的項(xiàng)解釋為其值集上的一個(gè)元素 – 類型 ? ? ? 的值集是函數(shù)集合，項(xiàng) ?x:?.M解釋為一個(gè)數(shù)學(xué)函數(shù) 類型和類型系統(tǒng) ? 類型論 – 為避免集合論悖論而建立起來的數(shù)學(xué)理論 – 主要研究集合的分層、分類方法 – 在程序設(shè)計(jì)語言理論中，類型論是指類型系統(tǒng)的設(shè)計(jì)、分析和研究 ? 類型提供了所有可能值的一種劃分 – 一個(gè)類型是一群有某些公共性質(zhì)的值 ? 對(duì)于不同的類型系統(tǒng)，類型的多少和值所屬的類型可能不同 類型和類型系統(tǒng) 類型和類型系統(tǒng) ? 類型語言 ：變量都被給定類型 ? 未 類 型化的 語 言 ：不限制變量值的范圍 ? 類型系統(tǒng) – 語言的一個(gè)組成部分 – 由一組定型規(guī)則構(gòu)成 ? 類型系統(tǒng)的研究有兩個(gè)分支 – 類型系統(tǒng)在程序設(shè)計(jì)語言中的應(yīng)用 – “純類型化 ?演算”和各種邏輯之
環(huán)評(píng)公示相關(guān)推薦
鄂ICP備17016276號(hào)-1