lambda calculus

• 从外往里
  reduction order
  image.png
• 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