Как бы вы реализовали функцию бета-сокращения в F #?

Question

Я пишу лямбда-исчисление в F #, но я застрял на реализации бета-редукции (заменяя формальные параметры фактическими параметрами).

(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 должна работать следующим образом:

Для приложения функции оно должно называть себя рекурсивно для обоих подвыражений.

Для лямбд он должен называть себя по выражению тела лямбды в если аргументе имя лямбды никогда равно идентификатору вы хотите заменить (в этом случае вы можете просто оставить лямбда быть, потому что идентификатор не может появиться свободно где-нибудь внутри).

Для переменной она должна либо возвращать переменную без изменений, либо заменять-выражение в зависимости от того, совпадает ли имя переменной с идентификатором.