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).