Induktion Klammerung

[SvenInfo12]

Hallo,
ich habe folgenden Pseudocode gegeben:
-Lese die Folge der Klammern von links nach rechts.
-Betrachte die aktuell gelesene Klammer:
-Falls "("gelesen, so lege diese auf den Stack.
-Falls ")"gelesen, so nimm eine "("vom Stack, erklare diese als zur
momentan gelesenen")"gehöig.
-Erkläre den Klammerausdruck als korrekt, falls der Stack am Ende leer
ist, jedoch zwischendurch niemals versucht wurde, auf den leeren Stack
pop() anzuwenden.


Ich will nun folgende Aussage mittels vollständiger Induktion über die Länge des nichtleeren Klammerausdrucks zeigen:
„Für eine nichtleere Eingabe erkennt der Algorithmus genau die korrekten Klammerausdrücke als korrekt und identifiziert zueinandergehörige Klammerpaare richtig“


Wie fange ich da an. Ich brauche doch immer eine gerade Zahl an Klammern oder verstehe ich etwas falsch. Dann kann mein Induktionsanfang nur für n=0 funktionieren.
Habt ihr vllt ein paar Tipps zum Verständnis?

 

[ComFreek]

Willkommen im Forum @SvenInfo12!

Zuallererst würde ich die zu zeigende Aussage genauer formalisieren:

• Was ist ein Klammerausdruck?
• Was ist seine Länge?

Die erste Frage würde ich z. B. so beantworten, mitunter hast du aber bereits eine bestehende Definition: Ein Klammernausdruck ein ein Term der Grammatik
t, t' ::= <empty> | (t) | t t'
wobei <empty> für den leeren String stehen soll.

Die zweite Frage würde ich als Anzahl von '(' und ')' definieren. Präziser: Wir definieren die Funktion length induktiv über die Grammatik via

• length(<empty>) = 0
• length((t)) = 2 + length(t) für einen korrekten Klammernausdruck t
• length(t t') = length(t) + length(t') für korrekte Klammernausdrücke t, t'

Für eine nichtleere Eingabe erkennt der Algorithmus genau die korrekten Klammerausdrücke als korrekt

"genau" sagt uns, dass das hier eine Äquivalenz ist bzw. Gleichheit von Mengen (wichtig!):
Die Menge von Ausdrücken, die der Algo als korrekt markiert = Die Menge von Ausdrücken, die per Grammatik korrekt sind.

Insgesamt musst du also zeigen:

\forall len, wobei len != 0: [Die Menge von Ausdrücken der Länge len, die der Algo als korrekt markiert] = [Die Menge von Ausdrücken der Länge len, die per Grammatik korrekt sind.] (*)

([...] ist nur zur Übersichtlichkeit benutzt.)

Nun siehst du eine forall-quantifizierte Variable, nämlich len, die auch noch Induktion erlaubt. Natürliche Zahlen erlauben Induktion, aber auch viele weitere Strukturen tun dies!
Für natürliche Zahlen bekommst du jetzt den IA mit len=1 und den IS, in dem du zeigst, dass wenn die Aussage für alle Längen <= len stimmt, dass sie auch korrekt für len+1 stimmt.

Weiterer Tip: Oft zeigt man Mengengleichheit mittels \subseteq in beiden Richtungen.

Ich brauche doch immer eine gerade Zahl an Klammern

Da hast du Recht! Für ungerade Längen ist die innere Aussage (unterm forall-Quantifier) äquivalent zu:

[Die Menge von Ausdrücken der Länge len, die der Algo als korrekt markiert] = {} (**)

Da ben per Grammatik Ausdrücke ungerader Länge nie korrekt sein können. (Diese Aussage würde man übrigens auch per Induktion zeigen. Eigentlich ist das eine gute Übung, allerdings muss man dabei über die Grammatik induzieren, eventuell ist das also ein Schritt zu viel, wenn man noch beim Lernen von Induktion über natürliche Zahlen ist )

Dann kann mein Induktionsanfang nur für n=0 funktionieren.

Dein IA für len=1 besteht eben darin zu zeigen, dass der Algorithmus *keinen* Klammernausdruck der Länge 1 als korrekt ansieht. Siehe (**).

Hilft das soweit?

 

[SvenInfo12]

Die erste Frage würde ich z. B. so beantworten, mitunter hast du aber bereits eine bestehende Definition: Ein Klammernausdruck ein ein Term der Grammatik
t, t' ::= <empty> | (t) | t t'

Hallo, danke für deine ausführliche Antwort. Leider habe ich mich noch nie mit Grammatik beschäftigt und ist mir auch noch nie untergekommen.
Also t und t' sind Klammerausdrücke.
Die rechte Seite bedeutet, dass man entweder keinen Klammerausdruck oder einen einfach geklammerten Ausdruck oder mehrere Klammerausdrücke hat. Ist das richtig? Den Rest lese ich mir gerade noch durch.

 

[SvenInfo12]

Dein IA für len=1 besteht eben darin zu zeigen, dass der Algorithmus *keinen* Klammernausdruck der Länge 1 als korrekt ansieht. Siehe (**).

D.h 1.: t besteht aus einer öffnenden Klammer, dann findet der Algo nie eine geschlossene und der Stack ist somit nie leer.
Analog andersrum.
Wäre das richtig?
Für den Induktionschritt wäre nehme ich an, dass für irgendeine len ungerade, die Aussage ** gilt.
Dann verstehe ich noch nicht, dass die Aussage für len+1 gelten muss, denn man kann ja eine passende Klammer hinzufügen, sodass man einen korrekten Klammerausdruck hat?

 

[ComFreek]

Also t und t' sind Klammerausdrücke.
Die rechte Seite bedeutet, dass man entweder keinen Klammerausdruck oder einen einfach geklammerten Ausdruck oder mehrere Klammerausdrücke hat. Ist das richtig? Den Rest lese ich mir gerade noch durch.

Korrekt. Korrekte Klammerausdrücke i. S. d. Grammatik sind also

()
() ()
()()()
((()))
((())) ((((()))))
...

wobei die erste Zeile der leere String ist.

D.h 1.: t besteht aus einer öffnenden Klammer, dann findet der Algo nie eine geschlossene und der Stack ist somit nie leer.

Das sieht sehr gut aus!
Kleine Anmerkung: in der Beschreibung des Algorithmus in deinem ersten Beitrag sollte wohl noch stehen, dass der Algo die Schleife abbricht, wenn er den ganzen String konsumiert hat und dann true ausgibt gdw. der Stack leer ist.

Für den Induktionschritt wäre nehme ich an, dass für irgendeine len ungerade, die Aussage ** gilt.

Du nimmst das Falsche an. (**) war (*) spezialisiert im Falle des IAs. (*) war dieser lang scrollbare Codeabschnitt von mir. Du musst (*) für den Induktionsschritt zeigen. Konkret:

Im Induktionsschritt musst du unter der Annahme
(***) Für ein fixes len gilt:
  [Die Menge von Ausdrücken der Länge len, die der Algo als korrekt markiert] = [Die Menge von Ausdrücken der Länge len, die per Grammatik korrekt sind.]

zeige, dass
(****) [Die Menge von Ausdrücken der Länge (len+1), die der Algo als korrekt markiert] = [Die Menge von Ausdrücken der Länge (len+1), die per Grammatik korrekt sind.].

(****) würde ich zuerst per Fallunterscheidung nach "(len+1) gerade?" und dann im komplizierteren Fall per Subseteq in beiden Richtungen zeigen.

Höchstwahrscheinlich müssen wir jedoch die Art der Induktion ändern, die wir anwenden. Die Induktionsvoraussetzung (***) sieht mir zu schwach aus. Ist dir bekannt, dass man in Induktionsbeweisen die Induktionsaussage für alle strikt kleineren Dinge im Induktionsschritt annehmen kann? Also nicht nur für das nächstkleinere Element, sondern für alle kleineren bis hin zur 0?
Das nennt sich "starke Induktion". (Übrigens gilt das auch i. Allg. für andere Strukturen, über die man induzieren kann: nämlich solche kleiner-werdenden Ketten müssen irgendwann abbrechen, in N eben bei der 0.)

Ich würde also nun den Induktionsschritt wie folgt aufziehen:

Im Induktionsschritt musst du für ein fixes len >= 1 unter der Annahme,
(***) dass für alle len' < len gilt:
  [Die Menge von Ausdrücken der Länge len', die der Algo als korrekt markiert] = [Die Menge von Ausdrücken der Länge len', die per Grammatik korrekt sind.]

zeige, dass
(****) [Die Menge von Ausdrücken der Länge len, die der Algo als korrekt markiert] = [Die Menge von Ausdrücken der Länge len, die per Grammatik korrekt sind.].

 

[SvenInfo12]

zeige, dass (****) [Die Menge von Ausdrücken der Länge len, die der Algo als korrekt markiert] = [Die Menge von Ausdrücken der Länge len, die per Grammatik korrekt sind.].

Vielen Dank für deine Antwort. Das mit der starken Induktion ist mir bekannt. Soweit ich dich verstanden habe, muss ich nun die Aussage für len zeigen, die natürlich größer ist als len'. D.h len und len' können sich auch um mehr als 1 unterscheiden.
Was ich nicht vertehe ist, wie man das zeigen soll. Ich weis nicht, in welcher Weise ich Klammer hinzufüge.
Sagen wir mal ich zeige: "c":
Dann ist der Klammerausdruck der Länge len korrekt markiert und dann?

 

[ComFreek]

D.h len und len' können sich auch um mehr als 1 unterscheiden.

Korrekt.

Sagen wir mal ich zeige: "c":
Dann ist der Klammerausdruck der Länge len korrekt markiert und dann?

Ah, du meinst ⊆! Hatte mich gerade gewundert Hmmm, ja das ist eine gute Frage, was du dann machst.
Möglicherweise hilft es die Funktion `f: {(,)}^* -> N \cup {\bot}` zu betrachten, die jeder Folge von Klammerungen entweder die Anzahl der noch zu schließenden Klammern zuordnet oder \bot, falls mal eine Klammer geschlossen wurde, die vorher gar nicht geöffnet wurde. Das ist genau die Anzahl der Dinge auf dem Stack in deinem Algorithmus.
Anders gesehen: f gibt eine natürliche Zahl zurück <=> Eingabe ein Präfix einer korrekten Klammerung war.

Tatsächlich habe ich das ganze Szenario mal aus Spaß in Coq versucht zu beweisen. Die Wahrscheinlichkeit, dass hier jemand in diesem Forum auch noch Coq benutzt, ist zwar sehr gering, aber Speicher gibt's ja genug Hier ein Auszug:

Inductive Parens := empty: Parens | wrapped: Parens -> Parens | juxtaposition: Parens -> Parens -> Parens.
Fixpoint parToStr (p: Parens): string := match p with
| empty => ""
| wrapped inner => "(" ++ (parToStr inner) ++ ")"
| juxtaposition l r => (parToStr l) ++ (parToStr r)
end.
Fixpoint isValidHelper (str: string) (counter: nat): bool := match str with
| EmptyString => beq_nat counter 0
| String s ss => match s with
  | "("%char => isValidHelper ss (S counter)
  | ")"%char => match counter with
    | S lowerCounter => isValidHelper ss lowerCounter
    | 0 => false
    end
  | _ => false
  end
end.
Definition isValid (str: string): bool := isValidHelper str 0.

Lemma preimage: forall (str: string), isValid str -> exists p, parToStr p = str.
Proof.
(* How to prove this? *)
(* Idea: consider the function which maps str indices to counter values.
   If it has a root, then build substrings and apply juxaposition.
   If it has no root, remove ( from start and ) from end.
*)
Admitted.

Theorem strAlwaysValid: forall (p: Parens), isValid (parToStr p).
Proof. (* based on unproven preimage, but working *)

 

[SvenInfo12]

Vielen Dank. Ich habe es mit deiner Hilfe hinbekommen.

 

[ComFreek]

Super!

 

[SvenInfo12]

Es tut mir leid für die sehr späte Antwort
Danke nochmals