rule1: All variables are lambda terms (a valid expression in the lambda calculus). If x and y are lambda terms, then (x y) is a lambda term, and (λx.y) is a lambda term.
rule2: The resolution of functions is the only thing we can ever do in the Lambda Calculus.
rule3: lambda calculus accepts only one variable each time.(concluded by myself)
rule4: Functions can be resolved if they are followed by another expression.
rule5: Once we have gotten rid of all the lambdas, or if there are no more expressions after the remaining functions, we cannot replace anything any more. We can go home now.
http://palmstroem.blogspot.com/2012/05/lambda-calculus-for-absolute-dummies.html
rule1: All variables are lambda terms (a valid expression in the lambda calculus). If x and y are lambda terms, then (x y) is a lambda term, and (λx.y) is a lambda term. rule2: The resolution of functions is the only thing we can ever do in the Lambda Calculus. rule3: lambda calculus accepts only one variable each time.(concluded by myself) rule4: Functions can be resolved if they are followed by another expression. rule5: Once we have gotten rid of all the lambdas, or if there are no more expressions after the remaining functions, we cannot replace anything any more. We can go home now.
在 lambda calculus 中计算的顺序虽然无关（eager evaluation / lazy evaluation），但是因为 lambda calculus 的可读性有点差，所有很容易把两个参数作为调用来互相计算。比如我在计算 1 + 2 的时候，可以改成 1S2，我直接计算了 S2，然后再把 S2 的结果作为参数给 1，但实际上不是的，S 和 2 是 1 的两个参数 。也就是说直接用 S 和 2 替换 1 中的内容。