Czy istnieje typowany rachunek lambda, który jest spójny i kompletny Turinga?

Czy istnieje typowany rachunek lambda, w którym odpowiednia logika w korespondencji Curry-Howarda jest spójna i gdzie istnieją możliwe do wpisania wyrażenia lambda dla każdej funkcji obliczeniowej?

Jest to wprawdzie pytanie nieprecyzyjne, pozbawione precyzyjnej definicji „typowanego rachunku lambda”. Zastanawiam się, czy istnieją (a) znane przykłady tego, lub (b) znane dowody niemożności dla czegoś w tej dziedzinie.

Edycja: @cody podaje dokładną wersję tego pytania w swojej odpowiedzi poniżej: czy istnieje logiczny system czystego typu (LPTS), który jest spójny i Turinga kompletny (w sensie zdefiniowanym poniżej)?

type-theory lambda-calculus typed-lambda-calculus curry-howard Morgan Thomas
źródło

Nie ma rachunku rekurencyjnie aksjomatyzowalnego (lambda lub inny), którego wszystkie możliwe do udowodnienia funkcje rekurencyjne są funkcjami rekurencyjnymi, więc rachunek musiałby obejmować wyrażenia nie kończące się.

Emil Jeřábek wspiera Monikę

Ta odpowiedź jest twierdzenie, które mówi, że nie można mieć żadnego rodzaju rachunku, który jest zarówno Turing-zupełny i całkowity.

Andrej Bauer,

Prawdopodobnie odpowie na twoje pytanie, gdy uczynisz je wystarczająco precyzyjnym. Myślę, że dowód Andreja jest niepotrzebnie skomplikowany (ale pokazuje więcej): chodzi o to, że gdyby istniał skutecznie opisany system, w którym wszystkie funkcje rekurencyjne byłyby reprezentowalne w taki sposób, że można syntaktycznie poświadczyć, że wyrażenie jest uczciwą reprezentacją funkcja rekurencyjna (np. przez sprawdzenie, czy jest poprawnie wpisana w systemie), wtedy uzyskasz uniwersalną całkowitą funkcję rekurencyjną, co jest niemożliwe.

Emil Jeřábek wspiera Monikę

Oczywiście klasyczną odpowiedzią na tego rodzaju pytanie może być: typ

rachunek z typami przecięć , ponieważ wpisuje on wszystkie (i tylko te) terminy, które są silnie normalizujące. Jest to raczej filozoficzne pytanie, czy rachunek dopuszcza „interpretację Curry-Howarda”.

λ

$\lambda$

cody

Trudno tu być bardziej precyzyjnym, ponieważ pytanie nie jest precyzyjne.

Andrej Bauer,

Odpowiedzi:

W porządku, poddam się temu: ogólnie dla danego systemu typów , prawda jest następująca: $T$

Jeśli wszystkie dobrze wpisane terminy w rachunku normalizują się, wówczas jest spójne, gdy jest postrzegane jako logika. $T$ $T$

Dowodem na ogół prowadzi się przy założeniu, że trzeba termin typu , poprzez redukcję z zastrzeżeniem uzyskania postaci normalnej, a następnie przebiega przez indukcję o strukturze takiej perspektywie się sprzeczność. $\mathrm{absurd}$ $\mathrm{False}$

Naturalne jest zastanawianie się, czy rozmowa się utrzymuje, tj

Dla dowolnego systemu typu , jeśli jest logicznie spójny , to każdy dobrze wpisany termin w jest normalizujący. $T$ $T$ $T$

Problem polega na tym, że nie ma tak naprawdę najbardziej ogólnego pojęcia „systemu typów”, a tym bardziej nie jest zgodna co do znaczenia logicznej spójności dla takich systemów. Możemy jednak empirycznie to zweryfikować

W przypadku większości znanych systemów typu, które mają logiczną interpretację, odwrotność rzeczywiście się sprawdza.

W jaki sposób łączy się to z Turing Completeness? Cóż, po pierwsze, jeśli sprawdzanie typu jest rozstrzygalne , to argument Andreja pokazuje, że jedno z poniższych musi być spełnione :

Zestaw wszystkich dobrze napisanych programów nie jest Turing Complete.
Istnieje nie kończący się dobrze napisany program.

Sugeruje to, że:

Systemy typów, które mają logiczną interpretację i są spójne i są rekurencyjnie wyliczalne, nie są Turing Complete.

Podanie faktycznego twierdzenia zamiast sugestii wymaga doprecyzowania matematycznego pojęcia systemów typów i interpretacji logicznych.

Teraz przychodzą mi na myśl dwie uwagi:

Istnieje nierozstrzygalny system typów, system typów skrzyżowań, który ma logiczną interpretację i może reprezentować każdy normalizujący termin . Jak zauważyłeś, nie jest to dokładnie to samo, co ukończenie Turinga, ponieważ typ funkcji totalnej może wymagać aktualizacji (dopracowania) przed zastosowaniem jej do żądanego argumentu. Rachunek ten jest rachunkiem „w stylu curry'ego” i jest równy STLC + $\lambda$ i
$\frac{Γ ⊢ M. : τ Γ ⊢ M. : σ}{Γ ⊢ M. : τ \cap σ}$ $\frac{\Gamma\vdash M:\tau\quad \Gamma\vdash M:\sigma}{\Gamma\vdash M:\tau\cap\sigma}$ Oczywiste jest, że „interpretacja”prowadzi do spójnej interpretacji logicznej. $\frac{Γ ⊢ M. : τ \cap σ}{Γ ⊢ M. : τ} \frac{Γ ⊢ M. : τ \cap σ}{Γ ⊢ M. : σ}$ $\frac{\Gamma\vdash M:\tau\cap\sigma}{\Gamma\vdash M:\tau}\quad \frac{\Gamma\vdash M:\tau\cap\sigma}{\Gamma\vdash M:\sigma}$ $\cap=\wedge$
Istnieje klasa systemów typów, Pure Type Systems , w których takie pytanie można by sprecyzować. W tych ramach logiczna interpretacja jest jednak mniej jasna. Można pokusić się o stwierdzenie: „PTS jest spójny, jeśli ma niezamieszkany typ”. Ale to nie działa, ponieważ typy mogą żyć w różnych „wszechświatach”, gdzie niektóre mogą być spójne, a inne nie. Coquand i Herbelin definiują pojęcie logicznych systemów typu czystego , w którym pytanie ma sens i pokazują

Każdy niespójny, niezależny LPTS ma kombinator pętli (podobnie jak Turing Complete)

Który odpowiada na pytanie w jednym kierunku (niespójne TC) w tym przypadku. O ile mi wiadomo, pytanie dotyczące ogólnego LPTS jest nadal otwarte i dość trudne. $\Rightarrow$

Edycja: Odwrotność wyniku Coquand-Herbelin nie jest tak łatwa, jak myślałem! Oto, co do tej pory wymyśliłem.

Logiczny Czysty Typ systemu jest PTS z (co najmniej) rodzaje i (co najmniej) Aksjomat i (przynajmniej) zasada , z dalszym wymogiem, że nie ma rodzajów . $\mathrm{Prop}$ $\mathrm{Type}$ $\mathrm{Prop}:\mathrm{Type}$ $(\mathrm{Prop},\mathrm{Prop},\mathrm{Prop})$ $\mathrm{Prop}$

Teraz przyjmuję szczególne stwierdzenie o kompletności Turinga: napraw LPTS i niech będzie kontekstem $L$ $\Gamma$

Γ = n a t : P r o p, 0 : n a t, S : n a t \to n a t

$\Gamma = \mathrm{nat}:\mathrm{Prop},\ 0:\mathrm{nat},\ S:\mathrm{nat}\rightarrow \mathrm{nat}$

oznaczaTuringa Całkowiteiff dla każdej całkowitej obliczalnej funkcji istnieje termin taki, że i dla każdego $L$ $f:\mathbb{N}\rightarrow\mathbb{N}$ $t_f$

Γ ⊢ t_{f} : n a t \to n a t

$\Gamma \vdash t_f : \mathrm{nat}\rightarrow \mathrm{nat}$

n \in N

$n\in\mathbb{N}$

t_{fa} ({S.}^{n} 0) \to_{β}^{*} {S.}^{fa (n)} 0

$t_f\ (S^n\ 0)\rightarrow^*_{\beta} S^{f(n)}\ 0$

Argument diagonalizacji Andreja pokazuje teraz, że nie ma końcówki typu $t$ $\mathrm{nat}$ .

Teraz wydaje się, że jesteśmy w połowie drogi! Biorąc pod uwagę nie kończący się termin , chcemy zastąpić wystąpienia jakimś ogólnym typem i pozbyć się i w , i będziemy mieć naszą niespójność ( jest zamieszkały w kontekście $\Gamma \vdash \mathrm{loop}:\mathrm{nat}$ $\mathrm{nat}$ $A$ $0$ $S$ $\Gamma$ $A$ $A:\mathrm{Prop}$ )!

Niestety utknąłem w tym miejscu, ponieważ łatwo jest zastąpić literę tożsamością, ale jest znacznie trudniejsze do usunięcia. Idealnie chcielibyśmy skorzystać z jakiegoś twierdzenia o rekurencji Kleene'a, ale jeszcze tego nie rozgryzłem. $S$ $0$

cody
źródło

OK, więc pierwsze dwa wyjaśnienia dotyczące twojej uwagi (1). Co masz na myśli mówiąc, że ten system typów skrzyżowań nie jest wymienny rekurencyjnie? Z pewnością zbiór twierdzeń systemu jest ponownie, ponieważ podałeś go jako prosty rachunek sekwencyjny. Ponadto wynik, który, jak udowodniłem, w powiązanym dokumencie jest taki, że terminy, które można wpisać w systemie, są dokładnie terminami silnie normalizującymi; ale czy to nie różni się od stwierdzenia, że może wpisać dokładnie całkowitą liczbę funkcji obliczalnych? Np. Nie jest

silnie normalizująca, ale nie całkowita?

λ x . x x

$\lambda x. xx$

Morgan Thomas

Teraz pytanie o twoją uwagę (2). Wydaje mi się, że cytowane przez ciebie twierdzenie nie jest tym, czym jesteśmy zainteresowani. Mówi ono, że dla każdego niezależnego LPTS, jeśli jest niespójny, to Turing jest kompletny. Ale chcielibyśmy wiedzieć, czy dla każdego LPTS, jeśli Turing jest kompletny, to jest niespójny. Czy coś tu nie rozumiem?

Morgan Thomas

@MorganThomas: Ach, masz rację co do pierwszego punktu: chciałem powiedzieć, że system typów nie może być rozstrzygalny , to znaczy, biorąc pod uwagę

, zdanie

jest nierozstrzygalne. Poprawię to w poście.

Γ, t, A

$\Gamma, t, A$

Γ ⊢ t : A

$\Gamma\vdash t:A$

cody

Drugi punkt: masz również rację, że można mieć niecałkowitą funkcję, która jest dobrze napisana (chociaż niekoniecznie można zastosować ją do danego argumentu). Poprawię odpowiedź.

cody

Trzeci punkt Znowu masz rację! Jednak odwrotna sytuacja (w szczególnym przypadku LPTS) jest dość trywialna. Przedstawię argument.

cody

Oto odpowiedź na wariant precyzji @ cody mojego pytania. Istnieje spójny LPTS, który Turing kończy w sensie z grubsza @ cody, jeśli pozwolimy na wprowadzenie dodatkowych aksjomatów i reguł redukcji . Zatem ściśle mówiąc, system nie jest LPTS; jest to po prostu coś w rodzaju jednego. $\beta$

Zastanów się nad rachunkiem konstrukcji (lub swoim ulubionym członkiem kostki ). To jest LPTS, ale dodamy dodatkowe rzeczy, które sprawiają, że nie jest to LPTS. Wybierz stałe symbole i dodaj aksjomaty: $\lambda$ $\text{nat}, 0, S$

⊢ nat : *

$\vdash \text{nat} : \ast$

⊢ 0 : nat

$\vdash 0 : \text{nat}$

⊢ S : nat \to nat

$\vdash S : \text{nat} \to \text{nat}$

Indeks Turinga programy maszynowe według liczb naturalnych, a dla każdej liczby naturalnej wybrać symbol stałej , dodać aksjomat , a dla wszystkich , dodaj regułę -redukcja $e$ $f_e$ $f_e : \text{nat} \to \text{nat}$ $e,x \in \mathbb{N}$ $\beta$

f_{e} (x) \to_{β} Φ_{e} (x),

$f_e(x) \to_\beta \Phi_e(x),$

gdzie normalnie ma wyjście XX Turingowi programu maszyny o . Jeśli różni się wówczas reguła ta nie robi nic. Zauważ, że dodając te aksjomaty i reguły, twierdzenia systemu pozostają rekurencyjnie policzalne, chociaż jego zestaw reguł redukcji nie jest już rozstrzygalny, a jedynie rekurencyjnie policzalny. Wierzę, że moglibyśmy z łatwością zachować zestaw $\Phi_e(x)$ $e$ $x$ $\Phi_e(x)$ $\beta$ $\beta$ porządku reguł redukcji poprzez wyraźne określenie szczegółów modelu obliczeniowego w składni i regułach systemu.

Teraz teoria ta jest całkowicie ukończona w sensie z grubsza @ cody, tylko brutalną siłą; ale twierdzenie jest takie, że jest również spójne. Stwórzmy jego model.

Niech będą trzema zestawami, takimi, że: $U_1 \in U_2 \in U_3$

(gdzie $\emptyset, \mathbb{N}, 0, S \in U_1$ $S$ jest funkcją następczą).
Każdy zestaw jest przechodni; jeśli , to $a \in b \in U_i$ $a \in U_i$ .
Każdy zestaw jest zamknięty pod tworzeniem przestrzeni funkcyjnych; tj. jeśli , to $A, B \in U_i$ $B^A \in U_i$ .
$A \in U_i$ $f : A \to U_i$ $\prod_{a \in A} f(a) \in U_i$

$U_i$

$v$ $U_2$ $v$ $I_v$

$I_v(x) = v(x)$ $x$
$I_v(\ast) = U_1, I_v(\Box) = U_2$
$I_v(\text{nat}) = \mathbb{N}, I_v(0) = 0, I_v(S) = S$
$I_v(f_e) = \Phi_e$ $\mathbb{N} \to \mathbb{N}$ $e$
$I_v(AB) = I_v(A)(I_v(B))$ $I_v(A)$ $I_v(B)$ $I_v(AB) = 0$
$I_v(\lambda x : A. B)$ $a \in I_v(A)$ $I_{v[x:=a]}(B)$
$I_v(\Pi x : A. B) = \prod_{a \in I_v(A)} I_{v[x:=a]}(B)$

$A$ $I_v(A) \in U_3$ $v$ $A : B$ $v \models A : B$ , gdyby $I_v(A) \in I_v(B)$ . Mówimy tak $\Gamma \models A : B$ jeśli dla wszystkich interpretacji $v$ , gdyby $v \models x : C$ dla wszystkich $(x : C) \in \Gamma$ , następnie $v \models A : B$ .

Łatwo jest sprawdzić, czy $\Gamma \vdash A : B$ , następnie $\Gamma \models A : B$ , więc jest to model systemu. Ale dla dowolnych zmiennych $x,y$ , tak nie jest $y : \ast \models x : y$ , ponieważ możemy interpretować $y$ przez $\emptyset$ , więc system jest spójny.

To jest odpowiedź na moje pierwotne pytanie, w tym sensie, że rozsądnie jest nazywać kalulus na maszynie, który jest spójny i Turinga kompletny. Nie jest to jednak odpowiedź na pytanie @ cody, ponieważ nie jest to LPTS, ponieważ dodano dodatkowe aksjomaty i $\beta$ zasady redukcji. Wyobrażam sobie, że odpowiedź na pytanie @ cody jest znacznie trudniejsza.

Morgan Thomas
źródło

To ładna odpowiedź, ale nie jestem pewien, czy musisz przejść przez wszystkie te ćwiczenia gimnastyczne, aby udowodnić spójność: określenie typu

A

$A$ w pustym kontekście może być „odsłodzony” do terminu w CoC: zadzwonię na

f_{e} (x) \to Φ_{e} (x)

$f_e(x)\rightarrow \Phi_e(x)$ zasady $\iota$ - rządzi i utrzymuje

β

$\beta$ dla zwykłych. Wykonaj wszystko

β

$\beta$ -redukcje (kończy się, ponieważ dodano tylko stałe) i zastępuje każdy termin formularza

f_{e} (x)

$f_e(x)$ przez jego redukcję, jeśli ma taką . Chodzi o to, że

ι

$\iota$ -zasady działają tylko na zasadach naziemnych, więc możesz zrobić wszystko

β

$\beta$ - najpierw obniżki, aby usunąć je z drogi.

cody

Myślę, że masz rację. To nie jest moja dziedzina, więc jestem trochę niezdarny. :-) Myślę, że twój dowód działa, a jedną ciekawą konsekwencją, jeśli mam rację, jest to, że ta teoria nie ma zbyt dużej siły spójności. Wygląda jak potencjalnie bardzo potężna teoria, ponieważ ma typy i liczby naturalne, co powinno pozwolić ci zinterpretować teorię mnogości; ale najwyraźniej nie możesz, ponieważ możesz udowodnić, że jest spójny bez użycia potężnej teorii mnogości!

Morgan Thomas