Strukturelle Induktion auf Binär-Bäume

Question

Betrachten wir die folgenden Funktionsdefinitionen:


data Tree a = Leaf a | Node a (Tree a) (Tree a)


sumLeaves :: Tree a -> Integer

sumLeaves (Leaf x) = 1

sumLeaves (Node _ lt rt) = sumLeaves lt + sumLeaves rt


sumNodes :: Tree a -> Integer

sumNodes (Leaf x) = 0

sumNodes (Node _ lt rt) = 1 + sumNodes lt + sumNodes rt

Nun wollen wir mittels struktureller Induktion beweisen, dass für alle endlichen Bäume t :: Tree a gilt:

sumLeaves t = sumNodes t + 1

Ich habe:

sumLeaves t = sumNodes t + 1

I.A. t = (Tree 0) = (Leaf 0)

sumLeaves (Leaf 0) = 1 sumNodes (Leaf 0) + 1

                                                            0 + 1 = 1

                             1 = 1

I.V.: Wir nehmen an, dass die Aussage für ein beliebiges t gilt.

I.S.:

Was ist nun der Induktionsschritt, ich habe wirklich Probleme, diesen letzten Schritt zu lösen.

Answer 1

Der Induktionsschritt besteht darin, zu zeigen, dass die Aussage für einen beliebigen Baum t gilt, wenn sie für alle seine Unterbäume gilt. Daher müssen Sie zeigen, dass:

sumLeaves t = sumNodes t + 1

gilt, wenn es für die linken und rechten Unterbäume von t gilt.

Um dies zu tun, können Sie die Definitionen der Funktionen sumLeaves und sumNodes verwenden, um die Ausdrücke für den übergeordneten Baum t in Bezug auf die Ausdrücke für die linken und rechten Unterbäume zu schreiben.

Für den Fall, dass t ein Node-Knoten ist, hat sumLeaves t die Form:

sumLeaves (Node _ lt rt) = sumLeaves lt + sumLeaves rt

und sumNodes t die Form:

sumNodes (Node _ lt rt) = 1 + sumNodes lt + sumNodes rt

Da die Aussage für die linken und rechten Unterbäume gilt, dann haben wir:

sumLeaves lt = sumNodes lt + 1

sumLeaves rt = sumNodes rt + 1

Wir ersetzen diese Ausdrücke in die Ausdrücke für den übergeordneten Baum t:

sumLeaves (Node _ lt rt) = sumLeaves lt + sumLeaves rt

= (sumNodes lt + 1) + (sumNodes rt + 1)

= sumNodes lt + sumNodes rt + 2

Auf der anderen Seite

sumNodes (Node _ lt rt) = 1 + sumNodes lt + sumNodes rt

Daher

sumLeaves (Node _ lt rt) = sumNodes (Node _ lt rt) + 1

Dies zeigt, dass die Aussage für den übergeordneten Baum t gilt, wenn sie für die linken und rechten Unterbäume gilt. Daher gilt die Aussage für alle endlichen Bäume t.