haskell - (λx.2*x) == (λx.x+x) のように、2 つの関数の同等性を比較する方法は?

Question

2 つの関数が等しいかどうかを比較する方法はありますか? たとえば、(λx.2*x) == (λx.x+x)これらは明らかに同等であるため、true を返す必要があります。

Answer 1

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))

Answer 2

2つの機能が等しいことを証明することは、一般的には決定できませんが、質問のように特別な場合には、機能が等しいことを証明できます。

これがリーンのサンプルプルーフです

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

Coq、Agda、Idris などの他の依存型言語でも同じことができます。

上記は戦術スタイルの証明です。生成される (証明)の実際の定義は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))))))