Czy klasa prymitywnych funkcjonałów rekurencyjnych jest równoważna z klasą funkcji, które płód kończy?

Płód, jeśli o nim nie słyszałeś, możesz przeczytać tutaj . Wykorzystuje system „macierzy wywołań” i „grafów wywołań”, aby znaleźć wszystkie „zachowania rekurencyjne” wywołań rekurencyjnych w funkcji. Pokazanie, że funkcja się kończy, pokazuje, że wszystkie zachowania rekurencyjne wywołań rekurencyjnych wykonanych do funkcji są zgodne z pewnym „porządkiem leksykograficznym”. Jego sprawdzanie zakończenia pozwala na wszystkie prymitywne funkcje rekurencyjne i funkcje, takie jak funkcja Ackermanna. Zasadniczo umożliwia wielokrotną argumentację prymitywnej rekurencji. Jest to również w zasadzie kontroler terminacji Agdy; Uważam, że Coq ma również podobne funkcje, choć może bardziej ogólne.

Po przeczytaniu artykułu „Total Functional Programming” DA Turnera . Wyjaśnia, że ​​jego proponowany język byłby w stanie wyrazić wszystkie „prymitywne funkcjonały rekurencyjne”, jak widać w Systemie T zbadanym przez Godela. Mówi dalej, że ten system „znany jest z tego, że obejmuje każdą funkcję rekurencyjną, której całość można udowodnić za pomocą logiki pierwszego rzędu”.

Dawka płodu pozwala wszystkim prymitywnym funkcjom rekurencyjnym? Jeśli tak, to czy pozwala na funkcje, które nie są prymitywnymi funkcjami rekurencyjnymi? Czy można podać cytat z odpowiedzią na to pytanie? (nie jest to tak naprawdę konieczne, ponieważ jestem po prostu zainteresowany; po prostu fajne byłoby czytanie małżeństwa w tej sprawie)

Pytanie dodatkowe: pierwotne funkcje funkcjonalne rekurencyjne mają bardzo zwięzłą definicję w odniesieniu do kombinacji: wpisane S i K (które nie mogą wyrazić kombinatory punktu stałego), zero, funkcja następcy i funkcja iteracji; Otóż ​​to. Czy istnieją inne bardziej ogólne takie języki, które mają tak zwięzłą definicję i w których kończą się wszystkie wyrażenia?

Tak, kontroler płodu może sprawdzać wszystko w Goedel's T. Możesz to pokazać za pomocą kontrolera, aby pokazać, że operator iteracji w T się kończy. Na przykład zadziała następująca definicja:

$$\begin{array}{lcl} \mathit{iter} & : & A \to (A \to A) \to \mathbb{N} \to A \\ \mathit{iter} \;i \;f \;0 & = & i \\ \mathit{iter} \;i \;f \;(n+1) & = & f\;(\mathit{iter} \;i \;f \;n) \end{array}$$

Jest to bardzo łatwe do sprawdzenia dla kontrolera płodu (lub większości innych kontrolerów terminacji), ponieważ jest to oczywiście strukturalnie rekurencyjna definicja.

Zarówno Agda, jak i Coq zezwalają na potwierdzenie zakończenia funkcji, które wykraczają daleko poza to, co jest możliwe do udowodnienia, w przypadku arytmetyki pierwszego rzędu. Funkcja, która to umożliwia, polega na tym, że pozwalają one definiować typy poprzez rekurencję danych, co nazywa się „dużą eliminacją”. (W teorii zbiorów ZF schemat zastępowania aksjomat służy mniej więcej temu samemu celowi).

Prostym przykładem czegoś, co wykracza poza T, jest spójność samej T Goedela! Możemy podać składnię jako typ danych:

data T : Set where 
   N : T 
   _⇒_ : T → T → T

data Term : T → Set where 
   zero : Term N
   succ : Term (N ⇒ N)
   k    : {A B : T} → Term (A ⇒ B ⇒ A)
   s    : {A B C : T} → Term ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C)
   r    : {A : T} → Term (A ⇒ (A ⇒ A) ⇒ N ⇒ A)
   _·_  : {A B : T} → Term (A ⇒ B) → Term A → Term B

Zauważ, że zależność typów pozwala nam zdefiniować typ danych terminów zawierających tylko dobrze wpisane terminy T. Możemy wtedy dać funkcję interpretacji dla typów:

interp-T : T → Set 
interp-T N       = Nat 
interp-T (A ⇒ B) = (interp-T A) → (interp-T B)

To mówi, że Npowinny to być liczby naturalne Agdy, a strzałkę T należy interpretować jako przestrzeń funkcji Agdy. Jest to „duża” eliminacja, ponieważ definiujemy zestaw przez rekurencję w strukturze typu danych T.

Następnie możemy zdefiniować funkcję interpretacji, pokazując, że każdy termin T Goedela można interpretować terminem Agda:

interp-term : {A : T} → Term A → interp-T A
interp-term zero    = 0 
interp-term succ    = \n → n + 1
interp-term k       = \x y → x
interp-term s       = \x y z → x z (y z)
interp-term r       = Data.Nat.fold 
interp-term (f · t) = (interp-term f) (interp-term t)

(Nie mam Agdy na tym komputerze, więc niewątpliwie brakuje niektórych importów, deklaracji poprawności i literówek. Naprawianie to ćwiczenie dla czytelnika, który może być także redaktorem, jeśli im się podoba).

Nie wiem, jaka jest siła konsystencji Agdy, ale Benjamin Werner wykazał, że Rachunek Konstrukcji Indukcyjnych (rachunek jądra Coqa) jest zgodny z ZFC i niezliczoną liczbą niedostępnych kardynałów.

W ramach wyjaśnienia powinienem zauważyć, że płód jest opracowywany przez Andreasa Abla , który opracował również oryginalny program sprawdzający zakończenie dla Agdy i od tego czasu pracował nad bardziej zaawansowanymi technikami przerywania .

Odpowiedź na twoje pytanie może być nieco rozczarowująca: klasa funkcji $\mathbb{N}$ do $\mathbb{N}$to dokładnie funkcje, które można zdefiniować w systemie$\mathrm{F}$. Powód tego: wspomniana klasa jest równa możliwym do udowodnienia funkcji kończącej w arytmetyki drugiego rzędu ($\mathrm{PA}^2$), co z kolei jest równe funkcjom definiowanym w systemie $\mathrm F$(patrz np. Dowody i typy , rozdział 11). Ponadto, jeśli usuniesz polimorfizm, wówczas upadasz do funkcji definiowanych w$\mathrm{PA}$, które zdarza się zbieżne z tymi, które można zdefiniować w systemie $\mathrm{T}$.

Ponownie, powodem tego jest to, że spadek wychwycony przez „matryce wywoływania” jest udowodniony , i że dowód ten można przeprowadzić całkowicie w$\mathrm{PA}$.

Nie oznacza to jednak, że płód nie jest bardziej przydatny niż system$\mathrm{T}$! W praktyce wymagane są bardziej złożone analizy terminacji, aby móc zaakceptować niektóre prezentacje funkcji obliczeniowych. Nie musisz na przykład wykonywać skomplikowanego dowodu w arytmetyki Peano za każdym razem, gdy piszesz funkcję unifikacyjną. Pod tym względem płód jest bardzo potężny i pozwala definiować funkcje w sposób, który nie byłby akceptowany przez Coq, Agda ani żaden inny powszechny system dowodowy.

Jeśli przez prymitywne funkcjonały rekurencyjne masz na myśli prymitywne funkcje rekurencyjne i wiesz, że płód zawiera funkcję Ackermanna, wówczas płód nie pokrywa się z klasą funkcji pr, ponieważ funkcja Ackermanna nie jest pierwotną rekurencyjną. Zostało to pokazane przez Ackermanna, a później uproszczony dowód przedstawił Rosza Peter w „ Konstruktion nichtrekursiver Funktionen ” 1935 (niestety, o ile wiem, tylko w języku niemieckim).

Jeśli szukasz większych klas funkcji rekurencyjnych, które mają zagwarantowane zakończenie, które mogą zbiegać się z klasą funkcji przechwyconych przez Płód, to może zainteresować Cię inne dzieło Roszy Peter.

Funkcja Ackermanna jest zawarta w klasie wielu funkcji rekurencyjnych zdefiniowanych przez Roszy Peter w „ Uber die mehrfache Rekursion ” 1937. Nieoficjalnie idea wielokrotnej rekurencji polega na tym, że możesz mieć wiele zmiennych rekurencyjnych, które mogą się zmieniać po kroku rekurencyjnym. Na przykład$f(a,b)$ może zadzwonić $f(a,b-1)$ lub $f(a-1,b)$.

Jednak silniejszą klasę stanowi koncepcja rekurencji transfinitowej opisana w „ Zusammenhang der mehrfachen und transfiniten Rekursion ” Roszy Peter. W przypadku rekurencji transfinitowej masz jedną zmienną rekurencyjną, która może wywoływać poprzedników wrt na specjalne zamówienie$<$

Na przykład można zinterpretować liczbę całkowitą jako parę liczb całkowitych i użyć kolejności

$$(a,b) < (c,d) \iff ( a < c \wedge b \leq d ) \vee ( a \leq c \wedge b < d )$$ Można to uogólnić dla potrójnych liczb całkowitych i tak dalej. Piotr nazywa te porządki$\omega^2, \omega^3$i tak dalej. Możesz pójść o krok dalej i zinterpretować liczbę całkowitą jako dowolną liczbę całkowitą. Pozwolić$p_i$ być $i$-ta liczba pierwsza. Następnie możemy rozważyć$z = p_1^{n} \cdot p_2^{x_1} \cdot p_3^{x_2} \cdot \dots$ gdzie $n$ oznacza liczbę liczb całkowitych zakodowanych w $z$ i $x_i$zawierają odpowiednio. wartość. Oznacza porządek dla takiej liczby liczb całkowitych jak$\omega^\omega$i pokazuje po przekątnej, że tego rodzaju rekurencja jest silniejsza niż wielokrotna rekurencja. Nie jestem jednak pewien, czy istnieje charakterystyka składniowa tej klasy.

[edytuj] Pierwotne funkcje rekurencyjne nie są takie same jak pierwotne funkcje rekurencyjne, jak zauważono w komentarzu poniżej. Myślę jednak, że można przenieść koncepcję rekurencji transfinitowej na funkcjonały. Jednak nie jest jasne, czy nadal ma większą moc w stosunku do ustawienia funkcjonalnego.