Jak porównać dwie funkcje równoważności, jak w (λx.2 * x) == (λx.x + x)?

Question

Czy istnieje sposób na porównanie dwóch funkcji równości? Na przykład: (λx.2*x) == (λx.x+x) powinien zwrócić wartość true, ponieważ są one oczywiście równoważne.

Answer 1

to całkiem dobrze wiadomo, że ogólna równość funkcja jest nierozstrzygalny w ogóle, więc trzeba wybrać podzbiór problemu, który Cię interesuje Można rozważyć niektóre z tych rozwiązań cząstkowych.

• Presburger arithmetic jest rozstrzygającym fragmentem logiki pierwszego rzędu + arytmetyki.
• Pakiet universe oferuje funkcje kontroli równości dla wszystkich funkcji z skończoną domeną.
• Możesz sprawdzić, czy twoje funkcje są równe na całej masie wejść i traktować to jako dowód równości na nieprzetestowanych wejściach; sprawdź QuickCheck.
• Twórcy SMT dokładają wszelkich starań, czasami odpowiadając "nie wiem" zamiast "równy" lub "nie równy". Istnieje kilka powiązań z rozwiązaniami SMT w hakowaniu; Nie mam wystarczającego doświadczenia, aby zaproponować najlepszy, ale Thomas M. DuBuisson sugeruje sbv.
• Istnieje zabawna linia badań nad decydowaniem o równości funkcji i innych rzeczach na kompaktowych funkcjach; podstawy tego badania opisano w poście na blogu Seemingly impossible functional programs. (Zwróć uwagę, że zwartość jest bardzo silnym i bardzo subtelnym warunkiem!) Nie jest to funkcja spełniająca większość funkcji Haskell.)
• Jeśli wiesz, że twoje funkcje są liniowe, możesz znaleźć podstawę dla przestrzeni źródłowej; wtedy każda funkcja ma unikalną reprezentację macierzy.
• Możesz spróbować zdefiniować własny język ekspresji, udowodnić, że równoważność jest decydująca dla tego języka, a następnie osadzić ten język w Haskell. Jest to najbardziej elastyczny, ale także najtrudniejszy sposób na osiągnięcie postępu.

Answer 2

Oprócz praktycznych przykładów podanych w innej odpowiedzi, wybierzmy podzestaw funkcji wyrażalnych w typowym rachunku lambda; możemy również pozwolić na typy produktów i sum. Chociaż sprawdzenie, czy dwie funkcje są równe, może być tak proste jak applying them to a variable and comparing results, nie możemy zbudować funkcji równości within the programming language itself.

ETA: λProlog to logiczny język programowania służący do manipulowania (typem lambda) funkcjami.

Answer 3

Minęły 2 lata, ale chcę dodać małą uwagę na to pytanie. Pierwotnie zapytałem, czy jest jakiś sposób, aby stwierdzić, czy (λx.2*x) jest równa . Dodawania i mnożenia na X-rachunku można zdefiniować jako:

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

Teraz, jeśli znormalizować następujących warunkach:

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

Otrzymasz:

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

Dla obu programów. Ponieważ ich normalne formy są równe, oba programy są oczywiście równe. Chociaż to nie działa w ogóle, działa w praktyce na wielu warunkach. (λx.(mul 2 (mul 3 x)) i (λx.(mul 6 x)) oba mają takie same zwykłe formularze, na przykład.

Answer 4

To jest nierozstrzygalny w ogóle, ale dla odpowiedniego podzbioru, można rzeczywiście zrobić to dzisiaj skutecznie używając rozwiązują 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 

uzyskać szczegółowe informacje, patrz: https://hackage.haskell.org/package/sbv

Answer 5

W języku z obliczeń symbolicznych jak Mathematica:

lub C# z 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)); 
} 

Powyższe wyświetla "Prawda" na konsoli.

Answer 6

Udowodnienie, że dwie funkcje są sobie równe, jest ogólnie nierozstrzygalne, ale nadal można udowodnić funkcjonalną równość w szczególnych przypadkach, tak jak w pytaniu.

Oto próbka dowód w 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 

można zrobić to samo w inny sposób zależny od języka pisanego, takich jak Coq, Agda, Idris.

Powyższe ma charakter taktyczny. Rzeczywista definicja foo (dowód), który pobiera generowany jest dość kęs być napisane ręcznie:

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