Zapytanie o wartości logiczne w rachunek lambda

Question

Jest to reprezentacja lambda rachunek za I operatora:

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

Czy ktoś może mi pomóc w zrozumieniu tej reprezentacji?

Answer 1

Aby zrozumieć, jak reprezentować Booleans w rachunku lambda, pomaga myśleć o wyrażeniu IF, "jeśli a następnie b else c". Jest to wyrażenie, które wybiera pierwszą gałąź, b, jeśli jest prawdą, a drugie, c, jeśli jest fałszywe. wyrażenia lambda może to zrobić bardzo łatwo:

lambda(x).lambda(y).x 

daje pierwszy z jej argumentów, a

lambda(x).lambda(y).y 

daje sekundę. Więc jeśli jest jednym z tych wyrażeń, a następnie

a b c 

daje albo b lub c, który jest po prostu to, co chcemy zrobić IF. Więc zdefiniować

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

i a b c będzie zachowywać się jak if a then b else c.

Zajrzyj do środka, używając wyrażenia na (n a b), co oznacza if n then a else b. Następnie m (n a b) b oznacza

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

wyrażenie to a gdy oba m i n są true oraz b inaczej. Ponieważ a jest pierwszym argumentem twojej funkcji, a b jest drugim, a true został zdefiniowany jako funkcja, która daje pierwszy z dwóch argumentów, a następnie, jeśli m i są zarówno true, jak i całe wyrażenie. W przeciwnym razie jest to false. I to tylko definicja and!

Wszystko to zostało wymyślone przez Alonzo Church, który wymyślił rachunek lambda.

Answer 2

W rzeczywistości jest to coś więcej niż tylko operator AND. Jest to wersja lambda "if m and n then a else b. Oto wyjaśnienie:

W rachunku lambda wartość true jest reprezentowana jako funkcja pobierająca dwa argumenty * i zwracająca pierwszą. Fałsz jest reprezentowany jako funkcja pobierająca dwa argumenty * i zwracająca drugą.

Funkcja, którą pokazałeś powyżej, przyjmuje cztery argumenty *. Z wyglądu m i n mają być boleańskie ai b inne wartości. Jeśli m jest prawdą, oceni swój pierwszy argument, który jest n a b. To z kolei oceni, czy jeśli n jest prawdziwe, a b, jeśli n jest fałszywe. Jeśli m jest fałszywe, to oceni na swój drugi argument b.

Tak więc funkcja zwraca a jeśli oba m i n są prawdziwe, a b w przeciwnym wypadku.

(*) Gdzie "podjęcie dwóch argumentów" oznacza "podjęcie argumentu i zwrócenie funkcji przyjmującej inny argument".

Edycja w odpowiedzi na Twój komentarz:

and true false jak widać na stronie wiki działa tak:

Pierwszym krokiem jest po prostu zastąpić każdy identyfikator z jego definicji, tj (λm.λn. m n m) (λa.λb. a) (λa.λb. b). Teraz zostanie zastosowana funkcja (λm.λn. m n m). Oznacza to, że każde wystąpienie m w m n m jest zastępowane pierwszym argumentem ((λa.λb. a)), a każde wystąpienie n jest zastępowane drugim argumentem ((λa.λb. b)). Otrzymujemy więc (λa.λb. a) (λa.λb. b) (λa.λb. a). Teraz po prostu stosujemy funkcję (λa.λb. a). Ponieważ treść tej funkcji jest po prostu a, to znaczy pierwszym argumentem, oznacza to (λa.λb. b), tj. false (jako λx.λy. y oznacza false).

Answer 3

W rachunku lambda wartość logiczna jest reprezentowana przez funkcję, która pobiera dwa argumenty: jeden dla sukcesu i jeden dla niepowodzenia. Argumenty te są nazywane kontynuacje, ponieważ kontynuują one resztę obliczeń; boolean True wywołuje kontynuację sukcesu, a Boolean False wywołuje kontynuację błędu. To kodowanie nazywa się kodowaniem Kościoła, a idea jest taka, że ​​Boolean jest bardzo podobna do funkcji "if-then-else".

Można więc powiedzieć

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

gdzie s stojaki na sukces, f oznacza niepowodzenie, a backslash jest lambda ASCII.

Teraz mam nadzieję, że możesz zobaczyć, gdzie to idzie. Jak kodujemy and? Cóż, w C możemy rozszerzyć ją

n && m = n ? m : false 

Tylko te są funkcjami, tak

(n && m) s f = (n ? m : false) s f = n ? (m s f) : (false s f) = n ? (m s f) : f 

ALE trójoperandowy konstrukt, gdy kodowane w rachunku lambda, to tylko funkcja aplikacji, więc mamy

(n && m) s f = (n m false) s f = n (m s f) (false s f) = n (m s f) f 

Więc w końcu dojeżdżamy

&& = \n . \m . \s . \f . n (m s f) f 

A jeśli zmiany nazwy sukces i porażka kontynuacje do a i b możemy powrócić do pierwotnego

&& = \n . \m . \a . \b . n (m a b) b 

jak w przypadku innych obliczeń w rachunku lambda, zwłaszcza przy użyciu kodowania Church, często łatwiej jest pracować rzeczy z prawami algebraicznymi i rozumowaniem równoprawnym, a następnie konwertuj na lambdas na końcu.