Haskell `let` связывания в лямбда-исчислении - PullRequest
Новая
       82

Haskell `let` связывания в лямбда-исчислении

0 голосов
/ 06 января 2019

Я хочу понять, как работают привязки let в Haskell (или, может быть, лямбда-исчисление, если реализация Haskell отличается?)

Я понимаю, прочитав Напишите вам на Haskell , что это действительно для одной let привязки. 

let x = y in e == (\x -> e) y

Это имеет смысл для меня, поскольку это согласуется с тем, как работают привязки в лямбда-исчислении. Меня смущает использование нескольких привязок let, где одна привязка может ссылаться на привязки выше. Я приведу тривиальный пример.

Оригинальный код: 

let times x y = x * y
    square x = times x x
in square 5

Мое предположение при реализации: 

(\square times -> square 5) (\x -> times x x) (\x -> x * x)

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

(\square -> square 5) ((\times x -> times x x) (\x -> x * x))

Это правильный способ реализации этой привязки, по крайней мере, в лямбда-исчислении?

Ответы [ 3 ]

0 голосов
/ 06 января 2019

Обратите внимание, что несколько привязок let можно уменьшить до одной, определяя пару (кортеж, в общем случае). Например. мы можем переписать 

let times x y = x * y
    square x = times x x
in square 5

в 

let times = \x y -> x * y
    square = \x -> times x x
in square 5

тогда 

let (times, square) = (\x y -> x * y, \x -> times x x)
in square 5

тогда, если хотите, 

let pair = (\x y -> x * y, \x -> fst pair x x)
in snd pair 5

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

(\pair -> snd pair 5) (fix (\pair -> (\x y -> x * y, \x -> fst pair x x)))

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

0 голосов
/ 06 января 2019

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

Мы хотим реализовать следующую программу с двумя привязками let: 

let times a b = a * b
    square x = times x x
in square 5

Для начала давайте упростим это до сути того, что мы хотим: 

square 5

Достаточно просто. Однако square в этом случае не определено! Ну, мы можем связать это, используя механизм, который обеспечивает нам наш язык - лямбда. Это дает нам (\ square -> square 5) (\x -> times x x). Теперь square определен, но его двоюродный брат times не ... Ну, нам нужна еще одна лямбда! Наша финальная программа должна выглядеть так: 

(\times -> (\square -> square 5) (\x -> times x x)) (\a b -> a * b)

Обратите внимание, что (\times -> ...) полностью охватывает наш последний шаг, так что times будет находиться в области видимости, поскольку он связан. Это согласуется с ответом @rampion и сокращается следующим образом: 

(\times -> (\square  -> square 5) (\x -> times x x)) (\a b -> a * b) =>
(\square -> square 5) (\x -> (\a b -> a * b) x x)                    =>
(\square -> square 5) (\x -> (\b -> x * b) x)                        => 
(\square -> square 5) (\x -> x * x)                                  => 
(\x -> x * x) 5                                                      =>
5 * 5                                                                => 
25

Если бы функция square не зависела от times, мы могли бы легко написать (\times square -> ..... Зависимость означает, что мы должны вкладывать эти две среды, одна из которых содержит times, а другая внутри той, которая может использовать ее определение.

Спасибо за вашу помощь! Я поражен простотой и мощью лямбда-исчисления.

0 голосов
/ 06 января 2019

Пример times / square можно выразить в терминах лямбда-функций, используя область видимости: 

(\times -> (\square -> square 5)(\x -> times x x))(\x y -> x * y)

Но области видимости недостаточно для рекурсивных или взаимно рекурсивных привязок типа 

let ones = 1 : ones in take 5 ones

let even n = n == 0 || odd (abs n - 1)
    odd n  = n /= 0 && even (abs n - 1)
in even 7

В лямбда-исчислении вы можете определить y-комбинатор для рекурсии как 

(\f -> (\x -> f (x x))(\x -> f (x x)))

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

Использование y-комбинатора позволяет нам выразить вышеупомянутые привязки, используя лямбда-исчисление: 

(\ones -> take 5 ones)((\f -> (\x -> f (x x))(\x -> f (x x)))(\ones -> 1 : ones))

(\evenodd -> evenodd (\x y -> x) 7)((\f -> (\x -> f (x x))(\x -> f (x x)))(\evenodd c -> c (\n -> n == 0 || evenodd (\x y -> y) (abs n - 1)) (\n -> n /= 0 && evenodd (\x y -> x) (abs n - 1))))
...