程序設(shè)計(jì)語言理論-展示頁
2024-08-04 07:13本頁面
【正文】 開卷 – 成績(jī)：考試成績(jī) 占 70%， 作業(yè)占 30% 第 1章 引 言 ? 介紹一個(gè)非常簡(jiǎn)單的、以自然數(shù)和布爾值作為基本類型的、基于類型化 ?演算的語言 ? 介紹該語言的語法、公理語義和操作語義 ? 主要議題如下： – ?表示法和 ?演算系統(tǒng)概述 – 類型和類型系統(tǒng)的扼要討論 – 基于表達(dá)式的歸納 、 基于證明的歸納和良基歸納 基 本 概 念 模型語言 ? 對(duì)程序設(shè)計(jì)語言進(jìn)行數(shù)學(xué)分析 – 從設(shè)計(jì)模型語言開始 – 突出感興趣的程序構(gòu)造，忽略無關(guān)的細(xì)節(jié) ? 語言的形式化分為兩部分 – 能抓住語言本質(zhì)機(jī)制的非常小的核心： ?演算 – 導(dǎo)出部分：它們可以翻譯成核心的 ?演算 ? 用類型化 ?演算的框架來研究程序設(shè)計(jì)語言的各種概念 基 本 概 念 ?表示法 ? ?表示法的主要特征 – ?抽象： 用于定義函數(shù) – ?應(yīng)用： 將所定義的函數(shù)作用于變?cè)? ? ?抽象的例子 （ 自然數(shù)類型上的幾個(gè)例子 ） – 恒等函數(shù)： ?x : // 命令式表示 Id(x : nat) = x – 后繼函數(shù)： ?x : ? 1 // 函數(shù)式無需給函數(shù)命名 – 常函數(shù)： ?x : – ?x : ? true 不是良形的表達(dá)式 ? ?表示法寫出的表達(dá)式叫做 ?表達(dá)式 或 ?項(xiàng) 基 本 概 念 ? ?項(xiàng) ?x:?.M 和謂詞演算公式 ?x :A.? 的比較 – ?是一個(gè)約束算子 – x是一個(gè)占位符 ，約束變?cè)?以重新命名 ?約束變?cè)?而不改變表達(dá)式的含義 – 在 ?x:?.x + y中， x的出現(xiàn)是 約束的， y的出現(xiàn)是自由的 – 不含自由變?cè)谋磉_(dá)式稱為閉表達(dá)式 ? ?應(yīng)用： 用項(xiàng)的并置來表示函數(shù)應(yīng)用，例： – (?x : ) 5 – (?x : ) 5 ? 5 // 應(yīng)用后面介紹的 ?公理 基 本 概 念 ? 一個(gè)簡(jiǎn)單的例子 ( ?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 = 12 基 本 概 念 ? ?表示法中有兩個(gè)約定 – 函數(shù)應(yīng)用是左結(jié)合的： MNP 應(yīng)看成 (MN)P – 每個(gè) ?的約束范圍盡可能地大 ： 一直到表達(dá)式的結(jié)束，或 碰到不能配對(duì)的右括號(hào)為止 ? 例 – ?x:?.MN解釋為 ?x:?.(MN)， 而不是 (?x:?.M)N – ?x:?.?y:?.MN是 ?x:?.(?y:?.(MN))的簡(jiǎn)寫 – (((?x:?.(?y:?.(?z:?.M)))N)P)Q可以簡(jiǎn)寫為 (?x:?.?y:?.?z:?.M)NPQ 等式、歸約和語義 ? ?表示法是 ?演算 的一部分， ?演算是關(guān)于 ?表達(dá)式的一個(gè)推理系統(tǒng) ? 除了語法外，該形式系統(tǒng)有三個(gè)主要部分 – 公理語義： 推導(dǎo)表達(dá)式相等的一個(gè)形式系統(tǒng) – 操作語義： 基于單方向的等式推理 （歸約、符號(hào)計(jì)算） 上述兩者都稱為證明
環(huán)評(píng)公示相關(guān)推薦
鄂ICP備17016276號(hào)-1