Lambda微积分表达式

Question

对于lambda表达式(x (λx y. x y) z h)，我不明白自由变量x (outer x),z和h可以在C代码中进行转换吗？

问候， darkie

Answer 1

自由变量是Lambda微积分中的一个特殊情况 - 它们不能被“转换”为任何东西，所以通常它们只被视为符号。显然

mk_app(mk_app(mk_app(mk_sym("x"), 
        mk_lam("x", 
          mk_lam("y", 
            mk_app(mk_var("x"), 
              mk_var("y"))))), 
       mk_sym("z")), 
     mk_sym("h")); 

，您可以使用mk_var()那些：在你的榜样，并给出了lambda表达式一些虚构的构造函数，你把它翻译为以下（包括对付隐钻营）C类的表达符号也是如此，但这会误导，因为它们不是真正的变量，因为它们没有绑定。换句话说，如果你对表达式进行了任何alpha转换，他们将不得不保持不变。

（顺便说一下，这里的相关部分是Barendregt的自由变量假设。）

Answer 2

转换演算为C代码是不平凡的。通常你会写一个解释器，逐步评估。也就是说，将表达式转换为树，并找到最接近根节点的节点，该节点是左侧为lambda的应用程序。现在替换在右侧。重复，直到你不能再申请，并且你有结果。

请注意，这里没有直接等价于自由变量;我们只是用它们来知道在哪里取代东西。

请记住，图灵等价不需要精确两个图灵完备语言中的任何概念之间的等价性。它只是要求你能够与另一个模拟一个，反之亦然。