Как определить y-combinator без "let 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 ....

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

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 ...?

Ответ 1

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

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

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

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-combinator:

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-combinator) аппликативного порядка:

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

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

Ответ 2

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

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

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

EDIT: kvb показывает в своем ответе, что определения типов (одна из функций, отсутствующих в просто типизированном лямбда-исчислении, но присутствующих в let-rec-less F #), позволяет получить некоторую рекурсию. Очень умный.

Ответ 3

Случаи case и let в производных ML - вот что делает Turing Complete, я считаю, что они основаны на System F, а не просто набраны, но точка одна и та же.

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

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

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

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

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

Ответ 4

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

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

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

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

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