中国科学技术大学：《程序设计语言理论》课程教学资源（PPT课件讲稿）第1章 引言（主讲：陈意云）

课程简介 学习的意义 掌握与程序设计语言有关的理论，为从事有关的 研究起一个奠基的作用 应用： 一程序设计语言的设计和实现 -程序的自动生成 程序分析与程序验证 -提高软件的可信程度 协议的形式描述和验证

课 程 简 介 学习的意义 – 掌握与程序设计语言有关的理论，为从事有关的 研究起一个奠基的作用 应用： – 程序设计语言的设计和实现 – 程序的自动生成 – 程序分析与程序验证 – 提高软件的可信程度 – 协议的形式描述和验证

第1章引言 ·介绍一个非常简单的、以自然数和布尔值作 为基本类型的、基于类型化λ演算的语言 介绍该语言的语法、公理语义和操作语义 主要议题如下： -λ表示法和λ演算系统概述 类型和类型系统的扼要讨论 -基于表达式的归纳、基于证明的归纳和良基归纳

第1章 引 言 • 介绍一个非常简单的、以自然数和布尔值作 为基本类型的、基于类型化演算的语言 • 介绍该语言的语法、公理语义和操作语义 • 主要议题如下： – 表示法和演算系统概述 – 类型和类型系统的扼要讨论 – 基于表达式的归纳、基于证明的归纳和良基归纳

1.1基本概念 1.1.1模型语言 对程序设计语言进行数学分析 从设计模型语言开始 一突出感兴趣的程序构造，忽略无关的细节 语言的形式化分为两部分 能抓住语言本质机制的非常小的核心：入演算 一导出部分：它们可以翻译成核心的演算 用类型化入演算的框架来研究程序设计语言的 各种概念

1.1 基 本 概 念 1.1.1 模型语言 • 对程序设计语言进行数学分析 – 从设计模型语言开始 – 突出感兴趣的程序构造，忽略无关的细节 • 语言的形式化分为两部分 – 能抓住语言本质机制的非常小的核心：演算 – 导出部分：它们可以翻译成核心的演算 • 用类型化演算的框架来研究程序设计语言的 各种概念

1.1基本概念 1.1.2入表示法 ·入表示法的主要特征 -入抽象：用于定义函数 -应用：将所定义的函数作用于变元 入抽象的例子（自然数类型上的几个例子） -恒等函数：x:nat.x /命令式表示Idx:nat)=x 后继函数：入x:natx+1∥函数式无需给函数命名 - 常函数：入x:nat.10 入x:nat.x+true不是良形的表达式 ·入表示法写出的表达式叫做入表达式或入项

1.1 基 本 概 念 1.1.2 表示法 • 表示法的主要特征 – 抽象：用于定义函数 – 应用：将所定义的函数作用于变元 • 抽象的例子（自然数类型上的几个例子） – 恒等函数：x : nat.x // 命令式表示Id(x : nat) = x – 后继函数：x : nat.x + 1 // 函数式无需给函数命名 – 常函数：x : nat.10 – x : nat.x + true 不是良形的表达式 • 表示法写出的表达式叫做表达式或项

1.1基本概念 入项x:o.M和谓词演算公式Vx:A.的比较 -入是一个约束算子 -x是一个占位符，约束变元， 可以重新命名入约束 变元而不改变表达式的含义 在入x:o.x+y中，x的出现是约束的，y的出现是 自由的 一不含自由变元的表达式称为闭表达式 入应用：用项的并置来表示函数应用，例： -(久x:nat.x)5 -(2x:nat.x)5=5 /应用后面介绍的B公理

1.1 基 本 概 念 • 项x:.M 和谓词演算公式x :A. 的比较 – 是一个约束算子 – x是一个占位符，约束变元，可以重新命名约束 变元而不改变表达式的含义 – 在x:.x + y中，x的出现是约束的， y的出现是 自由的 – 不含自由变元的表达式称为闭表达式 • 应用：用项的并置来表示函数应用，例： – (x : nat.x) 5 – (x : nat.x) 5 = 5 // 应用后面介绍的公理