Jak sprawić, by rachunek Lambda był silny normalizujący bez systemu typów?

Czy jest jakiś system podobny do rachunku lambda, który silnie się normalizuje, bez potrzeby dodawania na nim systemu typów?

Mogę wymyślić kilka możliwych odpowiedzi pochodzących z logiki liniowej.

Najprostszym jest afiniczny rachunek lambda: rozważ tylko te wyrażenia lambda, w których każda zmienna pojawia się najwyżej. Warunek ten jest zachowany przez redukcję i natychmiast widać, że rozmiar warunków afinicznych ściśle maleje z każdym krokiem redukcji. Dlatego niepisany afiniczny rachunek lambda silnie się normalizuje.

Bardziej interesujące przykłady (pod względem ekspresji) podane są przez tak zwane „lekkie” rachunki lambda, wynikające z podsystemów logiki liniowej wprowadzonej przez Girarda w „Lekkiej logice liniowej” (informacja i obliczenia 143, 1998), a także jako „Soft Linear Logic” Lafonta (Theoretical Computer Science 318, 2004). W literaturze istnieje kilka takich kamieni, być może dobrym odniesieniem jest „Rachunek lambda lambda afinicznego i silna normalizacja czasu wielomianowego” (Archive for Mathematical Logic 46, 2007). W tym artykule Terui definiuje rachunek lambda pochodzący od logiki afinicznej światła i wykazuje dla niego silny wynik normalizacji. Mimo że w artykule wymieniono typy, nie są one wykorzystywane w dowodzie normalizacji. Przydają się one do starannego sformułowania głównej właściwości lekkiego rachunku lambda afinicznego, a mianowicie do tego, że terminy określonego typu dokładnie reprezentują funkcje czasu politycznego. Podobne wyniki są znane z obliczeń elementarnych z wykorzystaniem innych „lekkich” obliczeń lambda (praca Terui zawiera dalsze odniesienia).

Na marginesie warto zauważyć, że w rachunku teoretycznym afiniczny rachunek lambda odpowiada logice intuicyjnej bez reguły skurczu. Grishin zauważył (przed wprowadzeniem logiki liniowej), że przy braku skurczu naiwna teoria mnogości (tj. Z nieograniczonym zrozumieniem) jest spójna (tj. Paradoks Russela nie daje sprzeczności). Powodem jest to, że eliminacja cięć w naiwnej teorii zbiorów bez skurczu może być udowodniona przez prosty argument zmniejszający rozmiar (jak ten, który podałem powyżej), który nie opiera się na złożoności formuł. Poprzez korespondencję Curry-Howarda jest to dokładnie normalizacja niepisanego afinicznego rachunku lambda. Dokonuje się to poprzez przetłumaczenie paradoksu Russela w logice liniowej i „dopracowanie” metody wykładnicze, aby nie można było ustalić sprzeczności, że Girard wymyślił lekką logikę liniową. Jak wspomniałem powyżej, w kategoriach obliczeniowych lekka logika liniowa daje charakterystykę funkcji obliczalnych w czasie wielomianowym. W teorii teoretycznej spójną naiwną teorię zbiorów można zdefiniować w lekkiej logice liniowej, tak że możliwe do udowodnienia funkcje całkowite są dokładnie funkcjami obliczalnymi w czasie wielomianowym (jest jeszcze inny artykuł autorstwa Terui na temat: „Teoria zbiorów afinicznych światła: Naiwny ustaw teorię czasu wielomianowego ”, Studia Logica 77, 2004).

Oryginalny artykuł Church and Rosser, „Some Properties of Conversion”, opisuje coś, co może być przykładem tego, czego szukasz.

Jeśli używasz ścisłego rachunku lambda, gdzie w każdym przypadku$\lambda x.M$ masz to $x$ pojawia się za darmo w $M$, a następnie bez systemu typów zachowana jest następująca właściwość (to Twierdzenie 2 w pracy Churcha i Rossera):

Gdyby $B$ jest normalną formą $A$, to jest liczba $m$ tak, że jakakolwiek sekwencja redukcji zaczyna się od $A$ zaprowadzi do $B$ [równoważność modulo alfa] co najwyżej $m$ redukcje.

Tak więc, nawet jeśli możesz pisać terminy nie kończące się w (niepisanym) ścisłym rachunku lambda, każdy termin o normalnej formie silnie normalizuje się; to znaczy, każda sekwencja redukcji osiągnie tę unikalną normalną formę.

Oto zabawna, autorstwa Neila Jonesa i Niny Bohr:

Zakończenie połączenia według wartości w Untyped $\lambda$-rachunek różniczkowy

Pokazuje, jak zastosować analizę zmiany wielkości (rodzaj analizy przepływu sterowania wykrywającej nieskończone pętle) na nietypowym$\lambda$-warunki. W praktyce jest to całkiem miłe, ale oczywiście ograniczone$\lambda$-termy bez zdefiniowanych stałych (choć metoda może zostać rozszerzona na bardziej ogólne zastosowanie).

Zaletą pisania jest oczywiście zarówno niski koszt złożoności, jak i modułowość podejścia: ogólnie analizy zakończenia są bardzo niemodularne, ale pisanie może być wykonywane „kawałek po kawałku”.