f# - 您将如何在 F# 中实现 beta 缩减功能？

Question

我正在用 F# 编写 lambda 演算，但我坚持执行 beta-reduction（用实际参数替换形式参数）。

(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
                (* ... *)

，你有一个用insubst (x:ident) (e1:expression) (e2:expression) : expression替换所有自由出现的函数，并且你想要正常的顺序评估，你的代码应该是这样的：xe1e2

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，因为标识符不能在其中的任何地方自由出现）。

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