Учитывая произвольную функцию, f , мы определяем функцию f ', которая возвращает 1 на входе n , если f останавливается на входе n . Теперь для некоторого числа x мы определяем функцию g , которая на входе n возвращает 1 , если n = x , а иначе вызывает f '(n).
Если функциональная эквивалентность была разрешимой, то решение о том, является ли g идентичным f ', решает, останавливается ли f на входе x . Это решило бы проблему остановки . С этим обсуждением связана теорема Райса .
Вывод: функциональная эквивалентность неразрешима.
Ниже обсуждается обоснованность этого доказательства. Итак, позвольте мне подробнее рассказать о том, что делает доказательство, и привести пример кода на Python.
Доказательство создает функцию f ', которая на входе n начинает вычислять f (n) . Когда это вычисление заканчивается, f 'возвращает 1. Таким образом, f' (n) = 1 тогда и только тогда, когда f останавливается на входе n и f ' не останавливается на n если f не останавливается. Python:
def create_f_prime(f):
def f_prime(n):
f(n)
return 1
return f_prime
Затем мы создаем функцию g , которая принимает n в качестве входных данных и сравнивает ее с некоторым значением x . Если n = x , то g (n) = g (x) = 1 , иначе g (n) = f '(n) . Python:
def create_g(f_prime, x):
def g(n):
return 1 if n == x else f_prime(n)
return g
Теперь хитрость в том, что для всех n! = X мы имеем g (n) = f '(n) . Кроме того, мы знаем, что g (x) = 1 . Итак, если g = f ', то f' (x) = 1 и, следовательно, f (x) останавливается. Аналогично, если g! = F ', то обязательно f' (x)! = 1 , что означает, что f (x) не останавливается. Таким образом, решение о том, g = f ' эквивалентно решению о том, останавливается ли f на входе x . Используя немного другое обозначение для двух вышеупомянутых функций, мы можем суммировать все это следующим образом:
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...
Я также добавлю иллюстрацию доказательства в Haskell (GHC выполняет некоторое обнаружение петли, и я не совсем уверен, является ли использование seq в этом случае доказательством дурака, но в любом случае):
-- 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