- 从外往里
reduction order
- normal order
M N P
left to right 先直接把N给M - applicative order
M N P
left to right
先把M 和N 内部可以reduce的先reduce
如果一个lambda expression 可以被reduce,那么normal order一定可以reduce到最简单的模式,applicative order不一定可以
convention
M N
(λx.xy)(λk.kx)
= (λt.ty)(λk.kx)
=kxy
bound variable in the left side = free variable in the right side