课程简介 计算机科学的理论体系 1、模型理论 ●关心的问题 -给定模型M, 哪些问题可以由模型M解决 -如何比较模型的表达能力 ·经典计算 确定的图灵机，可计算性理论属于模型理论 ·新型计算 本质特点是交互（并发、分布、网络、网格、云） ·计算和交互的统一模型理论尚未出现
课 程 简 介 计算机科学的理论体系 1、模型理论 • 关心的问题 – 给定模型M，哪些问题可以由模型M解决 – 如何比较模型的表达能力 • 经典计算 – 确定的图灵机，可计算性理论属于模型理论 • 新型计算 – 本质特点是交互( 并发、分布、网络、网格、云 ) • 计算和交互的统一模型理论尚未出现
课程简介 计算机科学的理论体系 2、程序理论 ·关心的问题 -给定模型M, 如何用模型M解决问题 ●包括的领域 一程序设计范型、程序设计语言、程序设计、形式 语义、类型论、程序验证、程序分析等
课 程 简 介 计算机科学的理论体系 2、程序理论 • 关心的问题 – 给定模型M，如何用模型M解决问题 • 包括的领域 – 程序设计范型、程序设计语言、程序设计、形式 语义、类型论、程序验证、程序分析等
课程简介 计算机科学的理论体系 3、计算理论 ·关心的问题 给定模型M和一类问题，解决该类问题需要多少 资源 ·包括的领域 一计算复杂性理论
课 程 简 介 计算机科学的理论体系 3、计算理论 • 关心的问题 – 给定模型M和一类问题，解决该类问题需要多少 资源 • 包括的领域 – 计算复杂性理论
课程简介 围绕程序设计语言的研究（课程涉及内容用 绿色表示) 语法：形式语言和自动机理论， 语法分析的实现 技术 语义：公理语义、操作语义、指称语义 形式描述技术还有：代数规范、范畴论、属性 文法 程序设计的范型：命令式语言、函数式语言、逻 辑程序设计语言、面向对象程序设计语言、并行 程序设计语言
课 程 简 介 围绕程序设计语言的研究（课程涉及内容用 绿色表示） – 语法：形式语言和自动机理论，语法分析的实现 技术 – 语义：公理语义、操作语义、指称语义 形式描述技术还有：代数规范、范畴论、属性 文法 – 程序设计的范型：命令式语言、函数式语言、逻 辑程序设计语言、面向对象程序设计语言、并行 程序设计语言
课程简介 围绕程序设计语言的研究（课程涉及内容用 绿色表示) 类型论与类型系统：多态类型、子类型、存在类 型 程序验证：程序正确性证明 程序分析技术：数据流分析、控制流分析、模型 检查、抽象解释 程序的自动生成技术：程序变换
课 程 简 介 围绕程序设计语言的研究（课程涉及内容用 绿色表示） – 类型论与类型系统：多态类型、子类型、存在类 型 – 程序验证：程序正确性证明 – 程序分析技术：数据流分析、控制流分析、模型 检查、抽象解释 – 程序的自动生成技术：程序变换
课程简介 学习的意义 掌握与程序设计语言有关的理论，为从事有关的 研究起一个奠基的作用 应用： 一程序设计语言的设计和实现 -程序的自动生成 程序分析与程序验证 -提高软件的可信程度 协议的形式描述和验证
课 程 简 介 学习的意义 – 掌握与程序设计语言有关的理论，为从事有关的 研究起一个奠基的作用 应用： – 程序设计语言的设计和实现 – 程序的自动生成 – 程序分析与程序验证 – 提高软件的可信程度 – 协议的形式描述和验证
第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 // 应用后面介绍的公理