如何編寫一個函數判斷兩個函數是否相等？

01-05

函數狹指計算機編程意義上的函數，擁有0個或以上的輸入值和1個輸出值。
對於兩個函數而言，f與g相等等價於如下條件：
－對於所有可能的輸入，f和g都會得到相同的輸出。

兩個函數相等的可能性包括但不限於：
1，它們具有相同的表達式(代碼)。
2，某一函數連續使用了原函數和反函數。
已知某一函數的代碼可以被其他函數所讀取，問：
如何編寫一個可以在有限步驟內執行的函數，輸入兩個函數f和g，判斷f和g是否相等，然後輸出一個布爾值？
如果不能，如何證明？
追問：在一些在線數學作業和題目中(比如webassign)，有些題目在解答框中需要輸入一個表達式(往往帶有變數x，n等)，而只要輸入的表達式同答案等價，一般都能作為正確答案通過，那麼此類程序是如何判斷表達式相等的呢？

理論上是不可以的.

但否定的答案多沒意思. 我就見識過可以檢測函數的等價性的"黑科技".

卡耐基梅隆有一個本科生的系統入門課. 它的第一次作業是熟悉位運算, 要你用儘可能少的指定操作符實現別的操作符. 在這可以看一下作業要求. 比如第一題, "bitAnd(x,y) xy using only ~ and |". 就是只能使用~或者|至多8次實現. 怎麼寫就折騰去吧. 那麼問題來了, 老師怎麼知道你寫的函數是正確的?

暴力搜么? 那可是2^32 * 2^32 = 2^64 的輸入空間. 不太現實.

老師們用了一個鬼東西叫Binary_decision_diagram. BDD表示的就是布爾函數. 布爾函數的輸入是好幾個位變數, 也就是只能取0或者1, 輸出是一個位變數. 最簡單的表示布爾函數的數據結構就是真值表. 但是普通的真值表的大小隨著輸入變數的個數指數級爆炸, 不科學. BDD就是高度壓縮後的真值表, 去掉了冗餘. 並且BDD有一個很好用的屬性就是兩個布爾函數如果數學上相等, 他們的BDD表示是一樣的. 所以老師們乾的事就是把學生寫的函數和標準答案都轉化成BDD, 然後看一下兩個BDD是不是相等就收工了. 具體怎麼把函數轉化成BDD的, 見這個PPT.

當然, 這種做法有他的局限, 複雜的數據結構和操作符會讓BBD的大小爆炸!

下面是作業中一個謎題的代碼, 將int轉換成float. BDD可以判斷這個函數是不是跟標答等價.

unsigned float_i2f(int x) { int e; unsigned char drop; /* store the bits we drop */ unsigned significand; unsigned carry = 0; unsigned mask = 0x300;


    if (x) {

        if (x &> 0) {

            e = 0x4f000000;

        } else {

            e = 0xcf000000;

            x = -x;

        }
        while (1) {

            if (x &>&> 31)

                break;

            x = x &<&< 1;
            e = e - 0x800000;
        }

        x = x &<&< 1;
        significand = x;
        significand = significand &>&> 9;
        drop = x; // save 1  op

switch (x mask) { case 0x300: // 1|1drop carry = 1; break; case 0x100: // 0|1drop if (drop) carry = 1; break; case 0x200: case 0x000: break; } return (e | significand) + carry; } else { return 0; }

編寫出一個程序判斷連個函數是否相等是不可能的，因為這是一個不可判定問題。

我假設你已經知道了停機定理：

$varphi_{a}$ 代表一個圖靈機（程序）， $a$ 是它演算法的編碼。 $varphi _{a}(x)=y$ 表示 $varphi_{a}$ 在輸入 $x$ 時會停機並輸出 $y$ 。則不存在圖靈機 $Phi$ ，使得 $Phi (a,x)=1$ 如果 $varphi_{a}(x)$ 停機； $Phi (a,x)=0$ 如果 $varphi_{a}(x)$ 不停機。

簡單地給一個證明：我們用反證法，先假設這樣的演算法 $Psi$ 存在：

$Psi (f,g)=1$ 如果 $f=g$ ；

$Psi(f,g)=0$ 如果 $f e g$ 。

我們再構造一個判斷停機問題的演算法。給定了一個 $varphi_{a}(x)$ ，

先構造函數 $f$ ， $f$ 是一個在任意輸入下都只輸出0的函數。

然後根據 $varphi_{a}(x)$ 構造 $g$ ：

$g(n)=0$ 如果 $varphi_{a}(x)$ 在圖靈機運行的 $n$ 步以內沒有停機；

$g(n)=1$ 如果 $varphi_{a}(x)$ 在圖靈機運行的 $n$ 步以內已經停機。

此時我們有：

$Psi (f,g)=1$ 當且僅當 $f=g$ 當且僅當 $varphi_{a}(x)$ 不停機當且僅當 $Phi (a,x)=0$ ；

$Psi(f,g)=0$ 當且僅當 $f e g$ 當且僅當 $varphi_{a}(x)$ 會停機當且僅當 $Phi (a,x)=1$ 。

證畢。

可以將停機問題歸約到這個問題。

證明：

function φ(function a, function b)://原問題求解程序 if(a equals b): return 1 return 0


function zero()://全0函數

   return 0
function Gen(var i, function a)://產生a輸入為i時的模擬程序

   temp = new function{

      a(i)

      return 0

   }

   return temp

function S(var i, function a)//求解停機問題 return φ(Gen(i,a),zero)

顯然上述代碼中的S函數可以求解停機問題，但這與停機問題不可解相矛盾！

廣義上的這類判斷是不能的。對於計算機編程意義的函數，即給定輸入，得到一個輸出（或出錯、死循環以致沒有輸出）的一段代碼，這等價於一個圖靈機概念，根據停機問題的證明結果，無法編寫一個函數來（根據讀取另一函數的代碼）判斷另一函數是否能否停機。所以更不可能判斷兩個函數是否等價了：首先連判斷函數是否能得到「1個輸出值」都已無法做到。

程序等價性不可判定。另外「等價」也有不同定義，語法/語義等價，內涵/外延等價等等。。

但是有很多情況還是可以的，比如某種lambda演算的contextual equivalence什麼的。。

舉個用SMT solver + 命令式語言的例子。。判斷以下2個函數的等價性（函數的「」in-out關係「」等價）

int power3(int in) { int i, out_a; out_a = in; for (i = 0; i &< 2; i++) out_a = out_a * in; return out_a; } int power3_new(int in) { int out_b; out_b = (in * in) * in; return out_b; }

可以簡單地做循環展開，然後用邏輯公式來encode程序語義（需要引入中間變數）。以上兩個程序分別編碼為 $varphi_a, varphi_b$

$egin{align} out0_a = in land \ out1_a = out0_a * in land \ out2_a = out1_a * in end{align}$

$out0_b = (in * in) * in$

1. 邏輯 $mathcal{L}$ 需要建模Fixed-width integer和*，正巧 QF_BV(quantifie-free bitvector theory)剛好適合（複雜度NEXP-complete）。等價性就轉化為判斷以下公式的Validity（可以轉化為Satisfiability）

$varphi_a land varphi_b Rightarrow out2_a = out0_b$

2. 比較取巧的，對於這個例子，其實可以用QF_EUF(theory of equality with uninterpreted function) (複雜度NP-complete)：把*換成uninterpreted function $G$ ，得到 $varphi^{EUF}_a , varphi^{EUF}_b$

$egin{align} out0_a = in land \ out1_a = G(out0_a, in) land \ out2_a = G(out1_a, in) end{align}$

$out0_b = G(G(in, in), in)$

對應地，得到

$varphi^{EUF}_a land varphi^{EUF}_b Rightarrow out2_a = out0_b$

關於函數判等不可計算這件事，其他答主已經講的很清楚了，下面回答一下追問的問題:為什麼存在一些程序可以判斷表達式相等？

其實不能再簡單了:

在允許一些誤差的情況下，這些系統一般是通過test case來進行大概的判斷:即在式子中帶入一些預先構造的或者是隨機生成的測試輸入，判斷結果是否相等即可。

不信你可以構造一個明顯會導致運算溢出但是最終結果正確的算式試一下。

這其實就是邱奇提出的一種不可計算問題：如何判斷兩個lambda表達式等價。這個問題的提出還早於停機問題。

這東西和停機問題等價啊。。。

這是不可能的。在函數式編程中，函數是一等公民，但是從來沒有見過支持他們比較的算符。如果可以的話，語言設計者一定會加入這麼一個操作的。

除了停機問題，還可以這麼想：大部分數學定理都可以表達成一個帶有變數的等式，那麼把等式兩邊拆成兩個函數（如果某側是常量，那麼它其實是常函數；常函數也是函數），假如真有一個程序能機械判斷兩個函數是否等價，那麼還要數學家去挖空心思找證明幹什麼？

數學基本法則之一就是正面對抗無窮（證明無窮集上的元素都有或沒有某個屬性）往往是徒勞的，必須啟發式地迂迴作戰（用人類智慧來證明定理）

可以證明不存在這樣的演算法。下面用C語言代碼輔助說明。

假設存在一個演算法能判斷任意兩個函數是否等價，如下：

bool judgeAlgoEql(void* fun1,void* fun2){ ...... }

那麼可以構造出兩個函數，使得judgeAlgoEql對這兩個函數是否等價做出錯誤的判定，那麼這就和假設矛盾了，從而證明了judgeAlgoEql並不存在。

這兩個破壞性的函數是這樣的：

int satanFun1(void* fun1,void* fun2){ if((fun1==santaFun1)(fun2==satanFun2)){ if(judgeAlgoEql(fun1,fun2)) return 1; } return 0; }

int satanFun2(void* fun1,void* fun2){ if((fun1==santaFun1)(fun2==satanFun2)){ if(judgeAlgoEql(fun1,fun2)) return 2; } return 0; }

好了，現在調用 judgeAlgoEql(satanFun1, satanFun2) 來判定satanFun1,satanFun2是否等價。

假設judgeAlgoEql判定satanFun1,satanFun2等價，那麼可以得出satanFun1(satanFun1, satanFun2)的值為1，satanFun2(satanFun1, satanFun2)的值為2，所以satanFun1,satanFun2不等價。

假設judgeAlgoEql判定satanFun1,satanFun2不等價，那麼對於任意輸入satanFun1的值為0，對於任意輸入satanFun2的值也為0，所以satanFun1,satanFun2是等價的。

總之，judgeAlgoEql對satanFun1,satanFun2是否等價不能做出正確的判定。

所以judgeAlgoEql是不存在的。

其實其它答主忽略了一點：雖然針對圖靈機的函數判等是不可行的，但是由於現實中的計算機並不能真正handle無窮——也就是真實計算機的狀態數是有限的，所以對於某一函數，合法的輸入是可枚舉的，所以判斷函數等價事實上在邏輯的層面是可行的——雖然可計算性會分分鐘糊你一臉

-_-誰知道手機搜狗怎麼打分割線-_-

昨天我忘記加對問題的限定了，我把問題私自篡改為在某台具體的電腦上兩個函數表現為等價能不能被判定——不過問題里可沒有限定在那台計算機上跑這個判定程序——所以你大可以理解為上帝造了一台速度和內存都無窮大的玩意來，反正你要是用數學證明也可以看做是寫了個抽象解釋程序跑在腦袋裡是不……

一一映射

來來來把實數域複數域先窮舉一遍。

如果函數也能處處一致收斂那麼兩函數相等。

這時候有人要打我了，窮舉你怎麼不去上天呢。

占坑，等我把程序編出來打臉。

你這問題一看就是不可能的,點開看果然有人把它規約到停機問題了.

不過你的追問的這種相等判定是可以做到的,只要取採樣點就可以了.例如如果答案是一個多項式,你取超過這個多項式的次數個的採樣,只要在採樣點全相等,那兩個多項式就會相等了.當然這樣的話會誤判一些錯誤答案,但是能輸入這些錯誤答案的人必然也是已經算出正確答案是啥了.

看看這一段

Equality of arrows of sets
Many of the discussion in category theory involves around equality of arrows, but how we test if an arrow f is equal to g?

Two maps are equal when they have the same three ingredients:

domain A

domain B

a rule that assigns f a

Because of 1, we can test for equality for ardors of sets f:A=&>B and g:A=&>B using this test

if for each point a:1=&>A, f a=g a, then f=g

確實，其實也慢直觀的。給定函數的定義域，如果定義域中得每個元素都被映射到值域中得相同元素，那麼這兩個映射自然是相同的。

所以能不能比較出來是不是就是看定義域有多大了？如果定義域不大自然可以比較出來。

那麼問題來了，關停機問題什麼事情呢？

具體到沒有副作用的純函數, 即我們只關注輸入與輸出的話. 並局限在C語言的話, 我認為可能的.

首先, 所有void類型的函數都是等價的. 因為我們只關注輸入輸出.

其次, 對於所有的函數, 只要輸入與輸出的類型是等價的, 譬如int f(int,int,int,int), structA ff(structB,structA,double);

這些函數的輸入輸出數據類型的size都是確定的, 也就是那麼所能取的值也就是有限的,因此只需要檢驗這些有限個狀態下輸入輸出是否等價就好了.

不過上面的做法好像碰到個長度不定的鏈表就不能玩了. 不過如果再把內存大小固定住的話, 還是可以玩的.

綜上所述, 在內存大小確定的情況下, 應當是可以判定兩個函數是否等價的

沒玩過oj嗎？給一定量的測試數據，過了就行了。

你們說的都好高深啊。

如果只是（腳本語言或者可以反編譯）並且只看錶達式是否相同的話。

1、找到這兩個函數所在的文件。

2、以（反編譯後的）文件形式讀取這兩個文件的源碼。

3、正則匹配出兩個函數表達式（反函數看情況其實也能正則過濾掉）。

4、匹配字元串相等。

5、逃

題外話，其實我認為函數只有代碼完全一樣的情況下才能相等，因為如果用了反函數還是什麼其他的東西，代碼的實際業務邏輯其實已經改變了，也就是說實際的意義已經改變了，而一個函數就算是完全輸入輸出一致，也不能表示這兩個函數的業務邏輯一致（例如一個函數寫了日誌，另一個函數沒寫，但輸入輸出一致，他們也不能算是一致的）。

另：這個答案只是為了看起來字不那麼少。。。

通過動態分析（執行了函數，看輸出結果）來判等是行不通的，鑒於停機問題——連函數能否停機都不能判斷，更別說判斷函數相等。

通過靜態分析（沒執行函數，看代碼語義）的方法的話就難說了。首先一種情況是函數不是「引用透明」的，調用了隱含的外部變數，比如用於生成隨機數的 entropy source，並影響輸出了，那同樣的函數執行兩遍結果也不一樣，這種情況到底算不算倆函數一樣？假設排除這種情況，函數符合函數式編程的無「副作用」的精神，不讀寫或調用外部變數和函數、保持獨立。編譯器內部可以把單個過程代碼對象構造出控制流圖 CFG，也就是以程序基本塊為節點的有向圖（去年搬的一塊磚就是這個相關的）——如果兩個函數可以構造、歸約出一樣的 CFG 那就是一樣？但內部實現的根本就是兩個演算法，CFG 勢必不同吧。O(n^2) 和 O(lgn) 的演算法肯定不一樣，BFS 和 DFS 肯定不一樣，但它們的輸入和輸出的 map 是一樣的。如果編譯器內部能把 CFG 簡化成最優演算法，那真是神了…硬是要說的話或許真的可能，畢竟 map 是單射…話說函數式編程是最適合拿來做這個事的吧。

符號執行也許可以幫忙，傳送門：s2e/EquivalenceTesting.rst at master · dslab-epfl/s2e · GitHub