程序設(shè)計(jì)語(yǔ)言理論-文庫(kù)吧
2025-07-05 07:13 本頁(yè)面
【正文】 Press, 1998. – Glynn Winskel, The Formal Semantics of Programming Languages: An Introduction , MIT Press, 1993. 課 程 簡(jiǎn) 介 課程要求 – 講課進(jìn)展較快 ， 平時(shí)不復(fù)習(xí)不加深理解 ， 后面將聽(tīng)不懂 – 作業(yè)較多 ， 要求獨(dú)立完成 – 沒(méi)有上機(jī)實(shí)驗(yàn) – 考試開(kāi)卷 – 成績(jī)：考試成績(jī) 占 70%， 作業(yè)占 30% 第 1章 引 言 ? 介紹一個(gè)非常簡(jiǎn)單的、以自然數(shù)和布爾值作為基本類型的、基于類型化 ?演算的語(yǔ)言 ? 介紹該語(yǔ)言的語(yǔ)法、公理語(yǔ)義和操作語(yǔ)義 ? 主要議題如下： – ?表示法和 ?演算系統(tǒng)概述 – 類型和類型系統(tǒng)的扼要討論 – 基于表達(dá)式的歸納 、 基于證明的歸納和良基歸納 基 本 概 念 模型語(yǔ)言 ? 對(duì)程序設(shè)計(jì)語(yǔ)言進(jìn)行數(shù)學(xué)分析 – 從設(shè)計(jì)模型語(yǔ)言開(kāi)始 – 突出感興趣的程序構(gòu)造，忽略無(wú)關(guān)的細(xì)節(jié) ? 語(yǔ)言的形式化分為兩部分 – 能抓住語(yǔ)言本質(zhì)機(jī)制的非常小的核心： ?演算 – 導(dǎo)出部分：它們可以翻譯成核心的 ?演算 ? 用類型化 ?演算的框架來(lái)研究程序設(shè)計(jì)語(yǔ)言的各種概念 基 本 概 念 ?表示法 ? ?表示法的主要特征 – ?抽象： 用于定義函數(shù) – ?應(yīng)用： 將所定義的函數(shù)作用于變?cè)? ? ?抽象的例子 （ 自然數(shù)類型上的幾個(gè)例子 ） – 恒等函數(shù)： ?x : // 命令式表示 Id(x : nat) = x – 后繼函數(shù)： ?x : ? 1 // 函數(shù)式無(wú)需給函數(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)的并置來(lái)表示函數(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)寫 –
環(huán)評(píng)公示相關(guān)推薦
鄂ICP備17016276號(hào)-1