Om stopp-problemet

”Kan man skriva ett program som avgör om ett godtyckligt program terminerar?

Vi skall nu med ett motsägelsebevis visa ett det inte finns något sådant program.
Antag att ett sådant program Q finns.

Q(P) =…
…True om P terminerar
…False om P inte terminerar

Detta innebär att det också är möjligt att skriva ett program Q’ sådant att

Q’(P) =…
… inte terminerar om P terminerar
… terminerar om P inte terminerar

Eftersom P är godtyckligt kan Q’ ta sig själv som indata. Detta innebär alltså att Q’ skall terminera om Q’ inte terminerar och att Q’ inte skall terminera om Q’ terminerar!

Q’(Q’) =…
… inte terminerar om Q’ terminerar
… terminerar om Q’ inte terminerar

Vi har således fått en motsägelse, vilket innebär att vårt ursprungliga antagande är felaktigt. Slutsatsen blir att det inte kan finnas något program som kan avgöra om ett godtyckligt program terminerar, vilket innebär att problemet är icke beräkningsbart.”

Så formulerades beviset för att det s.k. stopp-problemet inte är beräkningsbart i kursmaterialet till Programmeringsteknik, fortsättningskurs, som jag gick läsperiod 3 1997 (jag ber om ursäkt för den fula sättningen; det är mina skrala HTML-kunskaper som gör sig gällande). Jag tyckte redan från början att det var något som inte stämde med det här beviset, och efter en stunds funderande (mer nedan om varför jag ägnade tankemöda åt denna för kursen tämligen perifera frågeställning) insåg jag felet:

När vi inför Q(P) (och analogt Q’(P)), måste vi bestämma oss för om vi med P avser ett exekverbart, entydigt program inklusive dess indata, eller om P är ett program som blir entydigt bestämt och exekverbart först när vi tilldelat ett värde till dess indata – så att vi egentligen har ett program P(X). Om vi menar det senare, måste Q(P) egentligen vara ett kontraherat skrivsätt för Q(P,X), för det är ett trivialt faktum (som då och då gör sig påmint för alla som programmerar) att det finns program som terminerar med viss indata men inte med annan.

Om vi däremot inte vill krångla till resonemanget genom att införa ett ytterligare argument för Q och Q’(och inte få något av principiellt värde för det), måste vi med P mena ett program som är entydigt bestämt inklusive dess indata. Och då kan Q’ inte ta Q’ som indata! Inte enbart i alla fall, för Q’ i argumentet till Q’ måste också ha indata för att bli ett exekverbart program. Alltså: Q’(Q’) är inte definierat. Vi kan skriva Q’(Q’(P)), men för detta måste vi alltså bestämma vad P är. När vi väl gjort det, kan det förstås visa sig att Q’(P) terminerar, men att Q’(Q’(P)) inte gör det, men i det finns ingen motsägelse; det är ju två olika uttryck! En motsägelse blir det först om man slarvar och kallar både Q’(Q’(P)) och Q’(P) för Q’ och sätter in dem i samma mening.

Låt mig illustrera med en parodi på beviset ovan:
”…
Detta innebär att det också är möjligt att definiera en funktion f’ sådan att

f’(x)=…
… -1, om x är större än noll
… 1, om x är mindre än noll

Eftersom x är godtyckligt kan f’ ta sig själv som indata. Detta innebär alltså att f’ skall vara större än noll om f’ är mindre än noll och att f’ skall vara mindre än noll , om f’ är större än noll!” Slutsatsen skulle då bli att det inte kan finnas en funktion som räknar ut om ett tal är större eller mindre än noll.

Jag framförde den här invändningen (men jag har för mig att jag använde funktionen f(x)=x2 som exempel) till föreläsaren på rasten efter genomgången av det här beviset. Han grubblade i några minuter, men han var väl inte beredd att acceptera att beviset var felaktigt på en gång. Själv var jag heller inte beredd att acceptera att ett välkänt resultat inom datalogin kunde vara baserat på något så enfaldigt. Kanske var det så att någon väsentlig del av beviset gått förlorad i den lite informella framställningen av det som vi fick ta del av?

För ett ta reda på det sökte jag efter en mer stringent formulering av beviset och fann den här (scrolla ner till ”Stopp-problemet är oavgörbart”). Här har man gett Q’ en mer explicit beskrivning, kallad M(P). Ja, i alla fall ser den mer stringent ut, men den faller som ett korthus vid den mildaste prövning av dess grunder. Först och främst får man fråga sig vad som menas med ”Stopp(P,P)”. Funktionen ”Stopp” är ju införd som ”Stopp(P,X) som avgör stopp-problemet”, där X står för P:s indata. Måste P då vara ett program som tar just ett program som indata? Hur skulle man annars utan vidare kunna införa ”Stopp(P,P)”?

Men bortsett från den lapsusen(?), lägg märke till hur försåtligt argumentet till M försvinner, när M görs till argument till sig själv i ”Vad händer när M(M) körs?” Varför inte skriva M(M(P))? Tja, det skulle förstås ha gjort det uppenbart att man inte bara kan fråga vad som händer när M(M) körs, men hur kan man missa en så uppenbar sak? Kan personen som skrev det ha noterat den här bristen men ändå låtit det stå eftersom han var säker på att beviset ändå stämmer? Eller kan det vara så att det här faktiskt inte är så lätt att upptäcka om man inte tänker på det?

I grunden är det samma invändning som Wittgenstein framförde mot Russels paradox: En funktion kan inte ta sig själv som argument. Om han därmed lyckades avlägsna det problem som Russel uppmärksammade oss på kan jag inte avgöra, eftersom jag aldrig sysselsatt mig med att infoga mängdläran i något formellt system (och aldrig satt mig in i hans typteori heller för den delen), men jag håller i princip med Wittgenstein, och därför tror jag att paradoxen, så som den brukar formuleras*, är en konsekvens av ett slarvigt språkbruk.

Varför började jag fundera på detta, och varför var jag så övertygad om att beviset (gällande stopp-problemet alltså) inte kunde vara korrekt? Jo, jag insåg att en människa i allmänhet kan lösa det problem som det enligt beviset inte går att finna en algoritm för, dvs. avgöra om ett visst program terminerar eller inte. Visst finns det program som är för stora och komplexa för att en enskild person ska kunna utföra den uppgiften, men det går inte att föreställa sig ett program med givna indata som i princip inte skulle kunna analyseras i det här avseendet, även om ett större antal dataloger fick jobba med det under lång tid. Och om en människa, eller flera människor, kan lösa en beräkningsuppgift, kan man också – i princip – skriva ett program som löser samma uppgift. Det är i alla fall min övertygelse. Kan det vara så att de som lyfter fram stopp-problemet som ett icke beräkningsbart problem har den motsatta övertygelsen och därför inte bryr sig om att granska beviset så noga?

Nå, jag antar att jag stuckit ut hakan lite här (till och med gjort mig skyldig till viss psykologisering av oliktänkandes motiv), men jag går längre än så: Den som lyckas rädda beviset för att stopp-problemet inte är beräkningsbart bjuder jag på en öl eller motsvarande. Nej, två öl. Eller motsvarande. Maila mig eller lägg upp det på din egen blogg.

(*Russels paradox: Låt M vara mängden av alla mängder som inte är delmängder i sig själva. Är nu M en delmängd av sig själv? Om den är en delmängd av sig själv, är den inte en delmängd av sig själv, eftersom den inte uppfyller kriteriet för att ingå i M, dvs. att vara en delmängd i sig själv – och vice versa.)