例5-5高层表示的β归约 (An add nn)3 add33//3置换n后取消λn 6 (λf.λx.f(fx)succ7 〉λx.succ( suCC X)7 succ (succ 7 >succ(8)=9 注:ad,3,succ,7,9是为了清晰没进 步展开为λ表达式。 但β归约有时并不能简化, 如:(λx.xx)(λx.xx),归约后仍是原公式, 这种λ表达式称为不可归约的。对应为程序设 计语言中的无限递归
例5-5 高层表示的β归约 • (λn.add n n) 3 => add 3 3 //3置换n后取消λn => 6 • (λf.λx.f(f x)) succ 7 => λx.succ (succ x) 7 => succ (succ 7) => succ (8) = 9 注：add，3， succ， 7， 9是为了清晰没进 一步展开为λ表达式。 但β归约有时并不能简化， 如：(λx.xx)(λx.xx)，归约后仍是原公式， 这种λ表达式称为不可归约的。 对应为程序设 计语言中的无限递归
(2)n归约是消除一层约束的归约:λxFx=>F (3)a换名:归约中如发生改变束定性质,则允 许换名(λ后跟的变量名),以保证原有束定 关系。例如: (λx.(λy.x)(zy)/(zy)中y是自由变量 〉λy.(zy)//此时(zy)中y被束定了,错误 〉(λx.(λwx))(zy)//因(λy.x)中函数体 无y,可换名 >Aw(zy //正确!
(2)η归约是消除一层约束的归约:λx.Fx => F (3)α换名:归约中如发生改变束定性质， 则允 许换名(λ后跟的变量名)， 以保证原有束定 关系。 例如： (λx. (λy.x)) (z y) //(zy)中y是自由变量 => λy.(zy) //此时(zy)中y被束定了， 错误！ => (λx.(λw.x))(zy) //因(λy.x)中函数体 无y， 可换名 => λw.(zy) // 正确！