Jeśli abstrakcyjna maszyna może się symulować, czy to czyni Turinga kompletnym?

Na przykład w językach programowania często pisze się kompilator / interpreter X-w-X, ale na bardziej ogólnym poziomie wiele znanych systemów Turing-complete może symulować się w imponujący sposób (np. Symulując grę życia Conwaya w grze życia Conwaya ).

Moje pytanie brzmi zatem: czy system jest w stanie samodzielnie przeprowadzić symulację, aby udowodnić, że Turing jest gotowy? Z pewnością jest to warunek konieczny.

Niekoniecznie. Na przykład dwuwymiarowy blokowy automat komórkowy z dwoma stanami, w którym komórka staje się żywa tylko wtedy, gdy jej czterej poprzednicy mają dokładnie dwa sąsiednie żywe komórki, może symulować się ze współczynnikiem dwóch spowolnień i współczynnikiem powiększenia o dwóch rozmiarach, ale nie jest znane jako ukończenie Turinga. Więcej informacji na temat tego automatu blokowego oraz zasady B36 / S125 dla sąsiedztwa Moore, który jest w stanie symulować ten automat blokowy, można także znaleźć w Nathaniel Johnston B36 / S125 „2x2” Life-Like Cellular Automaton .

Nie, nie jest. Znam dwie główne klasy technik unikania niespójności / kompletności Turinga.

1. Pierwszą linią ataku jest skonfigurowanie systemu tak, aby składnia mogła być arytmetyczna, ale twierdzenie Godela o stałym punkcie nie przechodzi. Dan Willard intensywnie nad tym pracował i zapewnił spójne, samoregulujące systemy logiczne. Sztuką jest wyeliminowanie symboli funkcji mnożenia i dodawania oraz zastąpienie ich podzielnością i odejmowaniem. Daje to wystarczającą moc do arytmetycznego przedstawienia składni, ale twierdzenie o stałym punkcie nie przechodzi, ponieważ mnożenie nie jest możliwe do udowodnienia.

   Zobacz Dan Willard. Samo-weryfikujące się systemy aksjomatów, twierdzenie o niekompletności i pokrewne zasady refleksji . Journal of Symbolic Logic 66 (2001) str. 536-596.

2. Druga linia ataku pozwala na większe wykorzystanie ustalonych punktów, ale aby ustawić rzeczy tak, aby składnia nie była arytmetyczna. Najładniejsze systemy do tego celu to (IMO) oparte na wariantach logiki liniowej. Na przykład, w teorii afinicznych zestawów lekkich Kazushige Terui nawet pełna, nieograniczona zasada rozumienia zbioru jest zdrowa, ale ponieważ logika otoczenia teorii zbiorów jest liniowa (a zatem skurcz nie jest dozwolony), paradoks Russella nie jest możliwy do wyprowadzenia.

   Intuicyjnym powodem niepowodzenia arytmetyki jest to, że lekka liniowa przestrzeń funkcji jest tak ustawiona, że ​​wszyscy jej mieszkańcy są wielomianami. W rezultacie lekka liniowa wersja aksjomatów Peano nie może udowodnić całkowitego potęgowania (ponieważ potęgowanie liczb jednostkowych zajmuje czas wykładniczy), a zatem nie ma już izomorfizmu między liczbami naturalnymi a łańcuchami bitów.$A \multimap B$

   Kazushige Terui. Teoria zbiorów afinicznych światła: naiwna teoria zbiorów czasu wielomianowego. Studia Logica, vol. 77, nr 1, s. 9–40, 2004.

   Myślę, że ten artykuł jest bardziej dostępny po przeczytaniu następującego artykułu Yvesa Lafonta:

   Y. Lafont, Miękka logika liniowa i czas wielomianowy , Informatyka teoretyczna 318 (wydanie specjalne na temat niejawnej złożoności obliczeniowej) str. 163-180, Elsevier (2004)

   Teoria mnogości Terui jest bardzo ekspresyjna, ale trudno ją porównać z tradycyjnymi teoriami mnogości, ponieważ teorie teoretyczne nie są dobrym narzędziem do porównywania bardzo słabych układów. Na przykład teoria mnogości Terui'ego oczywiście nie może udowodnić całkowitego potęgowania, a zatem jej siła teoretyczna nie może sięgać nawet . Klasy złożoności są prawdopodobnie lepsze - są kompletne dla czasu politytime (może udowodnić, że każda funkcja polytime jest całkowita, ale nie więcej).$\omega$

   Często myślę o tego rodzaju systemach jako dowodach koncepcji, że teoria złożoności może służyć jako podstawa dla niektórych rodzajów ultrafinityzmu.

Rozważ następujący model maszyny. Maszyna z kodem , na wejściu x , zawsze wyprowadza 0 .$i$$x$$0$

Należy zauważyć, że każdy komputer w tym modelu jest powszechne, a M ( ⟨ ⌜ M ' ⌝ , x ⟩ ) = M ' ( x ) = 0 dla wszystkich M ' , x .$M$$M(\langle \ulcorner M' \urcorner, x \rangle ) = M'(x) = 0$$M', x$

To oczywiście nie jest kompletne Turinga, ale oczywiście ma uniwersalne maszyny.