(λx.2 * x) == (λx.x + x)에서와 같이 동등성을 위해 두 함수를 비교하는 방법은 무엇입니까?

(λx.2 * x) == (λx.x + x)에서와 같이 동등성을 위해 두 함수를 비교하는 방법은 무엇입니까?

---

두 함수가 같은지 비교하는 방법이 있습니까? 예를 들어 (λx.2*x) == (λx.x+x)는 반드시 동일하게 작성해야합니다.

---

일반적인 함수 평등은 일반적으로 있습니다. 따라서 관심있는 문제의 하위 집합을 선택해야합니다. 다음과 같은 부분 솔루션을 고려할 수 있습니다.

• Presburger 산술 은 1 차 논리 + 산술의 결정 가능한 조각입니다.
• 우주 패키지 이벤트 유한 도메인과 전체 기능에 대한 평등 테스트를 작동합니다.
• 함수가 전체 입력에서 동일한 지 확인하고 테스트되지 않은 입력에서 증거로 처리 할 수 ​​있습니다. QuickCheck를 확인하십시오 .
• SMT 솔버는 최선의 노력을 다하며 "같음"또는 "같지"대신 "모름"에 응답합니다. Hackage의 SMT 솔버에 대한 몇 가지 가지 바인딩이 있습니다. 나는 최고의 제안 제안 수준 경험이 없지만 Thomas M. DuBuisson은 sbv를 제안 합니다.
• 함수 평등과 콤팩트 함수에 대한 다른 기능 결정하는 재미있는 연구가 있습니다. 이 연구의 기초는 블로그 포스트에 설명되어 있습니다 . 불가능 해 보이는 기능 현관 프로그램 . (컴팩트 함은 매우 강력하고 미묘한 조건입니다! 대부분의 Haskell 함수가 만족하는 것은 아닙니다.)
• 함수가 선형이라는 것을 알고 있다면 소스 공간의 기초를 사용할 수 있습니다. 모든 함수는 고유 한 표현이 있습니다.
• 자신의 표현 언어를 정의 하고이 언어에 대해 동등 함을 증명할 수 있습니다. 다음 해당 언어를 Haskell에 포함 할 수 있습니다. 이것은 가장 유연하지만 발전하는 가장 어려운 방법이기도합니다.

---

이는 하위 집합의 경우 실제로 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를 참조하십시오.

---

다른 내용에있는 실제 사례 외에도 형식화 된 람다 미적분 표현 된 수있는 함수 하위 집합을 선택하겠습니다. 제품 및 전체 유형도 허용 할 수 있습니다. 두 함수가 같은지 확인 하는 것이 변수에 적용하고 결과를 비교하는 것처럼 간단하게 할 수있는 프로그래밍 언어 자체 내에서 같음 함수를 구축 할 수 없습니다 .

ETA : λProlog 는 (형식화 된 람다 계산법) 함수를 조작하기위한 논리 프로그래밍 언어입니다.

---

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))모두는 예를 들어, 동일한 형태를 포함한다.

---

Mathematica와 같은 기호 계산을 사용하는 언어에서 :

또는 컴퓨터 대수 라이브러리 가있는 C # :

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

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

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

위의 내용은 콘솔에 'True'를 표시합니다.

---

두 기능이 동일하다는 것을 증명하는 것은 일반적으로 가능하지만 질문에서와 같이 특별한 경우에도 기능적 동등 함을 증명할 수 있습니다.

다음은 Lean의 샘플 증명입니다.

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

참고 URL : https://stackoverflow.com/questions/17045941/how-to-compare-two-functions-for-equivalence-as-in-%ce%bbx-2x-%ce%bbx-xx