Wir wollen folgende Aussage beweisen:

anzahlKnoten baum = (anzahlKanten baum) +1

Die gegebene Datenstrucktur sieht wie folgt aus:

data Baum el = Baum el [(Baum el)] deriving Show

Ich habe folgende Funktionen, zur berechnung der Kanten und Knoten implementiert:

anzahlKnoten :: Baum el -> Int
(1) anzahlKnoten (Baum el []) = 1
(2) anzahlKnoten (Baum el liste) = 1 + anzahlKnoten' liste

anzahlKnoten' :: [(Baum el)] -> Int
(3) anzahlKnoten' [] = 0
(4) anzahlKnoten' (x:xs) = (anzahlKnoten x) + (anzahlKnoten' xs)

anzahlKanten :: Baum el -> Int
(5) anzahlKanten (Baum el []) = 0
(6) anzahlKanten (Baum el liste) = anzahlKanten' liste

anzahlKanten' :: [(Baum el)] -> Int
(7) anzahlKanten' [] = 0
(8) anzahlKanten' (x:xs) = 1 + anzahlKanten x + anzahlKanten' xs

 

Wir beginnen damit, die Aussage für den einfachsten Fall zu prüfen:

Induktionsanfang: baum = (Baum el [])

(1) anzahlKnoten baum = 1
(2) anzahlKanten baum = 0
=> anzahlKnoten baum = (anzahlKanten baum) + 1

 

Induktionsvoraussetzung: anzahlKnoten (Baum el xs) = (anzahlKanten (Baum el xs)) + 1

 

Induktionsschritt: (Baum el xs) -> (Baum el x:xs)

zu zeigen: anzahlKnoten (Baum el x:xs) = (anzahlKanten (Baum el x:xs)) + 1

anzahlKnoten (Baum el x:xs)
(2)  = 1 + anzahlKnoten' x:xs
(4)  = 1 + anzahlKnoten x + anzahlKnoten' xs
(2)  = anzahlKnoten x + anzahlKnoten (Baum el xs)
(IV) = anzahlKnoten x + (anzahlKanten (Baum el xs)) + 1

 

(anzahlKanten (Baum el x:xs)) + 1
(6)  = anzahlKanten' x:xs + 1
(8)  = 1 + anzahlKanten x + anzahlKanten' xs + 1
(6)  = 1 + anzahlKanten x + (anzahlKanten (Baum el xs) +1

 

Jetzt haben wir beide Seiten so weit umgeformt, dass dort nun folgendes steht:
anzahlKnoten x + (anzahlKanten (Baum el xs)) + 1 = 1 + anzahlKanten x + (anzahlKanten (Baum el xs) +1

Da auf beiden Seiten (anzahlKanten (Baum el xs)) + 1 steht, können wir diesen Ausdruck auf beiden Seiten entfernen. Es bleibt noch:

anzahlKnoten x = 1 + anzahlKanten x

Genau das wollten wir zeigen.
Damit sind wir fertig und haben anzahlKnoten baum = (anzahlKanten baum) + 1 bewiesen.

 


Konversation wird geladen