Как я определяю y-combinator без “rec, которому позволяют”?
Почти во всех примерах y-combinator на языках типа ML записан как это:
let rec y f x = f (y f) x
let factorial = y (fun f -> function 0 -> 1 | n -> n * f(n - 1))
Это работает как ожидалось, но как обманывать для определения использования y-combinator let rec ....
Я хочу определить этот combinator, не используя рекурсию, с помощью стандартного определения:
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-combinator в F# без использования let rec ...?
3 ответа
Как указывает компилятор, не существует типа, который можно было бы присвоить x , чтобы выражение (xx) было хорошо типизировано ( это не совсем так; вы можете явно ввести 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-комбинатора ( \ f. (\ Xf (\ y. (Xx) y)) (\ xf (\ y. (Xx) 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 property):
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 :?> _))
Это имеет очевидный недостаток, заключающийся в том, что он вызовет ненужную упаковку и распаковку, но, по крайней мере, это полностью внутренне для реализации и никогда не будет привести к сбою во время выполнения.
Я бы сказал, что это невозможно, и спросил почему, я бы рукой встряхнул и сослался на тот факт, что просто набранное лямбда-вычисление имеет свойство нормализации . Короче говоря, все условия простого лямбда исчисления заканчиваются (следовательно, Y не может быть определена в просто набранном лямбда исчислении).
F# система типов не совсем система типов просто набранной лямбда исчисления, но она достаточно близка. F# без let rec действительно близок к простому типизированному лямбда-вычислению -- и, повторяю, на этом языке вы не можете определить термин, который не завершается, и это исключает определение Y тоже.
Другими словами, в F#, "let rec" должен быть языком примитивным, по крайней мере потому, что даже если бы вы могли определить его по другим примитивам, вы не смогли бы набрать это определение. Наличие его в качестве примитива позволяет, среди прочего, дать этому примитиву специальный тип.
EDIT: kvb показывает в своем ответе, что определения типов (одна из особенностей, отсутствующая в просто набранном лямбда-вычислении, но присутствующая в let-rec-менее F#) позволяют получить некую рекурсию. Очень умно.
Операторы case и let в производных ML - это то, что делает его полным по Тьюрингу, я считаю, что они основаны на системе F, а не просто типизированы, но суть та же.
Система F не может найти тип для любого комбинатора с фиксированной точкой, если бы и могла, это не было строго нормализующим.
Сильно нормализация означает, что любое выражение имеет ровно одну нормальную форму, где нормальная форма - это выражение, которое не может быть сокращено дальше, это отличается от нетипизированного, где каждое выражение имеет на макс. одна нормальная форма, она может вообще не иметь нормальной формы.
Если типизированные лямбда-исчисления могут каким-либо образом построить оператор с фиксированной точкой, выражение вполне может не иметь нормальной формы.
Другая известная теорема, проблема остановки, подразумевает, что строго нормализующие языки не являются полными по Тьюрингу, она говорит, что невозможно решить (иначе, чем доказать) полного по Тьюрингу языка, какое подмножество его программ остановит на каком входе. Если язык сильно нормализуется, то он разрешимо, если он останавливается, а именно, он всегда останавливается. Наш алгоритм определения, что это программа: истина; .
Чтобы решить эту проблему, ML-производные расширяют System-F с помощью case и позволяют (rec) преодолеть это. Таким образом, функции могут снова ссылаться на себя в своих определениях, что фактически делает их больше не лямбда-исчислениями, больше невозможно полагаться только на анонимные функции для всех вычислимых функций. Таким образом, они могут снова войти в бесконечные циклы и восстановить свою полноту по Тьюрингу.