Rice's teorem

I beräkningsbarhetsteorin säger Rices teorem att alla icke-triviala semantiska egenskaper hos program är oavgjorda . En semantisk egenskap handlar om programmets beteende (till exempel avslutas programmet för alla ingångar), till skillnad från en syntaktisk egenskap (innehåller programmet till exempel en if-then-else- sats). En egenskap är icke-trivial om den varken är sann för varje partiell beräkningsbar funktion eller falsk för varje partiell beräkningsbar funktion.

Rice's teorem kan också sättas i termer av funktioner: för alla icke-triviala egenskaper hos partiella funktioner kan ingen generell och effektiv metod avgöra om en algoritm beräknar en partiell funktion med den egenskapen. Här kallas en egenskap hos partiella funktioner trivial om den gäller för alla partiella beräkningsbara funktioner eller för ingen, och en effektiv beslutsmetod kallas generell om den bestämmer korrekt för varje algoritm. Teoremet är uppkallat efter Henry Gordon Rice , som bevisade det i sin doktorsavhandling från 1951 vid Syracuse University .

Introduktion

Låt p vara en egenskap hos ett formellt språk L som är icke-trivialt, vilket betyder

det finns ett rekursivt uppräknat språk som har egenskapen p ,
det finns ett rekursivt uppräknat språk som inte har egenskapen p ,

(det vill säga, p är varken enhetligt sant eller enhetligt falskt för alla rekursivt uppräknade språk).

Då är det obestämbart att för en given Turing-maskin M avgöra om språket som känns igen av den har egenskapen p .

I praktiken betyder detta att det inte finns någon maskin som alltid kan avgöra om språket för en given Turing-maskin har en viss icke-trivial egenskap. Särskilda fall inkluderar t.ex. oavgörbarheten av huruvida språket som känns igen av en Turing-maskin skulle kunna kännas igen av en icke-trivial enklare maskin, såsom en finit automat (vilket betyder att det är obestämbart om språket i en Turing-maskin är regelbundet ).

Det är viktigt att notera att Rice's teorem inte berör egenskaperna hos maskiner eller program; det gäller egenskaper hos funktioner och språk. Till exempel, huruvida en maskin körs i mer än 100 steg på en viss ingång är en avgörbar egenskap, även om den är icke-trivial. Två olika maskiner som känner igen exakt samma språk kan kräva olika antal steg för att känna igen samma inmatningssträng. På samma sätt är om en maskin har fler än fem tillstånd en avgörbar egenskap hos maskinen, eftersom antalet tillstånd helt enkelt kan räknas. För egenskaper av detta slag, som avser en Turingmaskin men inte språket som känns igen av den, gäller inte Rice's teorem.

Med hjälp av Rogers karaktärisering av acceptabla programmeringssystem kan Rices sats i huvudsak generaliseras från Turing-maskiner till de flesta datorprogrammeringsspråk : det finns ingen automatisk metod som avgör generellt icke-triviala frågor om datorprograms beteende.

Som ett exempel, betrakta följande variant av stoppproblemet . Låt P vara följande egenskap för partiella funktioner F i ett argument: P ( F ) betyder att F är definierat för argumentet '1'. Det är uppenbarligen icke-trivialt, eftersom det finns delfunktioner som är definierade vid 1, och andra som är odefinierade vid 1. Det 1-stoppande problemet är problemet med att avgöra för vilken algoritm som helst om den definierar en funktion med denna egenskap, dvs. om algoritmen stannar vid ingång 1. Enligt Rices sats är 1-stoppproblemet oavgörbart. På samma sätt är frågan om huruvida en Turing-maskin T avslutas på ett initialt tomt band (snarare än med ett initialt ord w givet som andra argument utöver en beskrivning av T , som i det fullständiga stoppproblemet) fortfarande oavgjord.

Formellt uttalande

Låt $\mathbb {N}$ beteckna de naturliga talen , och låt $\mathbf {P} ^{(1)}$ beteckna klassen av unära (partiella) beräkningsbara funktioner. Låt $\phi \colon \mathbb {N} \to \mathbf {P} ^{(1)}$ vara en tillåten numrering av de beräkningsbara funktionerna . Beteckna med $\phi _{e}:=\phi (e)$ den $e$ (delvisa) beräkningsbara funktionen.

Vi identifierar varje egenskap som en beräkningsbar funktion kan ha med delmängden $\mathbf {P} ^{(1)}$ som består av funktionerna med den egenskapen. Således, givet en mängd ${\displaystyle F\subseteq \mathbf {P} ^{(1)}} ,$ har en beräkningsbar funktion ${\displaystyle \phi _{e}} egenskapen$ ${\ displaystyle F}$ om och endast om $\phi _{e}\in F$ . För varje egenskap $F\subseteq \mathbf {P} ^{(1)}$ finns det ett associerat medlemskapsbeslutsproblem D $\displaystyle D_{F}}$ att bestämma, givet $e$ , om $\phi _{e}\in F$ .

Rice teorem säger att beslutsproblemet $D_{F}$ är avgörbart (även kallat rekursivt eller beräkningsbart ) om och endast om $F=\varnothing$ eller ${\ displaystyle F=\mathbf {P} ^{(1)}}$ .

Exempel

Enligt Rices teorem, om det finns åtminstone en partiell beräkningsbar funktion i en viss klass C av partiella beräkningsbara funktioner och en annan partiell beräkningsbar funktion som inte finns i C så är problemet med att avgöra om ett visst program beräknar en funktion i C obestämbart. Till exempel visar Rice's teorem att var och en av följande uppsättningar av partiella beräkningsbara funktioner är obestämbara (det vill säga mängden är inte rekursiv eller inte beräkningsbar ):

0 Klassen av partiella beräkningsbara funktioner som återkommer för varje ingång, och dess komplement.
0 Klassen av partiella beräkningsbara funktioner som returnerar för minst en ingång, och dess komplement.
Klassen av partiella beräkningsbara funktioner som är konstanta och dess komplement.
Klassen av partiella beräkningsbara funktioner som är identiska med en given partiell beräkningsbar funktion, och dess komplement.
Klassen av partiella beräkningsbara funktioner som divergerar (dvs odefinierade) för viss indata, och dess komplement.
Klassen av index för beräkningsbara funktioner som är totala.
Klassen av index för rekursivt uppräknade uppsättningar som är kofinita.
Klassen av index för rekursivt uppräknade mängder som är rekursiva.

Bevis av Kleenes rekursionssats

En följd av Kleenes rekursionsteorem säger att för varje Gödel-numrering $\phi \colon \mathbb {N} \to \mathbf {P} ^{(1)}$ av de beräkningsbara funktionerna och varje beräkningsbar funktion $Q(x,y)$ , det finns ett index $e$ så att $\phi _{e}(y)$ returnerar $Q(e,y)$ . (I det följande säger vi att $f(x)$ "returnerar" $g(x)$ om antingen $f (x)=g(x)$ , eller både $f(x)$ och $g(x)$ är odefinierade.) Intuitivt, $\phi _{e}$ är en quine , en funktion som returnerar sin egen källkod (Gödel-nummer), förutom att istället för att returnera den direkt, skickar $\phi _{e}$ sitt Gödel-nummer till ${\ displaystyle Q}$ och returnerar resultatet.

Antag för motsägelse att $F$ är en uppsättning beräkningsbara funktioner så att $\emptyset \neq F\neq \mathbf {P} ^{(1)}$ . Sedan finns det beräkningsbara funktioner $f\in F$ och $g\notin F$ . Antag att mängden index $x$ så att $\phi _{x}\in F$ är avgörbar; då finns det en funktion $Q(x,y)$ som returnerar $g(y)$ om $\phi _{x} \in F$ , och $f(y)$ annars. Till följd av rekursionssatsen finns det ett index $Q( e,y)$ $\displaystyle e}$ så att $\phi _{e}(y)$ returnerar . Men sedan, om $\phi _{e}\in F$ , så är $\phi _{e}$ samma funktion som $g$ , och därför $\phi _{e}\notin F$ ; och om $\phi _{e}\notin F$ , så är $\phi _{e}$ $f$ , och därför $\phi _{e}\in F$ . I båda fallen har vi en motsägelse.

Bevis genom reduktion från stoppproblemet

Bevisskiss

Antag, för att vara konkret, att vi har en algoritm för att undersöka ett program p och ofelbart avgöra om p är en implementering av kvadreringsfunktionen, som tar ett heltal d och returnerar d ² . Beviset fungerar lika bra om vi har en algoritm för att bestämma någon annan icke-trivial egenskap hos programbeteende (dvs. en semantisk och icke-trivial egenskap), och ges generellt nedan.

Påståendet är att vi kan omvandla vår algoritm för att identifiera kvadreringsprogram till en som identifierar funktioner som stannar. Vi kommer att beskriva en algoritm som tar ingångarna a och i och bestämmer om ett program stannar när inmatningen i ges .

Algoritmen för att avgöra detta är begreppsmässigt enkel: den konstruerar (beskrivningen av) ett nytt program t med ett argument n , vilket (1) först kör program a på ingång i (både a och i är hårdkodade i definitionen av t ), och (2) returnerar sedan kvadraten på n . Om a ( i ) löper för alltid, kommer t aldrig till steg (2), oavsett n . Då är helt klart t en funktion för att beräkna kvadrater om och endast om steg (1) avslutas. Eftersom vi har antagit att vi ofelbart kan identifiera program för att beräkna kvadrater, kan vi avgöra om t , som beror på a och i , är ett sådant program; alltså har vi fått ett program som avgör om ett program stannar vid ingång i . Observera att vår stoppbeslutsalgoritm aldrig exekverar t , utan bara skickar sin beskrivning till kvadreringsidentifieringsprogrammet, som av antagande alltid avslutas; eftersom konstruktionen av beskrivningen av t också kan göras på ett sätt som alltid upphör, kan stoppbeslutet inte heller låta bli att stanna.

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

Denna metod är inte specifikt beroende av att kunna känna igen funktioner som beräknar kvadrater; så länge som något program kan göra det vi försöker känna igen kan vi lägga till ett anrop till a för att få vårt t . Vi kunde ha haft en metod för att känna igen program för att beräkna kvadratrötter, eller program för att beräkna den månatliga lönelistan, eller program som stannar när inmatningen " Abraxas" ges ; i varje fall skulle vi kunna lösa stoppproblemet på liknande sätt.

Formella bevis

Om vi har en algoritm som avgör en icke-trivial egenskap, kan vi konstruera en Turing-maskin som avgör stoppproblemet.

För det formella beviset antas algoritmer definiera delfunktioner över strängar och representeras själva av strängar. Den partiella _funktionen som beräknas av algoritmen representerad av en sträng a betecknas Fa . Detta bevis fortsätter genom reductio ad absurdum : vi antar att det finns en icke-trivial egenskap som avgörs av en algoritm, och visar sedan att det följer att vi kan avgöra stoppproblemet , vilket inte är möjligt, och därför en motsägelse.

_Låt oss nu anta att P ( a ) är en algoritm som bestämmer någon icke-trivial egenskap hos Fa . Utan förlust av generalitet kan vi anta att P ( no-halt ) = "no", där no-halt är representationen av en algoritm som aldrig stannar. Om detta inte är sant, så gäller detta för negationen av egendomen. Eftersom P bestämmer en icke-trivial egenskap, följer det att det finns en sträng b som representerar en algoritm och P ( b ) = "ja". Vi kan sedan definiera en algoritm H ( a , i ) enligt följande:

1. konstruera en sträng t som representerar en algoritm T ( j ) så att

T simulerar först beräkningen av _Fa ( i ) ,
sedan simulerar T beräkningen av F _b ( j ) och returnerar dess resultat.

2. returnera P ( t ).

Vi kan nu visa att H bestämmer stoppproblemet:

Antag att algoritmen som representeras av ett stopp vid ingång i . I det här fallet Ft = _Fb och eftersom P ( b ) = "ja" och utdata från P ( x ) _endast beror på F _x , följer det att P ( t ) = "ja" och därför H ( a , i ) = "ja".
Antag att algoritmen som representeras av a inte stannar vid ingång i . I detta fall F _t = F _no-halt , dvs den partiella funktionen som aldrig definieras. Eftersom P ( no-halt ) = "no" och utmatningen av P ( x ) endast beror på F _x , följer det att P ( t ) = "no" och därför H ( a , i ) = "no".

Eftersom stoppproblemet är känt för att vara oavgörbart är detta en motsägelse och antagandet att det finns en algoritm P ( a ) som avgör en icke-trivial egenskap för funktionen representerad av a måste vara falsk.

Rice's sats och indexuppsättningar

Rice's teorem kan kortfattat uttryckas i termer av indexuppsättningar:

Låt ${\mathcal {C}}$ vara en klass av partiella rekursiva funktioner med indexuppsättning $C$ . Då är $C$ rekursiv om och endast om $C=\varnothing$ eller $C=\mathbb {N}$ .

Här är $\mathbb {N}$ mängden naturliga tal , inklusive noll .

En analog till Rices sats för rekursiva mängder

Man kan betrakta Rices teorem som att det är omöjligt att effektivt avgöra för någon rekursivt uppräknad mängd om den har en viss icke-trivial egenskap. I det här avsnittet ger vi en analog till Rices sats för rekursiva mängder istället för rekursivt uppräknade mängder . I grova drag säger analogen att om man effektivt kan avgöra för varje rekursiv mängd om den har en viss egenskap, så avgör bara ändligt många heltal om en rekursiv mängd har egenskapen. Detta resultat är analogt med det ursprungliga satsen för Rice, eftersom båda resultaten hävdar att en egenskap är "avgörbar" endast om man kan avgöra om en mängd har den egenskapen genom att undersöka för högst ändligt många i {\displaystyle i } $för$ no $i$ , för den ursprungliga satsen), om $i$ till mängden.

Låt $W$ vara en klass (kallas ett enkelt spel och betraktas som en egenskap) av rekursiva mängder. Om $S$ är en rekursiv mängd, så är för vissa $e$ den beräkningsbara funktionen $\phi _{e}$ den karakteristiska funktionen för $S$ . Vi kallar $e$ ett karakteristiskt index för $S$ . (Det finns oändligt många sådana $e$ .) Låt oss säga att klassen $W$ är beräkningsbar om det finns en algoritm (beräknarbar funktion) som bestämmer för alla icke-negativa heltal $e$ (inte nödvändigtvis ett karakteristiskt index),

om $e$ är ett karakteristiskt index för en rekursiv mängd som tillhör $W$ , då ger algoritmen "ja";
om $e$ är ett karakteristiskt index för en rekursiv mängd som inte tillhör $W$ , så ger algoritmen "nej".

En mängd $S\subseteq \mathbb {N}$ förlänger en sträng $\tau$ av 0:or och 1:or om för varje $k<|\tau |$ (längden på $\tau$ ), ${\displaystyle k}:$ te elementet i $\tau$ är 1 om $k \i S$ ; och är 0 annars. Till exempel, $S=\{1,3,4,7,\ldots \}$ förlänger strängen $01011001$ . En sträng $\tau$ vinner och avgör om varje rekursiv uppsättning som sträcker sig $\tau$ tillhör $W$ . En sträng $\tau$ förlorar och avgör om ingen rekursiv uppsättning som sträcker sig $\tau$ tillhör $W$ .

Vi kan nu ange följande analog till Rice's teorem :

En klass $W$ av rekursiva mängder kan beräknas om och endast om det finns en rekursivt uppräknad uppsättning $T_{0}$ av förlorande bestämningssträngar och en rekursivt uppräknbar uppsättning $T_{1}$ av vinnande bestämningssträngar så att varje rekursiv uppsättning förlänger en sträng i $T_{0}\cup T_{1}$ .

Detta resultat har tillämpats på grundläggande problem i beräkningsmässigt socialt val (mer allmänt, algoritmisk spelteori) . Till exempel, Kumabe och Mihara tillämpar detta resultat på en undersökning av Nakamura-talen för enkla spel i kooperativ spelteori och sociala valteori .

Se även

Gödels ofullständighetssatser
Stoppa problem
Rekursionsteori
Ris–Shapiros teorem
Scott–Curry teorem , en analog till Rices teorem i lambdakalkyl
Turings bevis
Wittgenstein om regler och privat språk

Anteckningar

^ Soare, Robert I. (1987). Rekursivt uppräknade uppsättningar och grader . Springer. sid. 21 . ISBN 9780387152998 .
^ En mängd $S\subseteq \mathbb {N}$ är rekursivt uppräknad om ${\displaystyle S=W_{ e}:={\textrm {dom}}\,\phi _{e}:=\{x:\phi _{e}(x)\downarrow \}} för vissa e {\displaystyle$ e $,$ där $W_{e}$ är domänen ${\displaystyle {\textrm {dom}}\,\phi _{e}} ($ uppsättningen av ingångar $x$ så att $\phi _{e}(x)$ är definierad) av $\phi _{e}$ . Resultatet för rekursivt uppräknade mängder kan erhållas från det för (partiella) beräkningsbara funktioner genom att beakta klassen $\{\phi _{e}:{\textrm {dom}} \,\phi _{e}\in C\}$ , där $C$ är en klass av rekursivt uppräknade mängder.
^ En rekursivt uppräknbar mängd $S\subseteq \mathbb {N}$ är rekursiv om dess komplement är rekursivt numerbar. På motsvarande sätt $S$ rekursiv om dess karakteristiska funktion är beräkningsbar.
^ Kreisel, G.; Lacombe, D.; Shoenfield, JR (1959). "Delvis rekursiva funktioner och effektiva operationer". I Heyting, A. (red.). Konstruktivitet i matematik . Studier i logik och matematikens grunder. Amsterdam: Nord-Holland. s. 290–297.
^ ^a ^b Kumabe, M.; Mihara, HR (2008). "Beräkningsbarhet för enkla spel: En karaktärisering och tillämpning till kärnan" . Journal of Mathematical Economics . 44 (3–4): 348–366. arXiv : 0705.3227 . doi : 10.1016/j.jmateco.2007.05.012 . S2CID 8618118 .
^ Kumabe, M.; Mihara, HR (2008). "Nakamura-siffrorna för beräkningsbara enkla spel" . Socialt val och välfärd . 31 (4): 621. arXiv : 1107.0439 . doi : 10.1007/s00355-008-0300-5 . S2CID 8106333 .