Запрос на логиках в лямбда-исчислении

Question

Это представление о вычислении лямбда для и оператора:

lambda(m).lambda(n).lambda (a).lambda (b). m(n a b) b

Может кто-нибудь помочь мне в понимании этого представления?

Answer 1

Чтобы понять, как представлять логии в исчислении лямбда, он помогает подумать о том, что если выражение, «если a тогда b ust c». Это выражение, которое выбирает первую ветку B, если это правда, а второй, C, если это ложно. Лямбда выражения может сделать это очень легко:

lambda(x).lambda(y).x

даст вам первый из своих аргументов, а также

lambda(x).lambda(y).y

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

a b c

дает тоже b или c, что только то, чем мы хотим, если делать. Так определить

 true = lambda(x).lambda(y).x
false = lambda(x).lambda(y).y

а также a b c будет вести себя как if a then b else c.

Глядя внутрь вашего выражения в (n a b), это значит if n then a else bОтказ потом m (n a b) b означает

if m then (if n then a else b) else b

Это выражение оценивает a Если оба m а также n являются true, и к b иначе. С a является первым аргументом вашей функции и b второй, и true был определен как функция, которая дает первый из двух аргументов, то если m а также n оба true, Так что это все выражение. В противном случае это false. Отказ И это просто определение and!

Все это было изобретено Церкви Алонзо, который изобрел лямбда исчисления.

Answer 2

В укачении лямбда логическое значение представлено функцией, которая принимает два аргумента, один для успеха и один для неудачи. Аргументы называются продолжение, потому что они продолжаются с остальными вычислениями; Логические истинные называют продолжением успеха и логическими ложными основаниями, вызывает продолжение провала. Это кодирование называется кодированием церкви, и идея состоит в том, что логическое значение очень похоже на «функцию IF-Thans».

Итак, мы можем сказать

true  = \s.\f.s
false = \s.\f.f

куда s стоит за успех, f Стенды на неудачу, а обратная косание - это лямбда ASCII.

Теперь я надеюсь, что вы можете увидеть, где это происходит. Как мы кодируем and? Ну, в C мы могли бы расширить его

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

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

Answer 3

На самом деле это немного больше, чем просто и оператор. Это версия лямбда исчисления if m and n then a else b. Отказ Вот объяснение:

В Lambda Calculus True представлен как функция, принимающая два аргумента * и вернув первых. False представлен как функция, принимающая два аргумента * и возвращая вторую.

Функция, которую вы показали выше, принимает четыре аргумента *. Из взгляда его M и N должны быть логическими и a и b некоторые другие значения. Если M верно, он будет оценивать свой первый аргумент, который n a b. Отказ Это, в свою очередь, будет оценивать до A, если n верно и B, если n ложно. Если M ложно, он оценивает его второй аргумент b.

Таким образом, в основном функция возвращает A, если как M и N верно и B иначе.

(*) Где «принимать два аргумента» означает «взять аргумент и возвращение функции, предпринимающую другой аргумент».

Редактировать в ответ на ваш комментарий:

and true false Как видно на странице Wiki работает так:

Первый шаг - просто заменить каждый идентификатор с его определением, то есть (λm.λn. m n m) (λa.λb. a) (λa.λb. b). Отказ Теперь функция (λm.λn. m n m) применяется. Это означает, что каждое возникновение м в m n m заменяется первым аргументом ((λa.λb. a)) и каждое вхождение N заменяется на второй аргумент ((λa.λb. b)). Итак, мы получаем (λa.λb. a) (λa.λb. b) (λa.λb. a). Отказ Теперь мы просто применяем функцию (λa.λb. a). Отказ Поскольку тело этой функции просто A, то есть первый аргумент, это оценивает (λa.λb. b), т.е. false (так как λx.λy. y означает false).