torsdag, februari 01, 2007

Stopp-problemet, uppföljning

Det verkar som om jag blir tvungen att bjuda på de där ölen (eller vad blir egentligen bestämd form plural av ”öl” i betydelsen ”en öl”?) jag satsade för ett par veckor sedan. Mikael Ståldal har nämligen pekat på ett misstag i min analys av det andra av de två bevisen för att stopp-problemet inte är beräkningsbart.

Jag skrev att M(M) egentligen borde skrivas M(M(P)), och det kan man ju säga, men faktiskt behöver det P som M(P) i argumentet till M anropar aldrig specificeras. Skälet till det är att M(P) anropar Stopp(P,X) på ett mycket speciellt sätt: Stopp(P,P). Det betyder att M bara tar som indata program som kan ta sig själva som indata. Eftersom sådana program kan skrivas, kan programmet M(P) bildas, om Stopp(P,X) finns. Det betyder också (och det var det här jag inte insåg) att M(P) tar ett program P som indata exklusive P:s indata, eftersom M använder P två gånger i Stopp, både för ”programmet” P och ”indata” X.

En ytterligare spetsfundighet är att M råkar vara just ett program som kan tas sig självt som indata och därmed kvalificerar sig som indata till M. Anropet av Stopp(P,X) i M(M(P’)) (P’ för tydligheten skull) blir av formen Stopp(M(P'),M(P')). M(P') på P-platsen i Stopp(P,X) är ett program som tar som indata ett program exklusive detta programs indata. M(P') på X-platsen är ett program, exklusive indata, och är därmed just ett sådant program som M(P') på P-platsen tar som indata. Det fungerar!