形式语义学-Lambda演算

《形式语义学-Lambda演算》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、形式语义学FormalSemanticsofProgrammingLanguages2011.09第二章函数式抽象描述方法2.1论域理论基础2.2Lambda演算2.3函数式抽象语言2.4函数式抽象语言的应用2021/7/162第二章函数式抽象描述方法2.2Lambda演算(calculus)2.2.1Lambda演算介绍2.2.2Lambda演算作为计算模型2.2.3Lambda演算系统的扩充2021/7/163引言欧美等大学大都将函数式语言作为第一门程序设计语言函数式语言与过程式语言的区别强调值的概念：有什么类型就有

2、什么值，高阶值；运算的并行性：运算分量，函数实参表达式都可并行计算；引用透明性：计算的延迟性：支持模式和模式匹配；函数式语言具有比命令式语言更高的数学抽象力，因此在描述某些算法的时候更精炼和严格；2021/7/164引言函数式语言不仅可用于程序设计，还可用于算法、编译器、解释器的抽象描述，以及指称语义的定义等方面。本课程将分两个部分介绍函数式语言无类型的函数式语言–Lambda演算(calculus)有类型的函数式语言–类似ML,通用描述方法2021/7/165引言首先在1941年由Church作为一个可计算模型的精确定义

3、给出的；语法简单而又有强大的描述能力；已被证明其描述能力等价于图灵机；可以描述任何一个部分递归函数的计算过程；是指称语义描述语言和函数式语言的理论基础；LISP语言就是基于Lambda演算(JohnMcCarthy)设计的。2021/7/1662.2Lambda演算主要内容2.2.1Lambda演算介绍表达式自由变量freevariables(FV)替换substitution变换规则conversionrules归约reduction2.2.2Lambda演算作为计算模型2.2.3Lambda演算系统的扩充2021/7/

4、1672.2.1Lambda演算介绍Lambda演算可看作是一个简单的语义清楚的形式语言；可以用来解释复杂的程序设计语言或者计算模型；Lambda演算通常包括两个部分：合法表达式(表达式)的形式系统(语法)变换规则的形式系统(语义)2021/7/1682021/7/169表达式(1)—定义一个表达式由变量名、抽象符号，.以及(,)等符号构成，其语法为：<表达式>::=<变量名>

5、<表达式><表达式>

6、<变量名>.<表达式>

7、(<表达式>)没有类型；没有常量；变量名不仅可以代表变量，还可以代表函数；2021

8、/7/1610表达式(2)施用型和抽象型施用型表达式(APPLY):E1E2--函数调用，E1是函数定义，E1是实参抽象型表达式(Abstraction):x.E---无名函数定义，x对应形参,E是函数体举例：xx;x.xy;x(y.xy);x.y.x；2021/7/1611表达式(3)—记法约定施用型表达式的左结合规则：E1E2E3…En=(((E1E2)E3)…)En抽象型表达式的右结合规则：x1.x2.…xn.E=x1.(x2.(…(xn.E)…))x1x2…xn.E=x1.x2.…x

9、n.Ex1.x2.…xn.E1E2E3…Em=x1.x2.…xn.(E1E2E3…Em)2021/7/1612表达式(4)—子表达式子表达式（针对不同的表达式形式）设E是一个表达式，则E的子表达式可以定义为：Ex，x就是E的子表达式；EE1E2，E1和E2以及它们的子表达式都是E的子表达式；Ex.E’，x.E’以及E’的子表达式都是E的子表达式；E(E’)，E’及其子表达式都是E的子表达式；用SUB(E)来表示E的子表达式集；2021/7/1613表达式(5)—作用域表达式中变量的作用域：

10、x.E表达式中的变量x是被绑定的，它的作用域是体表达式E中去掉所有形如x.E’子表达式后的表达式部分；x.E表达式中x.部分可以看作是变量x的定义点，在E中x的定义域中出现变量x为其使用点；举例：表达式：y(xy.y(x.xy))(z(x.xx))x的作用域是y；y的作用域是y(x.xy)；x的作用域是xy；x的作用域是xx；2021/7/1614表达式(6)—自由出现在表达式中相同的变量名，可以出现在表达式的不同的位置，它们的含义可能不同；自由出现/约束出现：表达式E中变量名x的一次出现称为自由出现，如

11、果E中任何一个形如x.E’的子表达式不包含该出现；如果存在一个x.E’的子表达式包含该出现，称为约束出现；y(xy.y(x.xy))(z(x.xx))自由约束约束自由约束出现出现出现出现出现2021/7/1615表达式(7)–自由变量自由变量：称x为表达式E的自由变量，如果E中