这个 lambda 演算的范式是什么？是否有任何自由变量？

Question

我正在尝试学习 lambda 演算，但我很难做到。所以如果有人能解释一下，我将不胜感激！

(λj.λx.f(j x)) (λy.f y)

Answer 1

有一个自由变量，f。 j、x 和 y 都受抽象约束。

有两种方法可以达到正常形态。执行两次 beta 缩减

(λj.λx.f(j x)) (λy.f y) == (λx.f(<b>(λy.f y)</b> x))  <i>apply (λj.λx.f(j x)) to (λy.f y) </i>
                        == (λx.f(<b>f x</b>))        <i> apply (λy.f y) to x</i>

或执行 eta 缩减，然后进行 beta 缩减。

(λj.λx.f(j x)) (λy.f y) == (λj.λx.f(j x)) <b>f</b>  <i> replace (λy.f y) with f</i> 
                        == (λx.f(<b>f</b> x))       <i> apply (λj.λx.f(j x)) to f</i>

这个 lambda 演算的范式是什么？是否有任何自由变量？

What is the normal form of this lambda calculus and are there any free variables?

lambda-calculus