J'essaie de comparer 2 algorithmes. Je pensais que je peux essayer d'écrire une preuve pour eux. (Mon calcul est nul, alors donc la question.)
Normalement dans notre cours de mathématiques l'an dernier, nous recevrions une question comme Prouvez: (2R + 3) = N (N + 4)
Alors je ferais les 4 étapes nécessaires et obtenez la réponse à la fin.
Où je suis bloqué, c'est prouve Prims et Kruskals - Comment puis-je obtenir ces algorithmes à une forme comme le mathématique ci-dessus, afin que je puisse procéder pour prouver?
Remarque: je ne demande pas aux gens de me répondre pour moi - aidez-moi simplement à me remettre à une forme où je peux avoir un tour moi-même.
6 Réponses :
Vous n'abandonnez pas de nombreux détails, mais il y a une communauté de mathématiciens (gestion des connaissances mathématiques MKM) qui ont développé des outils permettant de soutenir les preuves informatiques de mathématiques. Voir, par exemple:
et la dernière conférence
de mes cours de mathématiques à UNI I (vaguement) N'oubliez pas de prouver des algorithmes Prims et Kruskals - et vous ne l'attaquez pas en l'écrivant sous une forme mathématique. Au lieu de cela, vous prenez des théories éprouvées pour les graphiques et combinez-les par ex. http://fr.wikipedia.org/wiki/prim%27s_algorithmfnof_of_correcnessleightle_/a > pour construire la preuve.
Si vous cherchez à prouver la complexité, alors simplement en fonctionnement de l'algorithme, c'est O (n ^ 2). Il existe certaines optimisations pour le cas particulier où le graphique est rare qui peut réduire ceci à O (nlogn).
Où je suis bloqué est prouve Prims et Kruskals - Comment puis-je obtenir ces algorithmes à une forme comme le mathématique ci-dessus afin que je puisse procéder pour prouver
Je ne pense pas que vous puissiez directement. Au lieu de cela, prouvez que les deux générer un MST, puis prouvent que deux MST sont égaux (ou équivalent, car vous pouvez avoir plus d'un MST pour certains graphiques). Si les deux algorithmes génèrent des MST qui sont montrés équivalents, les algorithmes sont équivalents.
Pour prouver l'exactitude d'un algorithme, vous devez généralement montrer (a) qu'il termine et (b) que ses satisfait de sortie de la spécification de ce que vous essayez de faire. Ces deux épreuves seront assez différentes des preuves algébriques que vous mentionnez dans votre question. Le concept clé dont vous avez besoin est l'induction mathématique . (Il est récursion des preuves.)
Take Let quicksort comme exemple.
Pour prouver que quicksort se termine toujours, vous devez d'abord montrer qu'elle se termine pour l'entrée de la longueur 1. (Ceci est trivialement vrai.) Montrent ensuite que si elle se termine pour l'entrée de la longueur jusqu'à n , il prendra fin pour l'entrée de longueur n + 1 . Merci à induction, cela suffit pour prouver que l'algorithme se termine pour toutes les entrées.
Pour prouver que quicksort est correcte, vous devez convertir la spécification de comparaison de tri à un langage mathématique précis. Nous voulons que la sortie soit une de l'entrée permutation telle que, si i ≤ j alors a i ≤ a j . Prouver que la sortie de quicksort est une permutation de l'entrée est facile, car il commence par les éléments d'entrée et de swaps seulement. Prouver la deuxième propriété est un peu plus délicat, mais encore une fois, vous pouvez utiliser l'induction.
Merci d'avoir partagé ce Jason Orendorff (+1).
La plupart des temps de la preuve dépend du problème que vous avez dans votre main. Argument simple peut suffire parfois, à d'autres moments, vous pourriez Besoin d'une preuve rigoureuse . Une fois, j'ai utilisé un corollaire et une preuve d'un théorème déjà prouvé pour justifier mon algorithme est juste. Mais c'est pour un projet collégial.
Peut-être que vous voulez essayer une méthode de protection semi-automatique. Juste pour aller pour quelque chose de différent;) Par exemple, si vous avez une spécification Java des algorithmes de PRIM et KRUSKAL, bâtiments de manière optimale sur le même modèle de graphique, vous pouvez utiliser le Prouve clé pour prouver l'équivalence de l'algorithme.
La partie cruciale consiste à formaliser votre obligation de preuve dans la logique dynamique (il s'agit d'une extension de la logique de premier ordre avec des types et des moyens d'exécution symbolique de programmes Java). La formule à prouver pourrait correspondre au motif suivant (Sketchy): ceci exprime que pour tous les graphiques, les deux algorithmes se terminent et le résultat est le même arbre. Si vous avez de la chance et que vos formules (et vos implémentations d'algorithme) ont raison, la clé peut la prouver automatiquement pour vous. Sinon, vous pourriez avoir besoin d'instancier certaines variables quantifiées, ce qui permet d'inspecter l'arbre de preuve précédent. Après avoir prouvé la chose avec la clé, vous pouvez être heureux d'avoir appris quelque chose ou d'essayer de reconstruire quelque chose ou d'essayer de reconstruire Une preuve manuelle de la preuve de clé - cela peut être une tâche fastidieuse car la clé connaît beaucoup de règles spécifiques à Java qui ne sont pas faciles à comprendre. Cependant, vous pouvez peut-être faire quelque chose comme une extraction d'une disjonction à Herbrand des termes de la clé utilisée pour instantiaire des quantificateurs existentiels sur le côté droit des séquents de la preuve. Eh bien, je pense que cette clé est une intéressante Outil et plus de personnes devraient s'habituer à prouver un code Java critique à l'aide d'outils tels que ceux;)
Si vous avez prouvé l'algorithme Prim's ou Kruskal dans la clé, j'aimerais le voir! Je ne crois tout simplement pas que tout assistant prouve convient à de telles choses.
essayez mathoverflow.com. Je pense que vous aurez plus de chance là-bas
Je ne pense pas que ce genre de question est ce que Mathoverflow.com est pour.
Je vote pour fermer cette question car il appartient aujourd'hui au cs.stackexchange.com .