《程序设计语言原理》课程教学资源（PPT课件讲稿）形式语义学 Formal Semantics

本PPT参考了金英老师的课程内容 形式语义学 Forma semantics 2021/2/5

2021/2/5 1 形式语义学 Formal Semantics 本PPT参考了金英老师的课程内容

语义定义 语义定义:赋予每个合法的程序一个明确的意义 语义定义的基本方法,是基于语言的语法结构: 定义语言中的基本元素的意义 定义语言中各种语法结构的意义 algol60修订报告中用BNF定义语言的语法,采用自然语言的说明和实例的 方式,非形式地定义 Algol60的语义。 Backus在讨论Algo60时说:现在我们已经有办法严格定义语言的语法了, 希望今后不久就能严格定义语言的语义。 至今的语言手册一直沿用这种方式 语义远比语法复杂,至今还没有开发出一种完美、功能充分强大、容易理解 容易使用的语义定义方式,可很好地用于定义一切语言中一切结构的语义 但是,对程序语义的研究已经得到许多成果

2021/2/5 2

操作语义学 执 代数语义学 代数 程序设计语言 逻辑 形式语义 模型 关系 公理语义学 功能 指称语义学 函数式描述方法 理论基础 2021/2/5

2021/2/5 3 代数语义学 理论基础 函数式描述方法 程序设计语言 形式语义 指称语义学 操作语义学 公理语义学 代数 功能执行 逻辑 模型 关系

匚程序设计语言丁 语义形式化 语法化编 译 原理 程序设计语言 形式语义 基 础论 离散数学 2021/2/5

2021/2/5 4 离散数学 程序设计语言 形式语义 编 译 原 理 程序设计语言 理 论 基 础 语义形式化 语法形式化

程序设计语言理解 Formal Method 抽象能力 程序设计语言 形式语义 程序设计方法 Formal Ⅴ erification 软件开发方法 Formal specification 2021/2/5

2021/2/5 5 软件开发方法 程序设计语言 形式语义 程 序 设 计 方 法 程序设计语言理解 抽 象 能 力 Formal Method Formal Specification Formal Verification

前言:“形式语义学”概述 o What? 形式语义学:给出对(形式)语言及其程序采 用形式系统方法进行语义定义的方法。 分类:从不同的角度研究程序的含义 操作语义学(执行) 指称语义学(功能) 公理语义学(逻辑) 代数语义学(代数,抽象数据结构) 其他 2021/2/5

2021/2/5 6 前言：“形式语义学”概述 ⚫ What？ –形式语义学：给出对(形式)语言及其程序采 用形式系统方法进行语义定义的方法。 ⚫ 分类：从不同的角度研究程序的含义 – 操作语义学（执行） – 指称语义学（功能） – 公理语义学（逻辑） – 代数语义学（代数，抽象数据结构） – 其他

Lambda演算 2021/2/5

2021/2/5 7 Lambda演算

关于 Lambda演算 久表达式 自由变量(计算一个λ表达式的自由变量 集合) 替换(计算) 变换规则(三种变换) 归约 ●范式(性质及其计算) 2021/2/5

2021/2/5 8 关于Lambda演算 ⚫ 表达式 ⚫ 自由变量（计算一个表达式的自由变量 集合） ⚫ 替换（计算） ⚫ 变换规则 （三种变换） ⚫ 归约 ⚫ 范式（性质及其计算）

关于 Lambda演算 入表达式 个表达式由变量名、抽象符号λ,以及括号等符 号构成,其语法为: := λ () 2021/2/5

2021/2/5 9 关于Lambda演算 ⚫ 表达式 一个表达式由变量名、抽象符号，.以及括号等符 号构成， 其语法为： ::= | |  . | ( )

关于 Lambda演算 变换规则(三种变换) α变换:设E是表达式,x是变量,则称下面变换为变换 (其中y不在FV(AxE)中) 入xE-2-)xyyx]E β变换:设xE)和E0为表达式,则称下面变换为变换 (称β变换规则的左部表达式为β基) (xEEO EEO/X ●η变换:假设入x,Mx是一个表达式,且满足条件xgFV(M 则称下面变换为变换: (x Mx)n M 2021/2/5

2021/2/5 10 关于Lambda演算 ⚫ 变换规则 （三种变换） ⚫ 变换：设E是表达式，x是变量，则称下面变换为α变换 （其中y不在 FV( x.E )中） x.E ------〉 y.[y/x] E ⚫ 变换：设(x.E)和E0为表达式，则称下面变换为β变换 （称β变换规则的左部表达式为β基） (x.E)E0 E[E0/x] ⚫ 变换：假设x.Mx是一个表达式，且满足条件xFV(M)， 则称下面变换为η变换: (x.M x) M   