是否发现两个函数的等价性是不可判定的？

Question

难道不知道两个函数是否相同吗？例如,编译器编写者想要确定开发人员编写的两个函数是否执行相同的操作,可以使用哪些方法来确定那个函数？或者我们可以做些什么来找出两个TM是相同的？有没有办法规范机器？

编辑:如果一般情况是不可判定的,在正确地说两个函数是等价的之前,您需要多少信息？

Answer 1

给定一个任意函数f,我们定义一个函数f',如果f在输入n上停止,它将在输入n上返回1.现在,对于某个数字x,我们定义一个函数g,如果n = x,则在输入n上返回1,否则调用f'(n).

如果功能等同是可判定的,那么在决定是否克等同于F"决定是否˚F停止对输入X.这将解决停机问题.与此讨论相关的是赖斯定理.

结论:功能对等是不可判定的.

关于这个证明的有效性,下面有一些讨论.让我详细说明证明的作用,并在Python中给出一些示例代码.

1. 证明创建了一个函数f',它在输入n上开始计算f(n).当此计算完成后,F"返回1.因此,F'(n)的 = 1个当且仅当˚F停止输入Ñ,和F’上不停止Ñ当且仅当˚F不.蟒蛇:

   def create_f_prime(f):
       def f_prime(n):
           f(n)
           return 1
       return f_prime
   

2. 然后我们创建一个函数g,它将n作为输入,并将其与某个值x进行比较.如果n = x,则g(n)= g(x)= 1,否则g(n)= f'(n).蟒蛇:

   def create_g(f_prime, x):
       def g(n):
           return 1 if n == x else f_prime(n)
       return g
   

3. 现在的诀窍是,对于所有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

Answer 2

是的,这是不可判定的.这是停止问题的一种形式.

请注意,我的意思是它对于一般情况来说是不可判定的.正如您可以确定停止足够简单的程序一样,您可以确定足够简单的函数的等效性,并且这对于应用程序来说可能是有用的并不是不可想象的.但是,您无法确定任何两个可能函数的等效性的一般方法.

Answer 3

一般情况是不可判定的，正如其他人已经说过的那样（莱斯定理本质上是说图灵完备形式主义的任何非平凡性质都是不可判定的）。

在某些特殊情况下，等价性是可判定的，最著名的例子可能是有限状态自动机的等价性。如果我没记错的话，下推自动机的等价性已经无法通过归约到 Post 的对应问题来确定。

为了证明两个给定的函数是等价的，您需要在某些形式中提供等价证明作为输入，然后您可以检查其正确性。这个证明的基本部分是循环不变量，因为它们不能自动导出。