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

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

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

пример использования:

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

Поэтому я хотел бы услышать некоторые предложения относительно того, как другие могут поступить по этому поводу. Любые идеи очень приветствуются.

Спасибо!


f# lambda-calculus
person klactose    schedule 28.10.2010    source источник
comment
Кстати, пример, который я использовал, взят из обсуждения лямбда-исчисления, найденного по адресу csse.monash.edu.au/~lloyd/tildeFP/Lambda/Ch/01.Calc.html   -  person klactose    schedule 28.10.2010

Ответы (1)


arrow_upward
4
arrow_downward

Предполагая, что ваше представление выражения выглядит как

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

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

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

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

person sepp2k    schedule 28.10.2010
comment
Спасибо за ответ sepp2K. Вы в значительной степени поняли суть того, что я пытаюсь сделать. Но та часть, с которой у меня возникли проблемы с полной реализацией, — это beta_reduce. Здесь вы внедрили функцию под названием subst, которая делает то же самое, что и beta_reduce, но без объяснения того, как будет реализована функция subst. Что оставляет меня в том же положении, что и раньше. - person klactose; 28.10.2010
comment
Кроме этого, ваш код довольно хорошо отражает то, как выглядит мой. - person klactose; 28.10.2010
comment
Да, и еще одна вещь... разве ваш пример приложения не должен заканчиваться на eval(beta_reduce(x,e) arg)? В противном случае, разве мы не просто возвращали бы функцию, фактически не применяя ее? - person klactose; 28.10.2010
comment
@klactose: я обновил свой ответ, чтобы объяснить, как реализовать subst. И да, конечно, он должен вызывать eval по результату подстановки. Глупая ошибка. - person sepp2k; 28.10.2010
comment
Спасибо за ваш вклад sepp2k. Я не уверен, что понимаю, что вы имеете в виду, когда предлагаете, чтобы subst вызывал себя рекурсивно для обоих подвыражений приложения-функции. Приложение моей функции выглядит так: App(expr1, expr2). В то время как expr1 должно быть лямбда-выражением, expr2 — это значение, которое должно заменять переменную в лямбда-выражении. Итак, если subst принимает 3 параметра, какие параметры будут использоваться для рекурсивных вызовов не-лямбда-выражений??? Извините за долгий ответ! - person klactose; 29.10.2010
comment
Я надеюсь, что этот вопрос имел смысл для вас - person klactose; 29.10.2010
comment
@klactose: Вы говорите, что expr1 должно быть лямбда-выражением. Хотя это не обязательно правильно. ((lambda x. x) y) z — допустимое выражение, которое следует анализировать как что-то вроде App ( App (Lambda ("x", Var "x"), Var "y") Var "z". Здесь внешний App имеет в качестве первого аргумента App, а не Lambda, и это совершенно верно. - person sepp2k; 29.10.2010
comment
Тогда вы говорите, что expr2 — это значение, которое должно заменить переменную в лямбда-выражении. В каком-то смысле это правильно, но технически expr2 — это выражение, которое при вычислении возвращает значение, которое вы хотите заменить (и это значение вполне может быть лямбда-выражением — в чистом лямбда-исчислении это было бы единственно возможное значение). - person sepp2k; 29.10.2010
comment
Итак, я пытаюсь сказать: и expr1, и expr2 должны иметь тип expression (и если ваше определение expression похоже на определение в моем ответе, они будут), поэтому вы можете использовать их в качестве третьего аргумента для subst без проблема. - person sepp2k; 29.10.2010
comment
Еще раз спасибо sepp2K. Я думаю, что разобрался с бета-снижением. Теперь я пытаюсь понять, как реализовать оператор фиксированной точки в том же лямбда-исчислении. Я дам этому вопросу новую тему. Цените все ваши вклады! - person klactose; 03.11.2010