Запрос на булевских переменных в лямбда-исчислении
Это - представление лямбда-исчисления для операции И:
lambda(m).lambda(n).lambda (a).lambda (b). m(n a b) b
Кто-либо может помочь мне в понимании этого представления?
3 ответа
Чтобы понять, как представлять логические значения в лямбда-исчислении, полезно подумать о выражении IF: «if a then b else c». Это выражение, которое выбирает первую ветвь b, если она истинна, и вторую ветвь c, если она ложна. Лямбда-выражения могут сделать это очень легко:
lambda(x).lambda(y).x
даст вам первый из своих аргументов, а
lambda(x).lambda(y).y
даст вам второй. Итак, если a - одно из этих выражений, тогда
a b c
дает либо b , либо c , что мы и хотим, чтобы IF выполняла. Итак, определение
true = lambda(x).lambda(y).x
false = lambda(x).lambda(y).y
и a b c будет вести себя как if a then b else c .
Если заглянуть внутрь вашего выражения (nab) , это означает if n then a else b .
Тогда m (nab) b означает
if m then (if n then a else b) else b
Это выражение оценивается как a , если оба m и n равны истина , и b иначе. Поскольку a является первым аргументом вашей функции, а b - вторым, а true было определено как функция, которая дает первый из двух своих аргументов, тогда если m и n оба истинны , то и все выражение является истинным. В противном случае это ложь . И это только определение и !
Все это было изобретено Алонзо Черчем, который изобрел лямбда-исчисление.
В лямбда-исчислении булево число представлено функцией, которая принимает два аргумента, один для успеха, другой для неудачи. Аргументы называются продолжениями, поскольку они продолжают остальные вычисления; булево True вызывает продолжение успеха, а булево False - продолжение неудачи. Такое кодирование называется кодированием Черча, и идея заключается в том, что булево число очень похоже на функцию "if-then-else".
Таким образом, мы можем сказать
true = \s.\f.s
false = \s.\f.f
где s означает успех, f означает неудачу, а обратная косая черта - это ASCII лямбда.
Теперь, я надеюсь, вы понимаете, к чему все идет. Как нам закодировать и? Ну, в Си мы могли бы расширить это до
n && m = n ? m : false
Только это функции, так что
(n && m) s f = (n ? m : false) s f = n ? (m s f) : (false s f) = n ? (m s f) : f
НО, троичная конструкция, когда кодируется в лямбда-исчислении, является просто применением функции, так что у нас есть
(n && m) s f = (n m false) s f = n (m s f) (false s f) = n (m s f) f
Итак, в итоге мы получаем
&& = \n . \m . \s . \f . n (m s f) f
И если мы переименуем продолжения успеха и неудачи в a и b, мы вернемся к вашему оригиналу
&& = \n . \m . \a . \b . n (m a b) b
Как и с другими вычислениями в лямбда-исчислении, особенно при использовании церковных кодировок, часто проще работать с алгебраическими законами и уравнительными рассуждениями, а затем в конце преобразовывать в лямбды.
На самом деле это немного больше, чем просто оператор AND. Это версия для лямбда-исчисления if m and n then a else b . Вот объяснение:
В лямбда-исчислении истина представлена как функция, принимающая два аргумента * и возвращающая первый. Ложь представлена как функция, принимающая два аргумента * и возвращающая второй.
Показанная выше функция принимает четыре аргумента *. Судя по всему, m и n должны быть логическими, а a и b - некоторыми другими значениями. Если m истинно, он будет оценивать свой первый аргумент, который равен n a b . Это, в свою очередь, будет оценивать как a, если n истинно, и b, если n ложно. Если m ложно, он будет оценивать свой второй аргумент b.
Таким образом, в основном функция возвращает a, если и m, и n истинны, и b в противном случае.
(*) Где «принять два аргумента» означает «взять аргумент и вернуть функцию, принимающую другой аргумент».
Отредактируйте в ответ на ваш комментарий:
и true false , как видно на странице вики, работает следующим образом:
Первый шаг - просто заменить каждый идентификатор его определением, то есть ( λm.λn. mnm) (λa.λb. a) (λa.λb. b) . Теперь применяется функция (λm.λn. M n m) . Это означает, что каждое вхождение m в mnm заменяется первым аргументом ( (λa.λb. A) ), а каждое вхождение n заменяется вторым аргументом ( (λa.λb. b) ). Таким образом, мы получаем (λa.λb. A) (λa.λb. b) (λa.λb. a) . Теперь просто применим функцию (λa.λb. A) . Поскольку тело этой функции - это просто a, т.е.первый аргумент, это оценивается как (λa.λb. b) , то есть ложь (поскольку λx.λy. y означает ложь ).