Comment comparer deux fonctions pour l'équivalence, comme dans (λx.2*x) == (λx.x+x)?

Est-il un moyen de comparer deux fonctions pour l'égalité? Par exemple, (λx.2*x) == (λx.x+x) doit retourner true, car ceux sont évidemment équivalent.

Avez-vous vraiment besoin de fonctions mathématiques ou êtes-vous simplement curieux au sujet de la comparaison des fonctions? Dans ce dernier cas, jetez un oeil à la normalisation dans tapé lambda calcul.
juste par curiosité, mais je vais jeter un oeil sur elle.
Votre conjonctif "mais" est de sortir de la place, il devrait plutôt être "tellement". 😉
vous avez raison.
connexes: stackoverflow.com/questions/13962811/...
Si vous êtes intéressé dans le calcul de l'égalité (par exemple. pas dans les mathématiques de la théorie contexte) il y a seulement 4 milliards de flotteurs, de sorte que vous pouvez les tester tous les randomascii.wordpress.com/2014/01/27/...
Cela sonne bien, jusqu'à ce que vous voulez prouver l'équivalence de deux fonctions binaires et tout à coup que 4 milliards de dollars taille du domaine est devenu 16 quintillion, et de votre essai de 1 minute suite est devenu un 10000 ans de suite de tests.

InformationsquelleAutor MaiaVictor | 2013-06-11

124

Il est assez bien connu que la fonction générale de l'égalité est indécidable en général, de sorte que vous aurez à choisir un sous-ensemble de la problématique qui vous intéresse. Vous pourriez envisager de certaines de ces solutions partielles:
- L'arithmétique de Presburger est decidable fragment de la logique du premier ordre + arithmétique.
- La univers offre la fonction de tests d'égalité pour le total des fonctions limitées de domaine.
- Vous pouvez vérifier que vos fonctions sont égales sur tout un tas d'entrées et de traiter cela comme une preuve de l'égalité sur la non testé entrées; découvrez QuickCheck.
- Solveurs SMT faire un meilleur effort, parfois ayant répondu "ne sais pas" au lieu de "l'égalité" ou "pas égal". Il y a plusieurs liaisons de solveurs SMT sur Hackage; je n'ai pas assez d'expérience pour proposer un meilleur, mais Thomas M. DuBuisson suggère sbv.
- Il y a un plaisir de la ligne de recherche sur le choix de la fonction de l'égalité et d'autres choses sur compact fonctions; les bases de cette recherche est décrite dans le billet de blog Apparemment impossible de programmes fonctionnels. (Notez que la compacité est un très fort et très subtile condition! Ce n'est pas celui que la plupart des Haskell fonctions satisfaire.)
- Si vous savez que vos fonctions sont linéaires, vous pouvez trouver une base de l'espace source; ensuite, chaque fonction a une unique représentation matricielle.
- Vous pouvez tenter de définir votre propre langage d'expression, de prouver que l'équivalence est decidable pour cette langue, et puis d'intégrer cette langue en Haskell. C'est la plus flexible, mais aussi la voie la plus difficile de faire des progrès.
- Êtes-vous sûr qu'il ne cherche pas seulement pour sbv ou quickcheck? Avec SBV: prove $ \(x::SInt32) -> 2*x .== x + x résultats dans Q.E.D.
- Très bonne suggestion! Je vais l'ajouter à la réponse.
- En fait j'ai été à la recherche pour une meilleure vue d'ensemble du problème, exactement ce que Daniel fourni.
InformationsquelleAutor Daniel Wagner

C'est indécidable en général, mais d'un sous-ensemble, en effet, vous pouvez le faire aujourd'hui efficacement à l'aide de solveurs 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

Pour plus de détails, voir: https://hackage.haskell.org/package/sbv

InformationsquelleAutor alias

11

En outre des exemples concrets donnés dans l'autre réponse, laissez-nous chercher le sous-ensemble de fonctions exprimable dans tapé lambda calcul, nous pouvons également nous laisser le produit et la somme des types. Bien que de vérifier si deux fonctions sont égales peut être aussi simple que en les appliquant à une variable et de comparer les résultats, nous ne pouvons pas construire l'égalité de la fonction dans le langage de programmation lui-même.

ETA: λProlog est une logique de langage de programmation pour manipuler (tapé lambda calcul) de fonctions.
- +1 Grande liens!
- Vous dites, "vérifier si les deux fonctions sont égales peut être aussi simple que de les appliquer à une variable et de comparer les résultats". Je vais avoir du mal à croire cela, mais, comme un exemple simple, serait-ce vraiment valider l'égalité (\x -> 2*x) == (\x -> x*2)?
- "(\x -> 2*x) == (\x -> x*2)" n'est pas nécessairement vrai, cela dépend de comment vous interprétez "*" et "2". Par exemple, vous pouvez définir le"==", sur un sol termes d'identité modulo quelques réécriture de termes de système.
InformationsquelleAutor lukstafi
9

2 ans ont passé, mais je voudrais ajouter un petit mot à cette question. A l'origine, je lui ai demandé si il n'y a aucun moyen de dire si (λx.2*x) est égal à (λx.x+x). L'Addition et la multiplication sur le λ-calcul peut être définie comme:
```
add = (a b c -> (a b (a b c)))
mul = (a b c -> (a (b c)))
```
Maintenant, si vous normaliser les termes suivants:
```
add_x_x = (λx . (add x x))
mul_x_2 = (mul (λf x . (f (f x)))
```
Vous bénéficiez de:
```
result = (a b c -> (a b (a b c)))
```
Pour les deux programmes. Depuis leurs formes normales sont égales, les deux programmes sont évidemment égaux. Bien que cela ne fonctionne pas, en général, il fonctionne pour le nombre de termes dans la pratique. (λx.(mul 2 (mul 3 x)) et (λx.(mul 6 x)) les deux ont les mêmes formes normales, par exemple.
- Il existe une technique appelée "supercompilation" (je recommande ceci papier). Je suppose une maturité supercompiler peut unifier vos fonctions, même si elles sont définies par récurrence et de filtrage.
- Le lien fourni ne fonctionne plus. Ce document de recherche est disponible ici: academia.edu/2718995/Rethinking_supercompilation
- 4 ans ont passé, et je veux ajouter encore une autre remarque: bien que cela fonctionne dans ce cas, une telle chose est que la plupart de l'exception. Les fonctions peuvent être définies sauvagement dans différentes façons et toujours être équivalent, donc une façon de manipuler les égalités manuellement est utile.
InformationsquelleAutor MaiaVictor
2

Dans un langage de calcul symbolique comme Mathematica:

Ou C# avec un algèbre informatique de la bibliothèque:
```
MathObject f(MathObject x) => x + x;
MathObject g(MathObject x) => 2 * x;

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

    Console.WriteLine(f(x) == g(x));
}
```
Ci-dessus affiche "True" dans la console.
- Mais, cependant (x \[Function] x + x) == (y \[Function] 2 y) est un support, il n'essayez même pas.
InformationsquelleAutor dharmatech

Prouvant deux fonctions de l'égalité est indécidable en général, mais on peut encore prouver fonctionnelle de l'égalité dans des cas particuliers comme à votre question.

Voici un exemple de preuve dans le 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

On peut faire la même chose dans d'autres dépendante tapé langue comme le Coq, Agda, Idris.

Ci-dessus est une tactique de style de la preuve. La définition même de foo (la preuve), qui est généré est tout à fait une bouchée à être écrit à la main:

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

Pourquoi le downvote?

InformationsquelleAutor Slavomir Kaslev

Vous devez vous connecter pour publier un commentaire.