Depuis des arbres à plusieurs voies peut être définie comme un type récursif:induction structurelle pour multivoies (rose) arbres
data RoseTree a = Node {leaf :: a, subTrees :: [RoseTree a]}
est là un principe correspondant pour effectuer induction sur ce type?
Affirmer que la propriété P détient pour tous (*) a augmenté les arbres, vous devez prouver que
l :: [RoseTree] est une liste d'arbres roses dont les éléments satisfaire P et x :: a est arbitraire, alors Note x l satisfait Pla partie sur la tenue P sur les éléments de l est l'hypothèse d'induction, que vous pouvez utiliser pour prouver P(Node x l).
Il n'y a pas de cas de base explicite ici: c'est parce qu'il n'y a pas de constructeur de cas de base explicite. Pourtant, Node x [] agit comme un cas de base implicite pour les arbres, et en effet, lorsque l est vide, nous obtenons implicitement un cas de base pour l'induction. Concrètement, l'hypothèse selon laquelle "tous les éléments de l satisfont P" devient vide lorsque l est vide, donc nous obtenons P(Node x []) du principe d'induction ci-dessus.
(*) Plus précisément, ce principe prouve P pour chaque rosier à profondeur finie. Si vous devez vraiment prendre en compte les arbres de profondeur infinie (par exemple les arbres circulaires), vous avez besoin de coinduction.
Pourriez-vous me montrer une explication de coinduction? Ou expliquez-vous vous-même? – dfeuer
@dfeuer Le sujet est assez large. Pour avoir un aperçu, vous pouvez consulter wikipedia pour cela, la corecursion, le théorème de (Knaster-) Tarski, les plus grands points fixes et les coalgebres finales. De plus, la bisimilarité entre les processus d'une algèbre de processus est une notion typique qui implique des preuves par coinduction. Dans le contexte spécifique de la programmation fonctionnelle et de la codata, je suppose que cela peut être utilisé, mais je ne peux pas citer un exemple typique. – chi
@dfeuer Le brillant papier de Andy de 1994 est la référence canonique pour la co-induction en FP, et il est très lisible: http://marcellodesales-cs-research.googlecode.com/svn/trunk/ms-cs-ufcg-brazil /functional-programming/docs/gordon94tutorial.pdf Notez que dans le contexte de Haskell, cela revient essentiellement à prouver P (bottom), puisque les données et les co-données sont les mêmes dans Haskell. –
Vous voulez dire 'Foldable' et' Traversable'? En utilisant '-XDeriveFunctor',' DeriveFoldable', 'DeriveTraversable' et' import Data.Foldable' et 'import Data.Traversable' vous pouvez' dériver (Functor, Foldable, Traversable) 'sur' RoseTree' pour obtenir un 'fold' générique et 'traverse' pour cela. – bheklilr
Merci. Je demandais vraiment en termes de raisonnement sur les structures (comme décrit dans http://en.wikipedia.org/wiki/Structural_induction), plutôt que de faire quoi que ce soit avec les arbres eux-mêmes. –
@RichAshworth Je trouve votre question peu claire. Si vous n'êtes pas intéressé à déclarer une instance 'Foldable' ou' Traversable' pour votre arbre et que tout ce que vous voulez c'est raisonner sur la structure de données (abstraite), pourquoi en montrer une implémentation Haskell? – Jubobs