Ecrire une preuve pour un algorithme
Salut les gars je suis en train de comparer les 2 algorithmes et de la pensée que je peut l'essayer et d'écrire une preuve pour eux!!!!! (mes maths suce donc la question)
Normalement dans notre leçon de maths de l'année dernière nous serait donnée à une question comme
prouver: (2r + 3) = n (n + 4)
puis je ferais le nécessaire 4 étapes et obtenir la réponse à la fin
Où je suis coincée se révèle prims et Kruskals - comment puis-je obtenir ces algorithmes dans une forme comme les mathématiques l'un au-dessus afin que je puisse procéder à prouver
note: je ne suis pas de demander aux gens de répondre pour moi - viens m'aider à l'obtenir en une forme où je peux avoir un aller moi-même
grâce
source d'informationauteur sonny
Vous devez vous connecter pour publier un commentaire.
De prouver l'exactitude de l'algorithme, vous avez l'habitude de montrer (a) qu'il se termine et (b) que sa production répond à la spécification de ce que vous essayez de faire. Ces deux épreuves seront assez différentes de la algébrique des preuves que vous mentionnez dans votre question. Le concept clé que vous avez besoin est induction mathématique. (C'est la récursivité pour les épreuves.)
Prenons quicksort comme un exemple.
De prouver que quicksort se termine toujours, vous avez d'abord montrer qu'il se termine pour l'entrée de longueur 1. (C'est trivialement vrai.) Montrons ensuite que si elle met fin, pour la saisie de la longueur jusqu'à npuis il s'arrêtera pour la saisie de la longueur n+1. Grâce à l'induction, c'est suffisant pour prouver que l'algorithme se termine pour toutes les entrées.
De prouver que quicksort est correcte, vous devez convertir la norme de comparaison de tri précis à l'aide du langage mathématique. Nous voulons la sortie à un permutation de l'entrée de telle sorte que si je ≤ j puis i ≤ j. Prouvant que la sortie de quicksort est une permutation de l'entrée est facile, car il commence à l'entrée et à seulement swaps éléments. Prouvant que la deuxième propriété est un peu plus délicat, mais encore une fois, vous pouvez utiliser l'induction.
Vous ne donnez pas beaucoup de détails mais il y a une communauté de mathématiciens (Mathématiques de Gestion des Connaissances MKM) qui ont développé des outils à l'appui de l'ordinateur épreuves de mathématiques. Voir, par exemple:
http://imps.mcmaster.ca/
et la dernière conférence
http://www.orcca.on.ca/conferences/cicm09/mkm09/
Je ne pense pas que vous pouvez directement. Au lieu de cela, prouver que de générer à la fois une MST, puis prouver que deux MST sont égaux ( ou l'équivalent, puisque vous pouvez avoir plus d'une MST pour certains graphiques ). Si les deux algorithmes génèrent des MSTs, qui se sont avérés être équivalent, ensuite, les algorithmes sont équivalents.
De mon en mathématiques à l'école à l'université, j' (vaguement), n'oubliez pas de prouver Prims et Kruskals algorithmes - et vous n'avez pas l'attaquer par écrit dans une forme mathématique. Au lieu de cela, vous prenez prouvé théories pour les Graphiques et les combiner entre elles, par exemple http://en.wikipedia.org/wiki/Prim%27s_algorithm#Proof_of_correctness pour construire la preuve.
Si vous cherchez à prouver la complexité, puis tout simplement par le travail de l'algorithme est O(n^2). Il y a quelques optimisations pour le cas particulier où le graphe est peu dense ce qui peut réduire cela à O(nlogn).
La plupart du temps la preuve dépend du problème que vous avez dans votre main. Simple argument peut suffire à certains moments, à certains autres moments, vous pourriez besoin de preuve rigoureuse. Une fois, j'ai utilisé un corollaire et la preuve de la déjà fait la preuve de théorème de justifier mon algorithme est droit. Mais c'est pour un projet de collège.
Peut-être vous voulez essayer un semi-automatique preuve de méthode. Il suffit d'aller pour quelque chose de différent 😉 Par exemple, si vous avez une spécification Java de Prim et de Kruskal les algorithmes de manière optimale, construit sur le même modèle graphique, vous pouvez utiliser le La Clé De L'Étalon pour prouver l'équivalence de l'algorithme.
La partie cruciale est de formaliser votre obligation de preuve dans une Logique Dynamique (c'est une extension de la logique du premier ordre avec des types et des moyens de la symbolique de l'exécution de programmes Java). La formule à prouver pourrait correspondre à la suivante (sommaire) modèle:
Ceci exprime que pour tous les graphes, les deux algorithmes fin et le résultat est le même arbre.
Si vous êtes chanceux et que votre formule (et des implémentations d'algorithmes) sont à droite, puis sur la Touche peut le prouver automatiquement pour vous. Si non, vous pourriez avoir besoin d'instancier certaines variables quantifiées qui fait qu'il est nécessaire d'inspecter la démonstration précédente arbre.
Après avoir prouvé la chose avec la Clé, vous pouvez être heureux d'avoir appris quelque chose ou essayer de reconstruire un manuel de preuve à partir de la Clé de la preuve - ce qui peut être une tâche fastidieuse puisque les connaît beaucoup de règles spécifiques à Java, qui ne sont pas faciles à comprendre. Cependant, peut-être vous pouvez faire quelque chose comme de l'extraction d'une Herbrand disjonction de termes Clés utilisées pour instancier des quantificateurs existentiel à la droite de sequents dans la preuve.
Bien, je pense que la Clé est un outil intéressant et plus les gens devraient s'habituer à prouver critique de code Java à l'aide d'outils comme ça 😉