您将如何在F#中实现beta减少功能? [英] How would you implement a beta-reduction function in F#?

问题描述

我正在用F#编写lambda演算，但我坚持执行beta缩减(用正式参数替换形式参数).

I am writing a lambda calculus in F#, but I am stuck on implementing the beta-reduction (substituting formal parameters with the actual parameters).

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

用法示例:

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

因此，我很乐意听到有关其他人可能如何解决此问题的一些建议.任何想法将不胜感激.

So I'd love to hear some suggestions in regards to how others might go about this. Any ideas would be greatly appreciated.

谢谢！

推荐答案

假设您的表达式表示形式如下

Assuming your representation of an expression looks like

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

，您具有函数subst (x:ident) (e1:expression) (e2:expression) : expression，该函数用e2中的e1替换了x的所有自由出现，并且想要进行正常的订单评估，您的代码应如下所示:

, you have a function subst (x:ident) (e1:expression) (e2:expression) : expression which replaces all free occurrences of x with e1 in e2, and you want normal order evaluation, your code should look something like this:

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

subst函数应如下工作:

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

For a function application it should call itself recursively on both subexpressions.

对于lambda，它应该在lambda的主体表达式上调用自己，除非它们是 .lambda的参数名称等于您要替换的标识符(在这种情况下，您可以只保留lambda，因为该标识符可以不会在其中的任何地方自由显示).

For lambdas it should call itself on the lambda's body expression unless the lambda's argument name is equal to the identifier you want to replace (in which case you can just leave the lambda be because the identifier can't appear freely anywhere inside it).

对于变量，应根据变量名是否等于标识符返回不变的变量或replace-expression.

For a variable it should either return the variable unchanged or the replacement-expression depending on whether the variable's name is equal to the identifier.

这篇关于您将如何在F#中实现beta减少功能?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！