Biorąc pod uwagę dowolną funkcję, F określamy funkcję f” która zwraca na wejściu n jeśli f zatrzymywane na wejściu n. Teraz, dla pewnej liczby x zdefiniować funkcję g, które na wejściu n, powraca jeśli n = x, a poza tym wymaga F '(n).
przypadku równoważności funkcjonalnej były rozstrzygalne, następnie podejmowanie decyzji czy g jest identyczna F” decyduje f postojów na wejściu x. To by rozwiązało Halting problem. Powiązane z tą dyskusją jest Rice's theorem.
Wniosek: Równoważność funkcjonalna jest nierozstrzygalna.
Poniżej znajduje się dyskusja na temat ważności tego dowodu. Pozwólcie, że omówię, co robi dowód, i podam przykładowy kod w Pythonie.
Dowód tworzy funkcję f” który na wejściu n zaczyna obliczenia f (n). Gdy ta obliczeniowy kończy f”zwraca 1. Zatem F '(n) = 1 IFF f postojów na wejściu n i f' nie zatrzyma na n IFF F nie robi "t. Pyton:
def create_f_prime(f):
def f_prime(n):
f(n)
return 1
return f_prime
Następnie utworzyć funkcję g która przyjmuje n jako dane wejściowe i porównuje się pewną wartość x. Jeśli n = x, wówczas g (n) = g (x) = 1, w innym przypadku g (n) = f '(n). Pyton:
def create_g(f_prime, x):
def g(n):
return 1 if n == x else f_prime(n)
return g
teraz trick jest to, że dla wszystkich N = X mamy że g (n) = f '(n)!. Ponadto wiemy, że g (x) = 1. Tak więc, jeśli g = f ', wówczas f' (x) = 1, a zatem f (x) zatrzymuje się. Podobnie, jeśli g! = F ' koniecznie musi być f' (x)! = 1, co oznacza, że f (x) nie zatrzymuje się. Tak więc, decydowanie, czy g = f ' jest równoważne podejmowaniu decyzji, czy f zatrzymuje się na wejściu x. Korzystanie z nieco innej notacji dla powyższych dwóch funkcji, możemy podsumować to wszystko, co następuje:
def halts(f, x):
def f_prime(n): f(n); return 1
def g(n): return 1 if n == x else f_prime(n)
return equiv(f_prime, g) # If only equiv would actually exist...
Ja też wrzucić na ilustrację dowodu w Haskell (GHC wykonuje pewne wykrywanie pętli, a nie jestem pewien, czy wykorzystanie seq jest głupi dowód w tej sprawie, ale w każdym razie):
-- Tells whether two functions f and g are equivalent.
equiv :: (Integer -> Integer) -> (Integer -> Integer) -> Bool
equiv f g = undefined -- If only this could be implemented :)
-- Tells whether f halts on input x
halts :: (Integer -> Integer) -> Integer -> Bool
halts f x = equiv f' g
where
f' n = f n `seq` 1
g n = if n == x then 1 else f' n
+1 za zgodę ze mną, ale z sexy matematyki. – chaos
+1, ale to nasuwa kolejne pytanie: Jaki jest minimalny zestaw ograniczeń koniecznych, aby można było o tym decydować?Oczywiście, jeśli zestaw wejściowy jest zdefiniowany jako wystarczająco mały i wprowadzono ograniczenie czasu wykonania, obie funkcje mogą być brutalnie wymuszone. – l0b0
"Kiedy jest coś równego jakiejś innej rzeczy" - www.math.harvard.edu/~mazur/preprints/when_is_one.pdf – nlucaroni