5.2.2约束变量和自由变量 (λx.(bx)x)) 自由变量 约束变量 (A. Ay.(a x y)(b(ny. (x y)))
5.2.2 约束变量和自由变量 (λx.((b x) x)) 自由变量 约束变量 （λx.λy.(a x y)(b (λy.(x y))))
入表达式中的作用域复盖 (Ax (Nx(x a)( b)(x c)) 第1个x约束于P 第2个x约束于0 第3个x在M中自由,约束于0,P 第4个x在N中自由,约束于P 第5个x在R中自由,在Q中这5个x均约束出现, b,c自由出现
λ表达式中的作用域复盖 （λx.(λx.(x a))(x b)(x c)） P M N R O Q 第1个x约束于P 第2个x约束于O 第3个x在M中自由，约束于O，P 第4个x在N中自由，约束于P 第5个x在R中自由，在Q中这5个x均约束出现, b，c自由出现
基本函数 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)))))))