如何比較兩個函數的等價性，如（λx.2* x）==（λx.x+ x）？

有沒有辦法比較兩個函數的相等性？例如，(λx.2*x) == (λx.x+x)應該返回true，因爲這些顯然是等價的。如何比較兩個函數的等價性，如（λx.2* x）==（λx.x+ x）？

來源

2013-06-11 MaiaVictor

你真的需要運算功能還是你只是好奇比較的功能呢？在後一種情況下，請看類型化的lambda結石的標準化。 – lukstafi

@lukstafi只是好奇，但我會看看它。 – MaiaVictor

你的連接詞「but」不合適，應該是「so」。 ;-) – lukstafi

118

這幾乎衆所周知，一般功能平等是一般不可判定的，所以你必須選擇那些你感興趣的問題的一個子集，你可能會考慮一些局部的解決方案：

Presburger arithmetic是一階邏輯+算術的可判定片段。
universe包爲有限域的全部函數提供功能相等測試。
您可以檢查您的函數在大量輸入上是否相等，並將其視爲未測試輸入上的相等證據;退房QuickCheck。
SMT求解器盡最大努力，有時會回答「不知道」而不是「相等」或「不相等」。在Hackage上對SMT解決方案有幾種綁定;我沒有足夠的經驗來推薦最好的，但Thomas M. DuBuisson建議sbv。
在緊湊函數上決定函數相等和其他事情的研究有趣;該研究的基礎知識在博客文章Seemingly impossible functional programs中進行了描述。（請注意，緊湊是一個非常強大和非常微妙的條件！它不是大多數Haskell函數都能滿足的。）
如果您知道函數是線性的，則可以找到源空間的基礎;那麼每個函數都有一個獨特的矩陣表示。
您可以嘗試定義自己的表達式語言，證明等效性對於此語言是可決定的，然後將該語言嵌入到Haskell中。這是最靈活，但也是最難取得進展的方式。

來源

2013-06-11 14:06:30

你確定他不只是在尋找sbv還是快速檢查？使用SBV：'證明$ \（x :: SInt32） - > 2 * x。== x + x'產生'Q.E.D.' –

@ ThomasM.DuBuisson很好的建議！我會將其添加到答案中。 –

我實際上是在尋找更深入的問題概覽，而這正是Daniel所提供的。 – MaiaVictor

除了在另一個答案中給出的實際例子之外，讓我們選擇在類型化lambda演算中可表達的函數的子集;我們也可以允許產品和總和類型。儘管檢查兩個函數是否相同可以像applying them to a variable and comparing results一樣簡單，但我們不能構建相等函數within the programming language itself。

ETA：λProlog是一種邏輯編程語言，用於操作（類型化的lambda微積分）函數。

來源

2013-06-11 18:33:41 lukstafi

+1偉大的鏈接！ – luqui

你說，「檢查兩個函數是否相等可以像將它們應用於變量和比較結果一樣簡單」。儘管如此，我很難相信這一點。作爲一個簡單的例子，這是否真的驗證了相等'（\ x - > 2 * x）==（\ x - > x * 2）'？ –

「（\ x - > 2 * x）==（\ x - > x * 2）」並不一定是真的，它取決於您如何解釋「*」和「2」。例如，您可以將基礎條件中的「==」定義爲某個術語重寫系統的標識。 – lukstafi

2年過去了，但我想在這個問題上添加一點點評論。最初，我問是否有任何方法可以告訴(λx.2*x)是否等於(λx.x+x)。現在

add = (a b c -> (a b (a b c))) 
mul = (a b c -> (a (b c)))

，如果您正常化以下條款：加法和乘法的λ演算可以被定義爲

add_x_x = (λx . (add x x)) 
mul_x_2 = (mul (λf x . (f (f x)))

你得到：

result = (a b c -> (a b (a b c)))

對於這兩種方案。由於它們的正常形式是平等的，所以這兩個節目顯然是平等的雖然這一般不起作用，但它在實踐中可以用於很多條款。例如，(λx.(mul 2 (mul 3 x))和(λx.(mul 6 x))都具有相同的標準形式。

來源

2015-08-02 20:48:21 MaiaVictor

有一種叫做「超級編譯」的技術（我推薦[this]（http://community.haskell.org/~ndm/temp/supero.pdf）論文）。我想一個成熟的超級編譯器可以統一你的函數，即使它們是通過遞歸和模式匹配來定義的。 – user3237465

這是一般的不可判定的，而是一個合適的子集，可以有效地使用SMT求解器確實做到今天：

$ ghci 
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help 
Prelude> :m Data.SBV 
Prelude Data.SBV> (\x -> 2 * x) === (\x -> x + x :: SInteger) 
Q.E.D. 
Prelude Data.SBV> (\x -> 2 * x) === (\x -> 1 + x + x :: SInteger) 
Falsifiable. Counter-example: 
    s0 = 0 :: Integer

有關詳細信息，請參閱：https://hackage.haskell.org/package/sbv

來源

2017-09-13 20:32:05

與符號計算語言像數學：

或C＃與computer algebra library：

MathObject f(MathObject x) => x + x; 
MathObject g(MathObject x) => 2 * x; 

{ 
    var x = new Symbol("x"); 

    Console.WriteLine(f(x) == g(x)); 
}

上面的控制檯顯示'True'。

來源

2017-09-14 21:28:22 dharmatech

但是，然而'（x \ [函數] x + x）==（y \ [函數] 2 y）'是在撒謊，它甚至不嘗試。 – tfb

-1

證明兩個函數相等是一般不可判定的，但在特殊情況下仍然可以證明函數相等，就像在你的問題中一樣。

下面是精益

def foo : (λ x, 2 * x) = (λ x, x + x) := 
begin 
    apply funext, intro x, 
    cases x, 
    { refl }, 
    { simp, 
    dsimp [has_mul.mul, nat.mul], 
    have zz : ∀ a : nat, 0 + a = a := by simp, 
    rw zz } 
end

一個樣本證明可以做其他的依賴性類型的語言，如勒柯克，阿格達，伊德里斯相同。

以上是戰術風格證明。獲取生成foo（證明）的實際定義是由手工寫得相當拗口：

def foo : (λ (x : ℕ), 2 * x) = λ (x : ℕ), x + x := 
funext 
    (λ (x : ℕ), 
    nat.cases_on x (eq.refl (2 * 0)) 
     (λ (a : ℕ), 
      eq.mpr 
      (id_locked 
       ((λ (a a_1 : ℕ) (e_1 : a = a_1) (a_2 a_3 : ℕ) (e_2 : a_2 = a_3), congr (congr_arg eq e_1) e_2) 
        (2 * nat.succ a) 
        (nat.succ a * 2) 
        (mul_comm 2 (nat.succ a)) 
        (nat.succ a + nat.succ a) 
        (nat.succ a + nat.succ a) 
        (eq.refl (nat.succ a + nat.succ a)))) 
      (id_locked 
       (eq.mpr 
        (id_locked 
        (eq.rec (eq.refl (0 + nat.succ a + nat.succ a = nat.succ a + nat.succ a)) 
         (eq.mpr 
          (id_locked 
           (eq.trans 
           (forall_congr_eq 
            (λ (a : ℕ), 
             eq.trans 
             ((λ (a a_1 : ℕ) (e_1 : a = a_1) (a_2 a_3 : ℕ) (e_2 : a_2 = a_3), 
              congr (congr_arg eq e_1) e_2) 
              (0 + a) 
              a 
              (zero_add a) 
              a 
              a 
              (eq.refl a)) 
             (propext (eq_self_iff_true a)))) 
           (propext (implies_true_iff ℕ)))) 
          trivial 
          (nat.succ a)))) 
        (eq.refl (nat.succ a + nat.succ a))))))

來源

2017-09-15 11:04:10

爲什麼downvote？ – MaiaVictor

如何比較兩個函數的等價性，如（λx.2* x）==（λx.x+ x）？

回答

相關問題