Hausübung 4.1

Benutzeravatar
Gnomix
Computerversteher
Computerversteher
Beiträge: 306
Registriert: 31. Okt 2005 08:44

Hausübung 4.1

Beitrag von Gnomix »

Hallo,

wie ist das gemeint, "Belegen Sie die Gültigkeit der Terminierungshypothesen durch Anwendung bekannter arithmeti-
scher Gleichungen" ?

Sollen wir durch Umformung nach true auswerten ?
Und wenn alles was zurückgegeben werden kann schon true ist [if{A,true, true}], müssen wir dennoch umformen [A]?
Zuletzt geändert von aderhold am 3. Feb 2009 17:26, insgesamt 1-mal geändert.
Grund: Beiträge beziehen sich nicht ausschließlich auf Aufgabenteil (d).

Benutzeravatar
mba
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 260
Registriert: 13. Jul 2007 19:16

Re: Hausübung 4.1 d)

Beitrag von mba »

Was in dieser Aufgabe gefordert wird, habe ich auch nicht ganz verstanden. Ist hier nach den Schritten gefragt, die man durch den Evaluation Viewer in VeriFun bekommen kann?
»Es ist noch kein Meister vom Himmel gefallen«
Wenn doch, wär er jetzt tot.
Bild

Benutzeravatar
C0RNi666
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 114
Registriert: 8. Jan 2008 12:51

Re: Hausübung 4.1 d)

Beitrag von C0RNi666 »

Ich kann mich meinem Vorredner nur anschließen und sehe darüberhinaus nicht den Grund die Normalisierungs-Vorschrift nach 5.3 anzuwenden.
Soll ich im Vorfeld meine Induktionshypothesen bewusst so auftellen, dass die Normalisierung darauf angewendet werden kann?

Für ein paar aufklärende Worte wäre wir sicherlich sehr dankbar.

Viele Grüße
Win32: Reboot!
Unix: Be root!

aderhold
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 212
Registriert: 21. Okt 2005 10:50

Re: Hausübung 4.1 d)

Beitrag von aderhold »

Hier ist nicht nach Auswertungsschritten oder Deutungen in Algebren gefragt. Es geht um Folgendes: Die alleinige Angabe von Maßtermen ist zum Terminierungsnachweis etwas dünn. Ein vollständig ausgearbeiteter formaler Beweis ist (unverhältnismäßig) aufwendig. Gesucht ist also etwas zwischen diesen Extremen. Aus der Begründung soll hervorgehen, warum die gewählten Maßterme für einen Terminierungsnachweis erfolgversprechend sind.

Beispiel: Für die Prozedur "gcd" aus Kapitel 8 (Folie 16) wählt man den Maßterm "x + y". Nun begründet man, weshalb die Terminierungshypothesen auf Folie 17 wahr sind. Etwa so: Wegen "x > y" ist "(x - y) + y = x". Zu zeigen ist also "x + y > x". Dies gilt, weil y verschieden von 0 ist.

aderhold
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 212
Registriert: 21. Okt 2005 10:50

Re: Hausübung 4.1 d)

Beitrag von aderhold »

Gnomix hat geschrieben:[if{A,true, true}], müssen wir dennoch umformen [A]?
Im Zuge der in (c) erbetenen Vereinfachung wäre "if{A,true, true}" zu "true" zu vereinfachen.

aderhold
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 212
Registriert: 21. Okt 2005 10:50

Re: Hausübung 4.1 d)

Beitrag von aderhold »

C0RNi666 hat geschrieben:Ich [...] sehe darüberhinaus nicht den Grund die Normalisierungs-Vorschrift nach 5.3 anzuwenden.
Eine gemäß Kapitel 8, Folie 7 gebildete Terminierungshypothese kann
  1. unmöglich bereits normalisiert sein, wenn H mindestens zwei Elemente enthält, und
  2. unmöglich von der Form "if{..., true, true}" sein, weil der Then-Zweig die Form "x > t" hat.
Da sich die Diskussion mittlerweile vom Aufgabenteil (d) entfernt hat, lösche ich das "(d)" mal aus dem Thread-Titel.

Remake
Mausschubser
Mausschubser
Beiträge: 64
Registriert: 15. Dez 2007 10:40

Re: Hausübung 4.1

Beitrag von Remake »

Noch mal zum Vereinfachen in Teil c):
Wenn wir sowas "offensichtliches" wie a > pred(a) haben, sollen wir das dann als true annehmen (dann eben evtl in Aufgabe d beweisen) und so weiter vereinfachen, oder ist das auf etwas anderes bezogen? Dann könnte man quasi evtl. bis nur noch true da steht vereinfachen, ist das so gewollt? ;-)

aderhold
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 212
Registriert: 21. Okt 2005 10:50

Re: Hausübung 4.1

Beitrag von aderhold »

Remake hat geschrieben:Noch mal zum Vereinfachen in Teil c):
Wenn wir sowas "offensichtliches" wie a > pred(a) haben, sollen wir das dann als true annehmen (dann eben evtl in Aufgabe d beweisen) und so weiter vereinfachen, oder ist das auf etwas anderes bezogen?
Die Terminierungshypothese repräsentiert eine Formel. Die Vereinfachung in (c) bezieht sich auf die rein (aussagen)logische Vereinfachung dieser Formel ohne Berücksichtigung von Lemmas oder der Definitionen von Prozeduren.
Beispiele:
  • if{A, B, B} wird vereinfacht zu B.
  • if{true, A, B} wird vereinfacht zu A.
  • if{A, A, B} wird vereinfacht zu if{A, true, B}.
Nicht-Beispiele (denn hierzu müsste man Lemmas oder Definitionen von Prozeduren anwenden):
  • if{?0(n), n > m, A} wird nicht vereinfacht zu if{?0(n), false, A}.
  • if{?0(m), n > m, A} wird nicht vereinfacht zu if{?0(m), not ?0(n), A}.
  • if{?succ(n), n > pred(n), A} wird nicht vereinfacht zu if{?succ(n), true, A}.
Übrig bleibt eine "Formel" ohne (aussagen)logische Redundanzen, quasi die Essenz der Terminierungshypothese. Dass diese Essenz wahr ist, begründet man in (d).

Antworten

Zurück zu „Archiv“