Twierdzenie Rice'a - Rice's theorem

W teoria obliczalności , Twierdzenie Rice'a twierdzi, że wszystkie nietrywialne semantyczne właściwości programów są nierozstrzygalne . Właściwość semantyczna dotyczy zachowania programu (na przykład, czy program kończy działanie dla wszystkich danych wejściowych), w przeciwieństwie do właściwości składniowej (na przykład, czy program zawiera instrukcję if-then-else ). Właściwość nie jest trywialna, jeśli nie jest ani prawdziwa dla każdej częściowej funkcji obliczalnej, ani fałszywa dla każdej częściowej funkcji obliczalnej.

Twierdzenie Rice'a można również ująć w kategoriach funkcji: dla dowolnej nietrywialnej własności funkcji cząstkowych żadna ogólna i skuteczna metoda nie może rozstrzygnąć, czy algorytm oblicza funkcję cząstkową o tej własności. Tutaj właściwość funkcji częściowych nazywana jest trywialną, jeśli obowiązuje dla wszystkich częściowych funkcji obliczalnych lub dla żadnej, a efektywna metoda decyzyjna jest nazywana ogólną, jeśli rozstrzyga poprawnie dla każdego algorytmu. Twierdzenie nosi imię Henry'ego Gordona Rice'a , który udowodnił je w swojej pracy doktorskiej w 1951 roku na Uniwersytecie Syracuse .

Wstęp

Niech p będzie właściwością języka formalnego, który jest nietrywialny, co oznacza

istnieje język rekurencyjnie przeliczalny mający własność p ,
istnieje język rekurencyjnie przeliczalny nie posiadający własności p ,

(to znaczy, p nie jest ani jednolicie prawdziwe, ani jednolicie fałszywe dla wszystkich języków rekurencyjnie przeliczalnych).

Wówczas nierozstrzygnięte jest ustalenie dla danej maszyny Turinga M , czy rozpoznawany przez nią język – L(M) – ma własność p .

W praktyce oznacza to, że nie istnieje maszyna, która zawsze może decydować o tym, czy język danej maszyny Turinga ma określoną nietrywialną właściwość. Przypadki szczególne obejmują np. nierozstrzygalność, czy język rozpoznawany przez maszynę Turinga może być rozpoznany przez nietrywialną maszynę prostszą, taką jak automat skończony ( tzn. nierozstrzygnięty jest, czy język maszyny Turinga jest regularny ).

Należy zauważyć, że twierdzenie Rice'a nie dotyczy właściwości maszyn lub programów; dotyczy własności funkcji i języków. Na przykład, czy maszyna działa przez więcej niż 100 kroków na określonym wejściu, jest właściwością rozstrzygalną, nawet jeśli nie jest to trywialne. Dwie różne maszyny rozpoznające dokładnie ten sam język mogą wymagać różnej liczby kroków, aby rozpoznać ten sam ciąg wejściowy. Podobnie, to, czy maszyna ma więcej niż 5 stanów, jest rozstrzygalną właściwością maszyny, ponieważ liczbę stanów można po prostu policzyć. Dla tego rodzaju własności, które dotyczą maszyny Turinga, ale nie rozpoznawanego przez nią języka, twierdzenie Rice'a nie ma zastosowania.

Korzystając z charakterystyki akceptowalnych systemów programowania Rogersa , twierdzenie Rice'a można zasadniczo uogólnić z maszyn Turinga na większość języków programowania komputerowego : nie istnieje żadna automatyczna metoda, która rozstrzyga z ogólności nietrywialne pytania dotyczące zachowania programów komputerowych.

Jako przykład rozważmy następujący wariant problemu zatrzymania . Niech P będzie następującą własnością funkcji częściowych F jednego argumentu: P ( F ) oznacza, że F jest zdefiniowane dla argumentu '1'. Jest oczywiście nietrywialne, ponieważ istnieje funkcja częściowa, które są zdefiniowane w 1, a inne, które nie są zdefiniowane w 1. 1-zatrzymanie problemem jest problem z podjęciem decyzji jakiegokolwiek algorytmu czy definiuje funkcję o tej własności, to znaczy, czy algorytm zatrzymuje się na wejściu 1. Według twierdzenia Rice'a, problem 1-zatrzymania jest nierozstrzygnięty. Podobnie pytanie, czy maszyna Turinga T kończy się na początkowo pustej taśmie (zamiast początkowym słowem w podanym jako drugi argument oprócz opisu T , jak w przypadku pełnego zatrzymania) jest nadal nierozstrzygnięte.

Formalne oświadczenie

Niech oznaczają liczby naturalne , a niech oznaczają klasę jednoargumentowych (częściowych) funkcji obliczalnych. Niech być dopuszczalne numeracja z funkcji obliczeniowych . Oznaczmy przez z $e$ -go (częściowo) funkcję obliczeniowego. ${\ Displaystyle \ mathbb {N}}$ ${\ Displaystyle \ mathbf {P} ^ {(1)}}$ ${\ Displaystyle \ phi \ dwukropek \ mathbb {N} \ do \ mathbf {P} ^ {(1)}}$ ${\ Displaystyle \ phi _ {e}: = \ phi (e)}$

Identyfikujemy każdą właściwość, jaką może mieć funkcja obliczalna, z podzbiorem składającym się z funkcji o tej właściwości. Tak więc, mając zestaw , funkcja obliczalna ma własność wtedy i tylko wtedy, gdy . Z każdą właściwością związany jest problem decyzyjny przynależności do określenia, dane $e$ , czy . ${\ Displaystyle \ mathbf {P} ^ {(1)}}$ ${\ Displaystyle F \ subseteq \ mathbf {P} ^ {(1)}}$ $\phi _{e}$ ${\ Displaystyle F}$ ${\ Displaystyle \ phi _ {e} \ w F}$ ${\ Displaystyle F \ subseteq \ mathbf {P} ^ {(1)}}$ $D_{F}$ ${\ Displaystyle \ phi _ {e} \ w F}$

Twierdzenie Rice'a mówi, że problem decyzyjny jest rozstrzygalny (zwany także rekurencyjnym lub obliczalnym ) wtedy i tylko wtedy, gdy lub . $D_{F}$ $F=\varnic$ ${\ Displaystyle F = \ mathbf {P} ^ {(1)}}$

Przykłady

Zgodnie z twierdzeniem Rice'a, jeśli istnieje co najmniej jedna częściowa funkcja obliczalna w określonej klasie C częściowych funkcji obliczalnych i inna częściowa funkcja obliczalna nie w C, to problem rozstrzygnięcia, czy dany program oblicza funkcję w C, jest nierozstrzygalny. Na przykład twierdzenie Rice'a pokazuje, że każdy z następujących zestawów częściowych funkcji obliczalnych jest nierozstrzygalny (to znaczy, że zestaw nie jest rekurencyjny lub nie jest obliczalny ):

Klasa częściowych funkcji obliczalnych, które zwracają 0 dla każdego wejścia i jego uzupełnienie.
Klasa częściowych funkcji obliczalnych, które zwracają 0 dla co najmniej jednego wejścia i jego uzupełnienie.
Klasa częściowych funkcji obliczalnych, które są stałe i ich uzupełnienie.
Klasa częściowych funkcji obliczalnych, które są identyczne z daną częściową funkcją obliczalną, oraz jej uzupełnienie.
Klasa częściowych funkcji obliczalnych, które różnią się (tj. są niezdefiniowane) dla pewnych danych wejściowych i ich uzupełnienie.
Klasa indeksów dla funkcji obliczalnych, które są sumą.
Klasa indeksów dla zbiorów rekurencyjnie przeliczalnych, które są koskończone.
Klasa indeksów dla zbiorów rekurencyjnie przeliczalnych, które są rekurencyjne.

Dowód przez twierdzenie Kleene'a o rekurencji

Następstwem do rekurencji twierdzenie KLEENE w stanach, że dla każdej numeracji Gödla z obliczalnych funkcji i każdy funkcja obliczalna , istnieje indeks taki, że powróci . (W dalszej części mówimy, że "zwraca", jeśli jedno lub oba i są nieokreślone.) Intuicyjnie jest to funkcja quine , która zwraca swój własny kod źródłowy (liczbę Gödla), z tym wyjątkiem, że zamiast zwracać go bezpośrednio, przekazuje swój Liczba Gödla do i zwraca wynik. ${\ Displaystyle \ phi \ dwukropek \ mathbb {N} \ do \ mathbf {P} ^ {(1)}}$ $Q(x,y)$ $e$ ${\ Displaystyle \ _ {e} (y)}$ $Q(e,y)$ $f(x)$ $g(x)$ ${\ Displaystyle f (x) = g (x)}$ $f(x)$ $g(x)$ $\phi _{e}$ $\phi _{e}$ $Q$

Załóżmy, że sprzeczność jest zbiorem funkcji obliczalnych, takich jak . Następnie są funkcje obliczalne i . Załóżmy, że zestaw wskaźników , takich że jest rozstrzygalne; wtedy istnieje funkcja, która zwraca if i inaczej. W następstwie twierdzenia o rekurencji istnieje indeks , który zwraca . Ale wtedy, jeśli , to jest tą samą funkcją co , a zatem ; a jeśli , to jest , a zatem . W obu przypadkach mamy sprzeczność. ${\ Displaystyle F}$ ${\ Displaystyle \ Emptyset \ neq F \ neq \ mathbf {P} ^ {(1)}}$ ${\ Displaystyle f \ w F}$ $g\notin F$ $x$ ${\ Displaystyle \ phi _ {x} \ w F}$ $Q(x,y)$ $g(y)$ ${\ Displaystyle \ phi _ {x} \ w F}$ $f(y)$ $e$ ${\ Displaystyle \ _ {e} (y)}$ $Q(e,y)$ ${\ Displaystyle \ phi _ {e} \ w F}$ $\phi _{e}$ $g$ ${\ Displaystyle \ phi _ {e} \ notin F}$ ${\ Displaystyle \ phi _ {e} \ notin F}$ $\phi _{e}$ $f$ ${\ Displaystyle \ phi _ {e} \ w F}$

Dowód przez redukcję z problemu zatrzymania

Szkic dowodowy

Załóżmy, dla konkretności, że mamy algorytm do badania programu p i nieomylnego określania, czy p jest implementacją funkcji podnoszącej do kwadratu, która przyjmuje liczbę całkowitą d i zwraca d ² . Dowód działa równie dobrze, jeśli mamy algorytm do decydowania o dowolnej innej nietrywialnej właściwości zachowania programu (tj. semantycznej i nietrywialnej właściwości) i jest ogólnie podany poniżej.

Twierdzi się, że możemy przekonwertować nasz algorytm identyfikacji programów do kwadratu na taki, który identyfikuje funkcje, które się zatrzymują. Opiszemy algorytm, który pobiera dane wejściowe a oraz i i określa, czy program a zatrzymuje się po podaniu danych wejściowych i .

Algorytm decydowania o tym jest koncepcyjnie prosty: konstruuje (opis) nowy program t na podstawie argumentu n , który (1) najpierw wykonuje program a na wejściu i (zarówno a, jak i i są na stałe zakodowane w definicji t ) i (2) następnie zwraca kwadrat n . Jeśli a ( i ) biegnie w nieskończoność, to t nigdy nie przechodzi do kroku (2), niezależnie od n . Oczywiście t jest funkcją do obliczania kwadratów wtedy i tylko wtedy, gdy kończy się etap (1). Ponieważ założyliśmy, że możemy nieomylnie zidentyfikować programy do obliczania kwadratów, możemy określić, czy t , który zależy od a oraz i , jest takim programem i że dla każdego a oraz i ; w ten sposób możemy uzyskać program, który decyduje, czy program, a postojów na wejściu í . Zauważ, że nasz algorytm decyzji o wstrzymaniu nigdy nie wykonuje t , a jedynie przekazuje jego opis do programu identyfikacji do kwadratu, który z założenia zawsze się kończy; ponieważ konstrukcja opisu t może być również wykonana w sposób, który zawsze się kończy, decyzja wstrzymania również nie może się nie zatrzymać.

 halts (a,i) {
   define t(n) {
     a(i)
     return n×n
   }
   return is_a_squaring_function(t)
 }

Ta metoda nie zależy konkretnie od możliwości rozpoznawania funkcji obliczających kwadraty; tak długo, jak jakiś program może zrobić to, co próbujemy rozpoznać, możemy dodać wywołanie do a, aby uzyskać nasze t . Mogliśmy mieć metodę rozpoznawania programów do obliczania pierwiastków kwadratowych, programów do obliczania miesięcznej listy płac lub programów, które zatrzymują się po wprowadzeniu „Abraxas” ; w każdym przypadku będziemy w stanie rozwiązać problem zatrzymania w podobny sposób.

Dowód formalny

Jeśli mamy algorytm, który decyduje o nietrywialnej właściwości, możemy skonstruować maszynę Turinga, która rozstrzyga problem zatrzymania.

W przypadku formalnego dowodu zakłada się, że algorytmy definiują funkcje częściowe na łańcuchach i same są reprezentowane przez łańcuchy. Funkcja częściowa obliczona przez algorytm reprezentowany przez łańcuch a jest oznaczona jako F _a . Dowód ten przebiega według reductio ad absurdum : zakładamy, że istnieje nietrywialna właściwość, o której decyduje algorytm, a następnie pokazujemy, że z tego wynika, że możemy rozstrzygnąć problem zatrzymania , co nie jest możliwe, a zatem sprzeczność.

Załóżmy teraz, że P ( a ) jest algorytmem decydującym o pewnej nietrywialnej własności F _a . Bez utraty ogólności możemy założyć, że P ( no-halt ) = „no”, przy czym no-halt jest reprezentacją algorytmu, który nigdy się nie zatrzymuje. Jeśli tak nie jest, to dotyczy to negacji własności. Ponieważ P decyduje o nietrywialnej właściwości, wynika z tego, że istnieje ciąg b, który reprezentuje algorytm, a P ( b ) = "tak". Możemy wtedy zdefiniować algorytm H ( a , i ) w następujący sposób:

1. skonstruować łańcuch t reprezentujący algorytm T ( j ) taki, że

T najpierw symuluje obliczenie F _a ( i ),
wtedy T symuluje obliczenie F _b ( j ) i zwraca jego wynik.

2. powrót P ( t ).

Możemy teraz pokazać, że H decyduje o problemie zatrzymania:

Załóżmy, że algorytm reprezentowany przez a zatrzymuje się na wejściu i . W tym przypadku F _t = F _{b ,} a ponieważ P ( b ) = "tak" i wyjście P ( x ) zależy tylko od F _x , wynika z tego, że P ( t ) = " tak " i dlatego H ( a , ja ) = "tak".
Załóżmy, że algorytm reprezentowany przez a nie zatrzymuje się na wejściu i . W tym przypadku F _t = F _no-halt , tj. funkcja częściowa, która nigdy nie jest zdefiniowana. Ponieważ P ( bez zatrzymania ) = "Nie", a sygnał wyjściowy P ( x ) zależy tylko od K _x wynika, że P ( t ) = "Nie", i w związku z tym H ( , I ) = "nie".

Ponieważ wiadomo, że problem zatrzymania jest nierozstrzygalny, jest to sprzeczność i założenie, że istnieje algorytm P ( a ), który decyduje o nietrywialnej własności funkcji reprezentowanej przez a, musi być fałszywe.

Twierdzenie Rice'a i zbiory indeksów

Twierdzenie Rice'a można zwięźle wyrazić w postaci zbiorów indeksów:

Niech będzie klasą częściowych funkcji rekurencyjnych z ustawionym indeksem . Wtedy jest rekurencyjna wtedy i tylko wtedy, gdy lub . ${\mathcal {C}}$ $C$ $C$ $C=\varnic$ ${\ Displaystyle C = \ mathbb {N} }$

Oto zbiór liczb naturalnych , w tym zero . ${\ Displaystyle \ mathbb {N}}$

Analogiczne twierdzenie Rice'a dla zbiorów rekurencyjnych

Można uznać, że twierdzenie Rice'a stwierdza niemożność skutecznego decydowania o jakimkolwiek rekurencyjnie przeliczalnym zbiorze, czy ma on pewną nietrywialną właściwość. W tym dziale dajemy analog Twierdzenie Rice'a dla rekurencyjnych zestawów , zamiast zbiorów rekurencyjnie przeliczalnych. Z grubsza mówiąc, analog mówi, że jeśli można skutecznie określić dla każdego zbioru rekurencyjnego, czy ma on określoną właściwość, to tylko skończenie wiele liczb całkowitych określa, czy zbiór rekurencyjny ma tę właściwość. Wynik ten jest analogiczny do oryginalnego twierdzenia Rice'a, ponieważ oba wyniki zapewniają, że właściwość jest „rozstrzygalna” tylko wtedy, gdy można określić, czy zbiór ma tę właściwość, badając co najwyżej skończoną liczbę $i$ (dla nie , dla oryginalnego twierdzenia). jeśli należy do zestawu. $i$ $i$

Niech będzie klasą (nazywaną prostą grą i uważaną za właściwość) zbiorów rekurencyjnych. Jeśli jest zbiorem rekurencyjnym, to dla niektórych funkcja obliczalna jest funkcją charakterystyczną . Nazywamy się charakterystyczny indeks dla . (Tych jest nieskończenie wiele .) Powiedzmy, że klasa jest obliczalna, jeśli istnieje algorytm (funkcja obliczalna), który decyduje o dowolnej nieujemnej liczbie całkowitej (niekoniecznie o indeksie charakterystycznym), ${\ Displaystyle W}$ $S$ $e$ $\phi _{e}$ $S$ $e$ $S$ $e$ ${\ Displaystyle W}$ $e$

jeśli jest charakterystycznym indeksem dla zbioru rekurencyjnego należącego do , to algorytm daje "tak"; $e$ ${\ Displaystyle W}$
jeśli jest indeksem charakterystycznym dla zbioru rekurencyjnego nie należącego do , to algorytm daje "nie". $e$ ${\ Displaystyle W}$

Zbiór rozciąga ciąg zer i jedynek if dla każdego (długości ), tym elementem jest 1 if ; a w przeciwnym razie wynosi 0. Na przykład rozszerza ciąg . Ciąg jest wygranie określenia czy każdy zbiór rekurencyjny rozszerzenie należy do . Ciąg jest tracąc ustalania jeśli nie zbiór rekurencyjny rozszerzenie należy do . ${\ Displaystyle S \ podseteq \ mathbb {N}}$ ${\ Displaystyle \ tau}$ $k<|\tau |$ ${\ Displaystyle \ tau}$ $k$ ${\ Displaystyle \ tau}$ ${\ Displaystyle k \ w S}$ ${\ Displaystyle S = \ {1,3,4,7, \ ldots \}}$ ${\ Displaystyle 01011001}$ ${\ Displaystyle \ tau}$ ${\ Displaystyle \ tau}$ ${\ Displaystyle W}$ ${\ Displaystyle \ tau}$ ${\ Displaystyle \ tau}$ ${\ Displaystyle W}$

Możemy teraz sformułować następujący odpowiednik twierdzenia Rice'a (Kreisel, Lacombe i Shoenfield, 1959, Kumabe i Mihara, 2008):

Klasa zbiorów rekurencyjnych jest obliczalna wtedy i tylko wtedy, gdy istnieje rekurencyjnie przeliczalny zbiór przegrywających ciągów określających i rekurencyjnie przeliczalny zbiór wygrywających ciągów określających w taki sposób, że każdy zbiór rekurencyjny rozszerza ciąg w . ${\ Displaystyle W}$ $T_{0}$ $T_{1}$ $T_{0}\kubek T_{1}$

Wynik ten został zastosowany do podstawowych problemów w obliczeniowym wyborze społecznym (szerzej, algorytmicznej teorii gier ). Na przykład Kumabe i Mihara (2008, 2008) stosują ten wynik do badania liczb Nakamury dla prostych gier w teorii gier kooperacyjnych i teorii wyboru społecznego .

Zobacz też

Twierdzenia o niezupełności Gödla
Zatrzymanie problemu
Teoria rekurencji
Twierdzenie o ryżu-Shapiro
Twierdzenie Scotta-Curry'ego , analog do twierdzenia Rice'a w rachunku lambda
Dowód Turinga
Wittgenstein o zasadach i języku prywatnym

Uwagi

^ Soare, Robert I. (1987). Rekurencyjnie przeliczalne zbiory i stopnie . Skoczek. P. 21 .
^ Zbiórjest rekurencyjnie przeliczalny, jeśli dla niektórych, gdziejest domeną (zbiór danych wejściowychtaki, który jest zdefiniowany). Wynik dla zestawów rekurencyjnie przeliczalnych można uzyskać z tego dla (częściowych) funkcji obliczalnych, biorąc pod uwagę klasę, gdziejest klasą zestawów rekurencyjnie przeliczalnych. ${\ Displaystyle S \ podseteq \ mathbb {N}}$ ${\ Displaystyle S = W_ {e}: = {\ textrm {dom}} \ \ phi _ {e}: = \ {x: \ phi _ {e} (x) \ strzałka w dół \}}$ $e$ $W_{e}$ ${\textrm {dom}}\,\phi _{e}$ $x$ ${\ Displaystyle \ _ {e} (x)}$ $\phi _{e}$ ${\ Displaystyle \ {\ phi _ {e}: {\ textrm {dom}} \ \ phi _ {e} \ w C \}}$ $C$
^ Zbiór rekurencyjnie przeliczalnyjest rekurencyjny, jeśli jego uzupełnienie jest rekurencyjnie przeliczalne. Równoważniejest rekurencyjny, jeśli jego funkcja charakterystyczna jest obliczalna. ${\ Displaystyle S \ podseteq \ mathbb {N}}$ $S$
^ Kreisel, G.; Lacombe, D.; Shoenfield, JR (1959). „Częściowe rekurencyjne funkcjonały i efektywne operacje”. W Heyting, A. (red.). Konstruktywność w matematyce . Studia z logiki i podstaw matematyki. Amsterdam: Holandia Północna. s. 290-297.
^ ^B Kumabe, M .; Mihara, HR (2008). „Obliczalność prostych gier: charakterystyka i zastosowanie do rdzenia” . Czasopismo Ekonomii Matematycznej . 44 (3–4): 348–366. arXiv : 0705.3227 . doi : 10.1016/j.jmateco.2007.05.012 .
^ Kumabe, M.; Mihara, HR (2008). „Liczby Nakamura dla prostych gier obliczeniowych” . Wybór społeczny i dobrobyt . 31 (4): 621. arXiv : 1107.0439 . doi : 10.1007/s00355-008-0300-5 .