Predykat T Kleene'a

W teorii obliczalności predykat T , po raz pierwszy zbadany przez matematyka Stephena Cole'a Kleene'a , jest szczególnym zbiorem trójek liczb naturalnych , który jest używany do reprezentowania funkcji obliczalnych w formalnych teoriach arytmetyki . Nieformalnie T mówi, czy określony program komputerowy zostanie zatrzymany po uruchomieniu z określonym wejściem, a odpowiadający mu predykat U Funkcja służy do uzyskania wyników obliczeń, jeśli program się zatrzyma. Podobnie jak w przypadku twierdzenia smn _. , oryginalna notacja używana przez Kleene stała się standardową terminologią dla tego pojęcia

Definicja

Przykład wywołania T ₁ . Pierwszy argument podaje kod źródłowy (w C , a nie jako liczba Gödla e ) funkcji obliczalnej, tj. funkcja Collatza f . Drugi argument podaje liczbę naturalną i , do której należy zastosować f . Trzeci argument podaje sekwencję x kroków obliczeniowych symulujących ocenę f na i (jako łańcuch równań, a nie numer porządkowy Gödla). Wywołanie predykatu ma wartość true , ponieważ x jest w rzeczywistości poprawną sekwencją obliczeń dla wywołania f (5) i kończy się wyrażeniem, które nie zawiera już f . Funkcja U zastosowana do sekwencji x zwróci jej końcowe wyrażenie, tj. 1.

Definicja zależy od odpowiedniej numeracji Gödla , która przypisuje liczby naturalne funkcjom obliczalnym (podanym jako maszyny Turinga ). Numeracja ta musi być wystarczająco efektywna, aby przy danym indeksie obliczalnej funkcji i danych wejściowych funkcji można było skutecznie symulować obliczenie funkcji na tym wejściu. Predykat uzyskuje się przez sformalizowanie tej $symulacji$

Relacja trójskładnikowa $_$ _ ${\ Displaystyle T_ {1} (e, i, x)}$ jest prawdziwe, jeśli koduje historię obliczeń funkcji obliczalnej z indeksem $e}$ x $Displaystyle$ uruchomić z wejściem ${\ displaystyle i}$ , a program zatrzymuje się jako ostatni krok tej historii obliczeń. To jest,

${\ Displaystyle T_ {1}}$ najpierw pyta, czy jest liczbą Gödla skończonej sekwencji $⟩ {\ Displaystyle \ langle x_ {j} \ rangle}$ $jot$ kompletnych konfiguracji maszyny Turinga ⟨ z indeksem $}$ uruchamiając obliczenia na wejściu ${\ displaystyle i$ .
Jeśli tak, $każdy$ kolejny element sekwencji odpowiada pojedynczemu krokowi maszyny Turinga
Jeśli tak, $pyta,$ $sekwencja$ kończy maszyny

$jest to$ pytań mają pozytywną odpowiedź, to fałsz

Predykat jest prymitywnie rekurencyjny w tym sensie, że istnieje prymitywna funkcja rekurencyjna, która przy danych wejściowych dla predykatu poprawnie określa wartość logiczną predykatu na tych $danych$

Istnieje $x$ prymitywna $U (x)}$ że $jeśli$ $to$ zwraca wynik funkcji z indeksem $\$ wejściu $displaystyle i}$ .

$formalizm$ Kleene przywiązuje pewną liczbę danych wejściowych do każdej funkcji, predykat być używany tylko w przypadku funkcji, które przyjmują jedno wejście Istnieją dodatkowe predykaty dla funkcji z wieloma danymi wejściowymi; relacja

{\ Displaystyle T_ {k} (e, i_ {1}, \ ldots, i_ {k}, x)}

jest prawdą, jeśli $}$ zatrzymujące się obliczenie funkcji z indeksem $Displaystyle$ wejściach $i_ {1}, \ ldots, i_ {k}$ .

Podobnie jak wszystkie funkcje $} .$ prymitywne rekurencyjne ${1}$ Z tego powodu każda teoria arytmetyki, która jest w stanie przedstawić każdą prymitywną funkcję rekurencyjną, jest w stanie przedstawić i $}$ $\ displaystyle U$ . Przykłady takich teorii arytmetycznych obejmują arytmetykę Robinsona i silniejsze teorie, takie jak arytmetyka Peano .

Twierdzenie o postaci normalnej

Predykaty mogą być użyte do uzyskania twierdzenia Kleene'a o postaci normalnej $dla$ (Soare 1987, s. 15; Kleene 1943, s. 52-53). Oznacza to $}$ że istnieje ustalona funkcja rekurencyjna, taka że funkcja jeśli U $Displaystyle$ i tylko wtedy, gdy istnieje taka liczba, $mi {\ displaystyle e}$ dla wszystkich ${\ Displaystyle n_ {1}, \ ldots, n_ {k}}$ jeden ma

{\ Displaystyle f (n_ {1}, \ ldots, n_ {k}) \ simeq U(\mu x\,T_{k}(e,n_{1},\ldots,n_{k},x))}

,

gdzie μ jest operatorem μ ( ${\ Displaystyle \ mu x \, \ phi (x)}$ jest najmniejszą liczbą naturalną, dla której jest prawdziwa) ${\ Displaystyle \ phi (x)}$ i ${\ displaystyle \ simeq}$ jest prawdziwe, jeśli obie strony są niezdefiniowane lub jeśli obie są zdefiniowane i są równe. Na mocy twierdzenia definicję każdej ogólnej funkcji rekurencyjnej f można przepisać do postaci normalnej, tak że μ operator jest używany tylko raz, a mianowicie. $obliczeniowej$ pod najwyższą $niezależna$ od funkcji .

Hierarchia arytmetyczna

Oprócz kodowania obliczalności predykat T może służyć do generowania pełnych zbiorów w hierarchii arytmetycznej . W szczególności zestaw

{\ Displaystyle K = \ {e {\ mbox {}}: {\ mbox {}} \ istnieje xT_ {1} (e, 0, x) \}}

który ma ten sam stopień Turinga , co problem zatrzymania , jest całkowitą relacją jednoargumentową (Soare 1987, s. 28, $41$ Bardziej ogólnie zestaw

{\ Displaystyle K_ {n + 1} = \ {\ langle e,a_{1},\ldots,a_{n}\rangle :\istnieje xT_{n}(e,a_{1},\ldots,a_{n},x)\}}

jest $+$ ( n ) -ary predykatem. Tak więc $, gdy$ w teorii arytmetyki uzyska się reprezentację predykatu T _{n ,} można z niej uzyskać reprezentację -pełnego

Konstrukcję tę można rozszerzyć wyżej w hierarchii arytmetycznej, jak w twierdzeniu Posta (por. Hinman 2005, s. 397). Na przykład, jeśli zestaw jest kompletny , to $N} ^ {$ $k + 1}}}$ ustawić

{\ Displaystyle \ {\ langle a_ {1}, \ ldots, a_ {k} \ rangle :\forall x(\langle a_{1},\ldots,a_{k},x)\in A)\}}

jest kompletny. ${\ Displaystyle \ Pi _ {n + 1} ^ {0}}$

Notatki

^ Opisany tutaj predykat został przedstawiony w (Kleene 1943) i (Kleene 1952) i jest to zwykle nazywane „ orzeczeniem T Kleene'a ”. (Kleene 1967) używa litery T do opisania innego predykatu związanego z funkcjami obliczalnymi, ale którego nie można użyć do uzyskania twierdzenia Kleene'a o postaci normalnej.

Peter Hinman, 2005, Podstawy logiki matematycznej , AK Peters. ISBN 978-1-56881-262-5
Stephen Cole Kleene (styczeń 1943). „Predykaty rekurencyjne i kwantyfikatory” (PDF) . Transakcje Amerykańskiego Towarzystwa Matematycznego . 53 (1): 41–73. doi : 10.1090/S0002-9947-1943-0007371-8 . Przedruk w The Undecidable , Martin Davis, red., 1965, s. 255–287.
—, 1952, Wprowadzenie do metamatematyki , Holandia Północna. Przedrukowane przez Ishi Press, 2009, ISBN 0-923891-57-9 .
—, 1967. Logika matematyczna, John Wiley. Przedrukowane przez Dover, 2001, ISBN 0-486-42533-9 .
Robert I. Soare , 1987, Rekurencyjnie wyliczalne zbiory i stopnie, Perspektywy w logice matematycznej, Springer. ISBN 0-387-15299-7

[1] Opisany tutaj predykat został przedstawiony w (Kleene 1943) i (Kleene 1952) i jest to zwykle nazywane „ orzeczeniem T Kleene'a ”. (Kleene 1967) używa litery T do opisania innego predykatu związanego z funkcjami obliczalnymi, ale którego nie można użyć do uzyskania twierdzenia Kleene'a o postaci normalnej.