структурной индукция для многоходовых (Rose) дерев

Question

Так как многоходовых дерева может быть определена как рекурсивный тип:

data RoseTree a = Node {leaf :: a, subTrees :: [RoseTree a]} 

является ли соответствующим принципом для осуществления структурной индукции по этому типу?

Answer 1

Чтобы указать, что свойство P справедливо для всех (*) выросли деревья, вы должны доказать, что

• если l :: [RoseTree] список розовых деревьев, элементы которых удовлетворяют P и x :: a произвольно, то Note x l удовлетворяет P

часть о P холдинга на элементах l является гипотеза индукции, которую вы можете использовать, чтобы доказать P(Node x l).

Здесь нет явного базового аргумента: это потому, что нет явного конструктора базового аргумента. Тем не менее, Node x [] действует как неявный базовый регистр для деревьев, и действительно, когда l пуст, мы получаем неявный базовый случай для индукции. Конкретно, гипотеза «все элементы l удовлетворяют P» становится незаменимой, когда l пуст, поэтому мы получаем P(Node x []) из принципа индукции выше.

(*) Точнее, этот принцип доказывает P для каждого дерева с высокой глубиной. Если вам действительно нужно рассматривать бесконечно-глубинные (например, круговые деревья), вам нужна монетация.