Как мне определить y-combinator без "let rec”?

Question

Почти во всех примерах y-комбинатор на языках типа ML пишется следующим образом:

let rec y f x = f (y f) x
let factorial = y (fun f -> function 0 -> 1 | n -> n * f(n - 1))

Это работает, как и ожидалось, но определение y-комбинатора с помощью let rec ....

Я хочу определить этот комбинатор без использования рекурсии, используя стандартное определение:

Y = λf·(λx·f (x x)) (λx·f (x x))

Прямой перевод выглядит следующим образом:

let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));;

Однако F # жалуется, что не может определить типы:

  let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));;
  --------------------------------^

C:\Users\Juliet\AppData\Local\Temp\stdin(6,33): error FS0001: Type mismatch. Expecting a
    'a    
but given a
    'a -> 'b    
The resulting type would be infinite when unifying ''a' and ''a -> 'b'

Как мне написать y-комбинатор в F # без использования let rec ...?

Answer 1

Как указывает компилятор, не существует типа, который можно было бы присвоить x так что выражение (x x) хорошо типизирован (это не совсем верно;вы можете явно ввести x как obj->_ - смотрите мой последний абзац).Вы можете обойти эту проблему, объявив рекурсивный тип, чтобы работало очень похожее выражение:

type 'a Rec = Rec of ('a Rec -> 'a)

Теперь Y-комбинатор можно записать в виде:

let y f =
  let f' (Rec x as rx) = f (x rx)
  f' (Rec f')

К сожалению, вы обнаружите, что это не очень полезно, потому что F # - строгий язык, поэтому любая функция, которую вы попытаетесь определить с помощью этого комбинатора, вызовет переполнение стека.Вместо этого вам нужно использовать версию Y-combinator в прикладном порядке (\f.(\x.f(\y.(x x)y))(\x.f(\y.(x x)y))):

let y f =
  let f' (Rec x as rx) = f (fun y -> x rx y)
  f' (Rec f')

Другим вариантом было бы использовать явную лень для определения Y-комбинатора нормального порядка:

type 'a Rec = Rec of ('a Rec -> 'a Lazy)
let y f =
  let f' (Rec x as rx) = lazy f (x rx)
  (f' (Rec f')).Value

Это имеет тот недостаток, что для определений рекурсивных функций теперь требуется явное принудительное использование отложенного значения (с использованием Value собственность):

let factorial = y (fun f -> function | 0 -> 1 | n -> n * (f.Value (n - 1)))

Однако у него есть то преимущество, что вы можете определять нефункциональные рекурсивные значения, точно так же, как вы могли бы в ленивом языке:

let ones = y (fun ones -> LazyList.consf 1 (fun () -> ones.Value))

В качестве последней альтернативы вы можете попытаться лучше аппроксимировать нетипизированное лямбда-исчисление, используя боксирование и даункастинг.Это дало бы вам (опять же, используя версию Y-комбинатора прикладного порядка):

let y f =
  let f' (x:obj -> _) = f (fun y -> x x y)
  f' (fun x -> f' (x :?> _))

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

Answer 2

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

Система типов F# не совсем похожа на систему типов просто типизированного лямбда-исчисления, но она достаточно близка к ней.Фа# без let rec очень близко к просто типизированному лямбда-исчислению - и, повторюсь, на этом языке вы не можете определить термин, который не заканчивается, и это исключает также определение Y.

Другими словами, в F# «let Rec» должен быть как минимум языковым примитивом, потому что даже если бы вы могли определить его на основе других примитивов, вы не смогли бы ввести это определение.Наличие его в качестве примитива позволяет, среди прочего, придать этому примитиву особый тип.

РЕДАКТИРОВАТЬ:kvb показывает в своем ответе, что определения типов (одна из функций, отсутствующая в просто типизированном лямбда-исчислении, но присутствующая в F # без let-rec) позволяют получить своего рода рекурсию.Очень умно.

Answer 3

Операторы Case и let в производных ML делают его полным по Тьюрингу. Я считаю, что они основаны на системе F, а не просто напечатаны, но суть та же.

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

Сильная нормализация означает, что любое выражение имеет в точности один нормальная форма, где нормальная форма — это выражение, которое не может быть сокращено дальше; это отличается от нетипизированной формы, где каждое выражение имеет на максимуме одна нормальная форма, но оно может вообще не иметь нормальной формы.

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

Другая известная теорема, «Проблема остановки», подразумевает, что сильно нормализуемые языки не являются полными по Тьюрингу. решать (отлично от доказательства) тьюринг-полного языка, какое подмножество его программ остановится на каком входе.Если язык сильно нормализуется, то его остановку можно разрешить, а именно: всегда останавливается.Наш алгоритм принятия решения - это программа: true;.

Чтобы решить эту проблему, производные ML расширяют System-F с помощью case и let (rec), чтобы преодолеть эту проблему.Таким образом, функции могут снова ссылаться на себя в своих определениях, что фактически делает их вообще не лямбда-исчислениями, больше невозможно полагаться только на анонимные функции для всех вычислимых функций.Таким образом, они могут снова войти в бесконечные циклы и восстановить свою полноту по Тьюрингу.

Answer 4

Короткий ответ:Вы не можете.

Длинный ответ:Просто типизированное лямбда-исчисление является строго нормализующим.Это означает, что это не эквивалент Тьюринга.Причина этого в основном сводится к тому, что Y-комбинатор должен быть либо примитивным, либо определяться рекурсивно (как вы обнаружили).Его просто невозможно выразить в системе F (или более простых типизированных исчислениях).Обойти это невозможно (в конце концов, это доказано).Y-комбинатор, ты может Однако реализация работает именно так, как вы хотите.

Я бы посоветовал вам попробовать схему, если вам нужен настоящий Y-комбинатор в церковном стиле.Используйте аппликативную версию, приведенную выше, поскольку другие версии не будут работать, если вы явно не добавите ленивость или не используете ленивый интерпретатор схемы.(Технически схема не является полностью нетипизированной, но она динамически типизирована, что для этого достаточно.)

См. это для доказательства сильной нормализации:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.127.1794

Подумав еще немного, я почти уверен, что добавление примитивного Y-комбинатора, который ведет себя точно так же, как определенный letrec, делает Систему F Тьюринга завершенной.Все, что вам нужно сделать, чтобы смоделировать машину Тьюринга, — это реализовать ленту как целое число (интерпретируемое в двоичном формате) и сдвиг (для позиционирования головы).