Dlaczego rachunek Lambda nie może reprezentować niektórych kombinacji?

Ten artykuł sugeruje, że istnieją kombinatory (reprezentujące obliczenia symboliczne), których nie można przedstawić za pomocą rachunku Lambda (jeśli dobrze rozumiem):

Jest kilka rzeczy, które można chcieć robić w praktyce i których nie można bezpośrednio wyrazić w rachunku lambda.

Rachunek SF jest przykładem. Jego ekspresyjna moc nie jest wiadomością; interesująca część artykułu (nie pokazana na slajdach) to leżąca u podstaw teoria kategorii. Rachunek SF jest analogiczny do implementacji lisp, w której pozwalasz funkcjom sprawdzać reprezentację ich argumentów - możesz więc pisać takie rzeczy jak (print (lambda (x) (+ x 2)))⟹ "(lambda (x) (+ x 2))".

Innym ważnym przykładem jest równoległość Plotkina lub . Intuicyjnie rzecz biorąc, ogólny wynik mówi, że rachunek lambda jest sekwencyjny: funkcja, która bierze dwa argumenty, musi wybrać jeden do oceny jako pierwszy. Niemożliwe jest napisanie wyrażenia lambda ortakiego, że ( or⊤ ⊥) ⟹ ⊤, ( or⊥ ⊤) ⟹ ⊤ i or⊥ ⊥ ⟹ ⊥ (gdzie ⊥ jest terminem nie kończącym się, a ⊤ jest terminem kończącym). Jest to znane jako „równoległe” lub „równoległe”, ponieważ równoległa implementacja może wykonać jeden krok każdej redukcji i zatrzymać się za każdym razem, gdy jeden z argumentów zakończy się.

Jeszcze inną rzeczą, której nie można zrobić w rachunku lambda, jest wejście / wyjście. Trzeba by do tego dodać dodatkowe prymitywy.

Oczywiście wszystkie te przykłady można przedstawić w rachunku lambda przez dodanie jednego poziomu pośredniego, zasadniczo reprezentując terminy lambda jako dane. Ale wtedy model staje się mniej interesujący - tracisz związek między funkcjami w modelowanym języku a abstrakcjami lambda.

Odpowiedź na twoje pytanie zależy od tego, jak zdefiniujesz „obliczenia” i „reprezentowane”. Z drugiej strony wątek na LtU, o którym wspominał sclv , składa się głównie z ludzi rozmawiających obok siebie z powodu niedopasowanych definicji różnych terminów.

Różnica z pewnością nie dotyczy mocy obliczeniowej - każdy rozważany system jest równoważny z Turingiem. Chodzi o to, że sama równoważność Turinga tak naprawdę nie mówi nic o strukturze lub semantyce wyrażenia. Z tego względu w wyjątkowo minimalistycznych modelach obliczeniowych, które wymagają skomplikowanych kodowań lub nietrywialnych stanów początkowych, może nawet być niejasne, czy system jest zdolny do uniwersalnych obliczeń, czy też iluzja uniwersalności powstaje w wyniku czyjejś interpretacji systemu . Na przykład zapoznaj się z dyskusją na liście mailingowej o 2-stanowym, 3-symbolowym urządzeniu Turinga, szczególnie obawach przedstawionych przez Vaughana Pratta.

W każdym razie rozróżnione jest coś takiego jak:

• Rzeczy, które można przedstawić bezpośrednio w systemie, przypisując semantykę do operacji pierwotnych w taki sposób, że operacje koniecznie zachowują semantykę
• Rzeczy, które można przedstawić „pośrednio”, określając procedurę interpretacji wykonywaną poza systemem, przy czym zakłada się, że interpretacja jest „prostsza” niż w pewnym sensie system
• Rzeczy, które można symulować w systemie za pomocą pełnej warstwy pośredniej, na przykład konstruując interpreter dla innego systemu, który zapewnia bezpośrednią reprezentację.

Równoważność Turinga oznacza jedynie, że system spełnia trzecie kryterium dowolnej funkcji obliczeniowej, podczas gdy najczęściej jest to pierwsze kryterium, na którym nam zależy, w formalnym systemie logiki lub języku programowania (niezależnie od tego, w jakim stopniu faktycznie się różnią).

To bardzo nieformalny opis, ale podstawową ideę można doprecyzować. We wspomnianym wątku LtU można znaleźć kilka odniesień do istniejącej pracy według podobnych linii.

Zarówno kombinacyjna logika Schönfinkela, jak i rachunek λ Kościoła zostały początkowo opracowane jako destylowane abstrakcje logicznego rozumowania, i jako takie, ich struktura bardzo starannie odwzorowuje się na logiczne rozumowanie i odwrotnie. Niosą również założenie ekstensywności , takie jak opisane w zasadzie eta-redukcji: λx. f xtam, gdzie xnie występuje f, jest równoważne tylko fsamemu.

W praktyce bardzo ścisłe pojęcie ekstensywności może być zbyt ograniczające, zaś nieograniczona intensywność utrudnia lub uniemożliwia lokalne rozumowanie o podwyrażeniach.

Rachunek SF jest zmodyfikowanym rachunkiem kombinatorycznym, który zapewnia, jako operację pierwotną, ograniczoną formę intensywnej analizy: Zdolność do dekonstrukcji częściowo zastosowanych wyrażeń, ale nie pierwotnych wartości lub wyrażeń nienormalizowanych. Zdarza się to ładnie odwzorować na pomysły, takie jak dopasowanie wzorców, jakie można znaleźć w językach programowania w stylu ML lub makrach, jak w Lisps, ale nie można tego opisać w rachunku SK lub λ bez efektywnego wdrożenia interpretera do oceny terminów „intensywnych”.

Podsumowując: rachunku SF nie można przedstawić bezpośrednio w rachunku λ w tym sensie, że najlepsza możliwa reprezentacja najprawdopodobniej obejmuje implementację interpretera rachunku SF, a przyczyną tego jest zasadnicza różnica semantyczna: czy wyrażenia mają wewnętrzne struktura, czy są one zdefiniowane wyłącznie przez ich zewnętrzne zachowanie?

Rachunek SF Barry'ego Jaya jest w stanie przyjrzeć się strukturze terminów, do których jest stosowany, co jest niefunkcjonalne. Rachunek Lambda i tradycyjna logika kombinacyjna są czysto funkcjonalne i dlatego nie mogą tego zrobić.

Istnieje wiele rozszerzeń rachunku lambda, które robią rzeczy naruszające czystość, z których większość wymaga do pewnego stopnia poprawienia strategii przepisywania, takich jak dodawanie stanu, kontrolki (np. Poprzez kontynuacje) lub zmienne logiczne.