Как бы вы реализовали оператор с фиксированной точкой (Y комбинатор) в F #?

Question

Я использую F # для создания лямбда-исчисления. В настоящее время я застрял, пытаясь выяснить, как мне реализовать оператор с фиксированной точкой (также называемый Y комбинатор).

Я думаю, что все остальное в порядке. Выражения представлены следующим дискриминационным объединением:

type Expr =
 | Const of int
 | Plus  of Expr * Expr
 | Times of Expr * Expr
 | Minus of Expr * Expr
 | Div   of Expr * Expr
 | Neg   of Expr
 | Var   of string
 | Fun   of string * Expr
 | App   of Expr * Expr
 | If    of Expr * Expr * Expr

Моя eval функция работает. Все следующие примеры дают ожидаемые результаты.
пример 1:
> eval (Fun("x",Plus(Const 7,Var("x"))));;
val it : Expr = Fun ("x",Plus (Const 7,Var "x"))
пример 2:
> eval (App(Fun("x",Plus(Const 7,Var("x"))),Const 3));;
val it : Expr = Const 10
пример 3:
> eval (If(Const 0,Const 3,Const 4));;
val it : Expr = Const 4

Но, как я уже говорил, мне трудно реализовать оператор с фиксированной запятой в моем лямбда-исчислении. здесь определяется как:
Y = lambda G. (lambda g. G(g g)) (lambda g. G(g g))

У кого-нибудь есть предложения? Я посмотрел на другие вопросы, касающиеся комбинатора Y, но не смог найти ничего, что смог бы успешно принять.

Вся помощь приветствуется.

Редактировать: Исправлена ​​опечатка в коде ... ранее у меня было Mult вместо Minus в дискриминируемом объединении. Забавно, что я только что это заметил!

Answer 1

Версия, на которую вы ссылаетесь, работает только с ленивым языком, и если ваш язык не использует ленивую стратегию оценки, вы застряли в бесконечном цикле. Попробуйте перевести это:

Y = lambda G. (lambda g. G(lambda x. g g x)) (lambda g. G(lambda x. g g x))

Answer 2

Насколько я помню, в нетипизированном лямбда-исчислении существует целый класс Y-комбинаторов, но реализовать его даже трудно, даже если ваш язык строго типизирован, хотя люди пытались делать особые случаи в ML, а также F #. Это не очень полезно, если ваш язык поддерживает рекурсию (а лямбда-исчисление - нет). Взгляните на обсуждения по этой теме, которые Stackoverflow отмечал как «функциональное программирование» или ML, я думаю, что есть некоторые идеи:

Практический пример Y-Combinator