如何在 F# 中实现 beta 缩减函数？

Question

我正在用 F# 编写 lambda 演算，但我一直坚持实现 beta 约简（用实际参数替换形式参数）。

(lambda x.e)f
--> e[f/x]

使用示例：

(lambda n. n*2+3) 7
--> (n*2+3)[7/n]
--> 7*2+3

所以我很想听到一些关于其他人如何解决这个问题的建议。任何想法将不胜感激。

谢谢！

Answer 1

假设您的表达式表示形式类似于

type expression = App of expression * expression
                | Lambda of ident * expression
                (* ... *)

，您有一个函数 subst (x:ident) (e1:expression) (e2:expression) : expression ，它替换所有出现的 x 与 e2 中的 e1，并且您想要正常的顺序评估，您的代码应如下所示：

let rec eval exp =
  match exp with
  (* ... *)
  | App (f, arg) -> match eval f with Lambda (x,e) -> eval (subst x arg e)

subst 函数应按如下方式工作：

对于函数应用程序，它应该在两个子表达式上递归地调用自身。

对于 lambda，它应该在 lambda 的主体表达式上调用自身，除非 lambda 的参数名称等于您要替换的标识符（在这种情况下，您可以保留 lambda，因为标识符不会出现自由地在其内部的任何地方）。

对于变量，它应该返回未更改的变量或替换表达式，具体取决于变量的名称是否等于标识符。