lambda-calculus - Lambda 演算表达式

Question

对于一个lambda表达式(x (λx y. x y) z h)，我不明白怎么自由变量x (outer x)，z并且h可以在C代码中转换？

问候，小黑

Answer 1

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

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

请记住，图灵等价并不要求两种图灵完备语言中的任何概念之间完全等价。它只要求您能够模仿另一个，反之亦然。

Answer 2

自由变量是 Lambda 演算中的一种特殊情况——它们不能“转换”为任何东西，所以通常它们被视为符号。在您的示例中，并为 lambda 表达式提供了一些虚构的构造函数，您将其转换为以下（包括处理隐式柯里化）类 C 表达式：

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()这些符号，但这会产生误导，因为它们不是真正的变量，因为它们没有被绑定。换句话说，如果您对表达式进行任何 alpha 转换，它们将必须保持不变。

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