Übung 7.2

Steven
Kernelcompilierer
Kernelcompilierer
Beiträge: 425
Registriert: 2. Sep 2008 10:00
Wohnort: Frankfurt am Main

Re: Übung 7.2

Beitrag von Steven »

Es ist richtig, dass VeriFun genau deswegen Aussagen in einer bestimmten erzeugten Algebra beweist. Allerdings war in dieser Aufgabe gefordert, es für eine beliebige Algebra zu zeigen und da funktioniert Verschiedenes eben nicht. Einen partiellen Beweis gibt es nicht! Alles, was ich annehme, muss ich in der Hypothesenmenge aufführen. Steht es nicht dort, darf ich es auch nicht einfach unter der Hand annehmen. Du kannst den Beweis natürlich retten, indem du die Aussage entsprechend abschwächst und nur über erzeugete Algebren redest.

tzeenie
Mausschubser
Mausschubser
Beiträge: 80
Registriert: 14. Okt 2008 20:04

Re: Übung 7.2

Beitrag von tzeenie »

Steven hat geschrieben:Wenn ich "alpha?add(k) => not alpha?empty(k)" behaupte und dies per Fallunterscheidung zeigen will, muss ich alle Elemente aus dem Definitionsbereich der Funktionen "alpha?add" und "alpha?empty" kennen. Du hättest recht, wenn ich als Prämisse noch fordern würde, dass A eine erzeugte Algebra ist, dann gibt es keine solchen Zusätze.
Naja, P ist ja auch nur eine Beschränkung des Ausdrucksraums von L. 8) Nach meinem Verständnis ist das Entscheidende beim Beweis, dass er für alle Algebren, die AxP erfüllen gelten muß. Schlüsse wie "wenn nicht alpha ?empty(k) dann alpha ?add(k)" sind unzulässig, da gebe ich Dir Recht. Allerdings kommt ja auch ohne solche Schlüsse aus, in dem man die Gültigkeit seiner Aussage auf die aus P bekannten Elemente beschränkt. Oder nicht? Ihr verwirrt mich. :mrgreen:

tzeenie
Mausschubser
Mausschubser
Beiträge: 80
Registriert: 14. Okt 2008 20:04

Re: Übung 7.2

Beitrag von tzeenie »

Ein "partieller Beweis" ist natürlich vollkommener Quatsch, da war ich beim Tippen mal wieder schneller als im Kopf, sorry. Was ich meinte, ist dass Deine Aussage partiell ist, in dem Sinne dass sie nur eine Teilmenge der Trägermenge umfasst. Bspw. könnte man ja auch eine gültige Aussage über alle Zahlen zw. 5 und 10 machen. Damit sind alle andere Zahlen (und auch fußball :) ) von der Aussage ausgeschlossen.

Simon Siegler
Computerversteher
Computerversteher
Beiträge: 369
Registriert: 16. Apr 2007 09:12

Re: Übung 7.2

Beitrag von Simon Siegler »

Bei der Erstellung der Aufgaben wurde die Relationenbeschreibung offenbar fehlerhaft aufgestellt, statt ?add wurde ¬?empty verwendet. Damit wird der Beweis deutlich vereinfacht.

Auf ?add(u) kann man im Allgemeinen nicht ¬?empty(u) folgern, auch nicht mit Hilfe der Axiome der Programms. Wie angeführt, kann es ein Trägerelement x geben, das nicht durch empty und add erzeugt wird, so dass ?add(x) und ?empty(x) gilt.

In einer erzeugten Algebra (mit Konstruktoren add und empty) kann man die Äquivalenz von ?add(u) und ¬?empty(u) mit Hilfe der Programm-Axiome nachweisen.

Um die Schrittsequenz mit ?add(u) zu beweisen, muss man eine Fallunterscheidung über ?empty(u) vornehmen. Dies ist wegen phi_bool möglich. Damit ist aber der Induktionsbeweis im Grunde sinnlos: Der Schrittfall unterteilt sich nochmal in Basis- und Schrittfall.

Für die Klausur können Sie ¬?empty als äquivalent zu ?add annehmen, da dies in den Lösungsvorschlägen überall so gehandhabt wurde.

Benutzeravatar
Tigger
Kernelcompilierer
Kernelcompilierer
Beiträge: 404
Registriert: 26. Okt 2007 17:35
Wohnort: Hofheim
Kontaktdaten:

Re: Übung 7.2

Beitrag von Tigger »

Simon Siegler hat geschrieben: Auf ?add(u) kann man im Allgemeinen nicht ¬?empty(u) folgern, auch nicht mit Hilfe der Axiome der Programms. Wie angeführt, kann es ein Trägerelement x geben, das nicht durch empty und add erzeugt wird, so dass ?add(x) und ?empty(x) gilt.
Ehrlich gesagt bin ich jetzt etwas verwirrt. Mir ist klar, dass es Elemente geben kann für die weder ?add(x) oder ?empty(x) gilt. Aber wie kann es denn einen Term geben für das beides gilt. Das ? Prädikat gibt doch an, ob ein Term aus einem bestimmten Konstruktor konstruiert wurde. Wie kann denn ein Term gleichzeitig aus 2 Konstruktoren erstellt sein.

Edit: Oder rührt dass daher, dass in nicht-Erzeugenden Algebren einem Element aus der Trägermenge durchaus mehrere Terme zugeordnet werden können?
Zuletzt geändert von Tigger am 26. Mär 2009 19:20, insgesamt 1-mal geändert.

xAx
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 157
Registriert: 6. Mär 2008 17:20

Re: Übung 7.2

Beitrag von xAx »

ist ja auch bei 6.2 keinem aufgefallen, wo es ähnlich mit nat ist (not ?0(u) statt ?succ(u)). können wir dort dann auch die beiden als äquivalent annehmen?
Nichts ist wie es scheint!
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
Zuletzt geändert von xAx am 14. Mär 2009 16:17, insgesamt 99-mal geändert.

Benutzeravatar
Tigger
Kernelcompilierer
Kernelcompilierer
Beiträge: 404
Registriert: 26. Okt 2007 17:35
Wohnort: Hofheim
Kontaktdaten:

Re: Übung 7.2

Beitrag von Tigger »

xAx hat geschrieben:ist ja auch bei 6.2 keinem aufgefallen, wo es ähnlich mit nat ist (not ?0(u) statt ?succ(u)). können wir dort dann auch die beiden als äquivalent annehmen?
Ich denke hier stimmts, da hier ja die die Relationsbeschreibung aus einer Prozedur stammt, in der ja ?0(n) in einer if-anweisung steht. Und hier wird der Schrittfall ja wirklich genau für not ?0(n) aufgerufen.

tzeenie
Mausschubser
Mausschubser
Beiträge: 80
Registriert: 14. Okt 2008 20:04

Re: Übung 7.2

Beitrag von tzeenie »

xAx hat geschrieben:ist ja auch bei 6.2 keinem aufgefallen, wo es ähnlich mit nat ist (not ?0(u) statt ?succ(u)). können wir dort dann auch die beiden als äquivalent annehmen?
Stimmt! Mir selbst ist es auch bei beiden Aufgaben nicht wirklich aufgefallen, weil in 6.2 \(R_{plus}\) als Relationenbeschreibung verwendet wurde. Ähnlich siehts bei der 7.2 aus, wenn man \(R_{length}\) als R.-Beschr. nimmt, statt \(R_{list}\). :shock: Nun bin ich völlig verwirrt, ist das jetzt ein Fehler oder darf man die Relationenbeschreibungen der Prozeduren verwenden?!

Steven
Kernelcompilierer
Kernelcompilierer
Beiträge: 425
Registriert: 2. Sep 2008 10:00
Wohnort: Frankfurt am Main

Re: Übung 7.2

Beitrag von Steven »

Tigger hat geschrieben:Edit: Oder rührt dass daher, dass in nicht-Erzeugenden Algebren einem Element aus der Trägermenge durchaus mehrere Terme zugeordnet werden können?
Der Term muss doch gar nicht einem Element in der Trägermenge entsprechen. Wenn die Algebra nicht erzeugend ist, kann sie beliebige weitere Elemente definieren, die nicht durch irgendetwas erzeugt werden, und die Rückgabewerte der ?-Funktionen dafür ebenfalls beliebig festlegen.

Ich denke, dass ist auch bei ?0(n) vs. ?succ(n) genauso. Auch hier kann ich aus "not ?0(n)" nicht "?succ(n)" folgern, zumindest nicht ohne weitere Einschränkungen für die Algebra.

Benutzeravatar
Tigger
Kernelcompilierer
Kernelcompilierer
Beiträge: 404
Registriert: 26. Okt 2007 17:35
Wohnort: Hofheim
Kontaktdaten:

Re: Übung 7.2

Beitrag von Tigger »

Steven hat geschrieben:
Tigger hat geschrieben:Edit: Oder rührt dass daher, dass in nicht-Erzeugenden Algebren einem Element aus der Trägermenge durchaus mehrere Terme zugeordnet werden können?
Der Term muss doch gar nicht einem Element in der Trägermenge entsprechen. Wenn die Algebra nicht erzeugend ist, kann sie beliebige weitere Elemente definieren, die nicht durch irgendetwas erzeugt werden, und die Rückgabewerte der ?-Funktionen dafür ebenfalls beliebig festlegen.

Ich denke, dass ist auch bei ?0(n) vs. ?succ(n) genauso. Auch hier kann ich aus "not ?0(n)" nicht "?succ(n)" folgern, zumindest nicht ohne weitere Einschränkungen für die Algebra.

Jaja, aber wie kann denn ein Term GLEICHZEITIG ?0(n) und ?succ(n) wahr auswerten. Wenn ein Element aus nichts erzeugt werden kann, wird es auch auf kein Konstruktorprädikat wahr auswerten. Ich dachte eher, das es wie zb. bei der Algebra von "int" war, wo zb. die 1 durch succ(0) oder pred(succ(succ(0) darstellbar war. Dann wäre sowohl ?pred(1) als auch ?succ(1) == true möglich.

Steven
Kernelcompilierer
Kernelcompilierer
Beiträge: 425
Registriert: 2. Sep 2008 10:00
Wohnort: Frankfurt am Main

Re: Übung 7.2

Beitrag von Steven »

Tigger hat geschrieben:Wenn ein Element aus nichts erzeugt werden kann, wird es auch auf kein Konstruktorprädikat wahr auswerten.
Es geht nicht darum, wo du ein Element herbekommst. Wir sagen, dass für alle Elemente im gemeinsamen Definitionsbereich der Funktionen "alpha?0" und "alpha?succ" gilt: Wenn alpha?0(x) = alphaFalse, dann alpha?succ(x) = true. Rein mathematisch müssen wir nun den gesamten Definitionsbereich betrachten. Von dem wissen wir aber nur, dass er *mindestens* die Elemente 0 und succ(n) enthält sowie ein paar Eigenschaften über diese Elemente. Das ist aber zu wenig. Vergleiche es mit der intentionalen Definiton in FoC: Wir definieren die Menge LAND als { D, F, GB } (+) WEITERE, wobei wir die Menge WEITERE unterspezifiziert lassen. Demnach können wir hier keine Fallunterscheidung machen, da wir nicht alle Fälle kennen. Genau verhält es sich hier.

Wenn dein Beispiel mit INT alle Axiome erfüllt, ist auch das eine denkbare Algebra, die ein Gegenbeispiel für unsere Implikation liefert. Du kannst deine Algebra ja sehr frei aufbauen, da geht vieles.

Antworten

Zurück zu „Archiv“