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

, 你有一个函数 subst (x:ident) (e1:expression) (e2:expression) : expression它替换了所有免费出现的 x与 e1在 e2 ，并且您想要正常的订单评估，您的代码应如下所示:

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

对于一个变量，它应该返回不变的变量或替换表达式，这取决于变量的名称是否等于标识符。