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

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