前言:“形式语义学”概述 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是一个表达式，且满足条件xFV(M)， 则称下面变换为η变换: (x.M x) M