Với một chức năng tùy ý, f, chúng ta định nghĩa một hàm f' trả về trên đầu vào n nếu f tạm dừng trên đầu vào n. Bây giờ, đối với một số số x chúng ta định nghĩa một hàm g đó, trên đầu vào n, trả nếu n = x, và nếu không gọi f '(n).
Nếu tương đương chức năng đã decidable, sau đó quyết định có g giống hệt f' quyết định liệu f tạm dừng trên đầu vào x. Điều đó sẽ giải quyết được Halting problem. Liên quan đến cuộc thảo luận này là Rice's theorem.
Kết luận: chức năng tương đương là không thể xác định.
Có một số thảo luận dưới đây về tính hợp lệ của bằng chứng này. Vì vậy, hãy để tôi xây dựng trên những gì các bằng chứng hiện, và cung cấp cho một số mã ví dụ trong Python.
Các giấy tờ chứng minh tạo ra một hàm f' mà trên đầu vào n bắt đầu để tính toán f (n). Khi tính toán này kết thúc, f' trả về 1. Như vậy, f '(n) = 1 khi và chỉ khi f tạm dừng trên đầu vào n, và f' không ngừng trên n iff f doesn 't. Python:
def create_f_prime(f):
def f_prime(n):
f(n)
return 1
return f_prime
Sau đó chúng ta tạo một hàm g mà mất n như đầu vào, và so sánh nó với một số giá trị x. Nếu n = x, thì g (n) = g (x) = 1, khác 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
Bây giờ Bí quyết là, mà cho tất cả n = x chúng tôi có mà g (n) = f '(n)!. Hơn nữa, chúng tôi biết rằng g (x) = 1. Vì vậy, nếu g = f ', thì f' (x) = 1 và do đó f (x) tạm dừng. Tương tự, nếu g! = F ' thì nhất thiết phải f' (x)! = 1, có nghĩa là f (x) không dừng lại. Vì vậy, hãy quyết định xem g = f ' có tương đương với việc quyết định xem f tạm dừng trên đầu vào x hay không. Sử dụng một ký hiệu hơi khác nhau cho hai chức năng trên, chúng ta có thể tóm tắt tất cả điều này như sau:
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...
Tôi cũng sẽ quăng trong một minh chứng bằng chứng trong Haskell (GHC thực hiện một số phát hiện vòng lặp, và tôi không thực sự chắc chắn cho dù việc sử dụng các seq là đánh lừa bằng chứng trong trường hợp này, nhưng dù sao):
-- 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 để đồng ý với tôi nhưng với tính toán gợi cảm. – chaos
+1, nhưng điều này đặt ra một câu hỏi khác: Bộ giới hạn tối thiểu cần thiết để đưa ra quyết định này là gì?Rõ ràng, nếu tập hợp đầu vào được xác định là đủ nhỏ, và giới hạn được giới thiệu đến thời gian thực hiện, cả hai hàm đều có thể bị ép buộc. – l0b0
"Khi nào một điều tương đương với một số điều khác" - www.math.harvard.edu/~mazur/preprints/when_is_one.pdf – nlucaroni