4. Riceova věta¶

Podle první Riceovy věty nelze algoritmicky rozhodovat žádnou netriviální vstupně-výstupní vlastnost programů. Například tedy nelze rozhodovat, jestli program na vstupu zastaví pro každý vstup; jestli program na vstupu vrací pro všechna lichá čísla jejich druhou mocninu; jestli program na vstupu nikdy nevrátí False; jestli program na vstupu vrací pro nějaký vstup 42, ...

K pochopení důkazu Riceovy věty může pomoci následující příklad. Představme si (pro spor), že bychom uměli rozhodovat, zda Pythoní funkce na vstupu vrací pro všechna lichá (nepárna) čísla jejich druhou mocninu (nazvěme toto chování jako lichočtvercové chování). Všimněme si, že lichočtvercové chování je čistě vstupně-výstupní (závisí pouze na vstupu a výstupu funkce) a je netriviální - nemá ho například prázdná funkce a má ho například následující Pythoní funkce theta:

# Priklad funkce lichoctvercoveho chovani
def theta(x):
    return x * x

Ukážeme, že pokud bychom uměli rozhodovat lichočtvercové chování, pak bychom uměli rozhodovat i problém zastavení (v ukázce použijeme variantu se 2 parametry - chceme rozhodnout, zda funkce f zastaví pro vstup i). Ukážeme tedy redukci problému zastavení na problém lichočtvercového chování. Jak bude rekukce vypadat? Chceme, aby halt(f, i) == True právě tehdy, když has_squaring_behavior(reduction(f, i)) == True. Redukce tedy musí vracet funkci, která má lichočtvercové chování právě tehdy, když funkce f zastaví pro vstup i. Není těžké takovou funkci napsat:

# Funkce, ktera se bud chova jako prazdna funkce (pokud f na i cykli),
# nebo jako funkce theta (pokud f na i zastavi).
# Funkce ma jediny vstupni parametr x. (f, i jsou uzaverove parametry)
def epsilon_or_theta(x):
    f(i)
    return theta(x)

Funkce epsilon_or_theta se buď chová úplně přesně jako theta (pokud f nad i zastaví), nebo úplně přesně jako prázdná funkce (pokud f nad i cyklí). Přitom theta má lichočtvercové chování a prázdná funkce nemá lichočtvercové chování. Funkce epsilon_or_theta tedy má lichočtvercové chování právě tehdy, když f nad i zastaví. A to je přesně to, co jsme chtěli, redukce je hotova. Celý kód by vypadal takto:

# Pro spor predpokladame, ze existuje funkce, ktera rozhoduje,
# zda ma predana funkce ctvercove chovani, tj. vraci druhe mocniny
# vstupu (pro libovolny vstup).
from impossibility import has_squaring_behavior

# Vraci True, pokud fce f zastavi na vstupu i
def halt(f, i):
    return has_squaring_behavior(reduction(f, i))

# Priklad funkce ctvercoveho chovani
def theta(x):
    return x * x

# Redukuje problem zastaveni na problem lichoctvercoveho chovani
def reduction(f, i):
    # Funkce, ktera se bud chova jako prazdna funkce (pokud f na i cykli),
    # nebo jako theta (pokud f na i zastavi) (jde o uzaver nad f, i).
    def epsilon_or_theta(x):
        f(i)
        return theta(x)
    # Redukce vraci vyse uvedenou funkci epsilon_or_theta
    return epsilon_or_theta

Rozmyslete si, proč byly oba požadavaky na lichočtvercovou vlastnost (aby byla netriviální a čistě vstupně-výstpuní) při redukci nutné.

Podobně bychom mohli vést důkaz pro všechny další netriviální vstupně-výstupní vlastnosti (například ty uvedené v úvodním odstavci). Abychom viděli, že tyto dva požadavky jsou opravdu to jediné, co k důkazu nerozhodnutelnosti vlastnosti potřebujeme, zobecněme nyní uvedené schéma pro libovolné netriviální vstupně-výstupní chování Y.

# Pro spor predpokladame, ze existuje funkce, ktera rozhoduje
# nejake netrivialni vstupne-vystupni chovani Y, ktere splunuje
# funkce theta a nesplnuje prazdna funkce.
from impossibility import has_Y_behavior, theta

# Vraci True, pokud fce f zastavi na vstupu i
def halt(f, i):
    return has_Y_behavior(reduction(f, i))

# Redukuje problem zastaveni na problem rozhodovani o chovani Y
def reduction(f, i):
    # Funkce, ktera se bud chova jako prazdna funkce (pokud f na i cykli),
    # nebo jako theta (pokud f na i zastavi) (jde o uzaver nad f, i).
    def epsilon_or_theta(x):
        f(i)
        return theta(x)
    # Redukce vraci vyse uvedenou funkci epsilon_or_theta
    return epsilon_or_theta