基本函数 TRUE和 FALSE的λ表达式 TF λx.λy.x nX. My y 整数的入表达式: 0=λx.λy.y 1=入x.入y.xy 2=λx.λy.x(xy) 入x.入 yX(X y n个
基本函数 • TRUE 和FALSE的λ表达式 T = λx.λy.x F = λx.λy.y • 整数的λ表达式： 0=λx.λy.y 1=λx.λy.x y 2=λx.λy.x(x y) n=λx.λy.x(x(…(x y)) n个
基本操作函数 not=λz.(zF)T)=Az.((zλx.λy.y)(λx.Ay.x)) and=λa.λb.(ab)F)=λa.λb.(ab)x.Ay.y) or=λa.Ab.(aT)b)=Ma.λb.((aλx.λy.x)b) 以下是算术操作函数举例 =add=λx.λy.λa.λb.(xa)(ya)b *= multiply=λx.λy.Aa.(x(ya)) kx= sqr X. My(X identity=λx.x //同一函数 succ=An.(λx.λy.nx(xy)//后继函数 zerop=n.n(λx.F)T λn.n(λz.λx.λy.y)(λx.λy.y)/判零 函数
• 基本操作函数 not=λz.((zF)T)=λz.((zλx.λy.y)(λx.λy.x)) and=λa.λb.((ab)F) = λa.λb.((ab)λx.λy.y)) or = λa.λb.((aT)b) = λa.λb.((a λx.λy.x)b) 以下是算术操作函数举例： + = add = λx.λy.λa.λb.((xa)(ya)b) * = multiply = λx.λy.λa.((x(ya))) ** = sqr = λx.λy.(yx) identity = λx.x //同一函数 succ = λn.(λx.λy.nx(x y)) //后继函数 zerop = λn.n(λx.F)T =λn.n(λz.λx.λy.y)(λx.λy.y) //判零 函数
例:3+4就写add34,add3返回“加3函数 ”应用到4上当然就是7。写全了是: (λx.λy.λa.λb.((xa)(ya)b)) (λp.λq.(p(p(pq))(λs.λt.(s(s(s(st)) naMb.aa(a(ala(a(a b)
例：3+4就写add 3 4， add 3返回“加3函数 ”应用到4上当然就是7。写全了是： （λx.λy.λa.λb.((x a)(y a) b )） (λp.λq.(p(p(p q)))(λs.λt.(s(s(s(s t))) λa.λb.(a(a(a(a(a(a(a b)))))))
归约与范式 归约将复杂的表达式化成简单形式,即按一定的 规则对符号表达式进行置换。 例:归约数1的后继 (succ1)=〉(λn.(λx.Ay.nx(xy))1 =>(λx.λy.1x(xy)) 〉(λx.λy.(λp.λq.pq)x(xy)) 〉(λx.λy.(λq.xq)(xy) 〉(λx.Ay.x(xy))=2 注:succ和1都是函数(1是常函数),第一步是λn 束定的n被1置换。展开后,x置换p,(xy)置换 q,最后一行不能再置换了,它就是范式,语 义为2
归约与范式 归约将复杂的表达式化成简单形式， 即按一定的 规则对符号表达式进行置换。 例：归约数1的后继 (succ 1) => (λn.(λx.λy.n x(x y))1) => (λx.λy.1 x(x y)) => (λx.λy.(λp.λq. p q) x(x y)) => (λx.λy.(λq. x q)(x y)) => (λx.λy.x(x y))=2 注：succ和1都是函数(1是常函数)，第一步是λn 束定的n被1置换。 展开后， x置换p， (xy)置换 q， 最后一行不能再置换了， 它就是范式， 语 义为2
(1)β归约:β归约的表达式是一个A应用表 达式(Ax.MN),其左边子表达式是入函数表 达式,右边是任意λ表达式。β归约以右边的 λ表达式置换函数体M中λ指明的那个形参变量 形式地,我们用[N/X,M表示对(AxMN)的 置换(规则略)。 关键的问题是注意函数体中要置换的变量是否 自由出现,如: ((λx.x(λx.(xy)(z2) >(z)(λx.(z)y)//错误,第二x个非自由出现 (zz)(λx.(xy)//正确
（1）β归约：β归约的表达式是一个λ应用表 达式(λx.M N)， 其左边子表达式是λ函数表 达式，右边是任意λ表达式。β归约以右边的 λ表达式置换函数体M中λ指明的那个形参变量。 形式地，我们用[N/X,M]表示对（λx.M N）的 置换（规则略）。 关键的问题是注意函数体中要置换的变量是否 自由出现，如： ((λx.x(λx.(xy)))(zz)) =>(zz)(λx.((zz)y)) //错误，第二x个非自由出现。 =>(zz)(λx.(xy)) //正确