Seite 1 von 1

Induktion

Verfasst: 13. Feb 2012 20:55
von bafnai
Hallo,
ich habe zwei Fragen zu Induktionsaufgaben.

1) Muss bei HPL-Sequenzen in der Menge der Induktionshypothesen der Allquantor über die benutzten Variablen angegeben werden?
In Kapitel 6 auf Folie 21 und in der Lösung des 2. Teils der 4. Hausübung wird jeweils allquantifiziert, in den Lösungen der 6. und 7. Übung nicht.
2) Dürfen in der Klausur, wie in der Lösung des 2. Teils der 4. Hausübung, Auslassungszeichen und Zusammenfassungen von Teiltermen (damit ist t := hd(k) :: append(tl(k), l) gemeint) verwendet werden?

Re: Induktion

Verfasst: 13. Feb 2012 22:23
von Christoph Walther
bafnai hat geschrieben:Hallo,
ich habe zwei Fragen zu Induktionsaufgaben.
1) Muss bei HPL-Sequenzen in der Menge der Induktionshypothesen der Allquantor über die benutzten Variablen angegeben werden?
Ja sicher. Es ist ja ein unterschied, ob man einen schrittfall der form

∀ x, y: ℕ x ≠ 0 ∧ φ[x - 1, y] → φ[x, y]

oder der form

∀ x, y : ℕ x ≠ 0 ∧ ∀ y : ℕ φ[x - 1, y] → φ[x, y]

hat. Im zweiten fall darf man bei verwendung der induktionshypothese y durch einen beliebigen term ersetzen, im ersten fall dagegen nicht.
bafnai hat geschrieben:2) Dürfen in der Klausur, wie in der Lösung des 2. Teils der 4. Hausübung, Auslassungszeichen und Zusammenfassungen von Teiltermen (damit ist t := hd(k) :: append(tl(k), l) gemeint) verwendet werden?
Siehe meine antwort unter http://www.fachschaft.informatik.tu-dar ... 77#p138477 .

Re: Induktion

Verfasst: 14. Feb 2012 10:56
von Nathan Wasser
bafnai hat geschrieben:Hallo,
ich habe zwei Fragen zu Induktionsaufgaben.

1) Muss bei HPL-Sequenzen in der Menge der Induktionshypothesen der Allquantor über die benutzten Variablen angegeben werden?
In Kapitel 6 auf Folie 21 und in der Lösung des 2. Teils der 4. Hausübung wird jeweils allquantifiziert, in den Lösungen der 6. und 7. Übung nicht.
2) Dürfen in der Klausur, wie in der Lösung des 2. Teils der 4. Hausübung, Auslassungszeichen und Zusammenfassungen von Teiltermen (damit ist t := hd(k) :: append(tl(k), l) gemeint) verwendet werden?
zu 1) Wir haben bestimmte Variablen nicht nach belieben allquantifiziert, wenn das die Frage ist. Es ist nur so richtig.

zu 2) Zu Auslassungszeichen haben wir jetzt schon mehrfach im Forum geantwortet. Wer Platz sparen will, darf gerne Teilterme zusammenfassen, solange folgendes beachtet wird:
  • die Variable \(t\) im Beispiel muss eine neue, unbenutzte Variable sein
  • es muss klar sein was zusammengefasst wird
  • es muss beachtet werden, dass dort eigentlich weiterhin der ursprüngliche Term steht