Übung 7.2

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

Übung 7.2

Beitrag von Remake »

Hallo.

Eine Frage zur Sequenz 2:
Man sollte ja aus der Relationenbeschreibung von der Struktur "list" und dem Lemma Sequenzen bilden.
Ich habe als zweite atomare Relationenbeschreibung {?add(k)} genommen [nach dem Vorgehen von Foliensatz 7]. Wird hier in der Musterlösung einfach "nicht?empty(k)" genommen, weil das äquivalent dazu ist? (Bsp: für alle x € nat: nicht?0(x) äquivalent zu ?succ(x) ?)

Ich habe dann beim Induktionsschritt gesagt, dass alpha?Empty(k) = alphaFalse, da die gewählte Algebra {add(k) äquivalent true}, AXlist und phiBool erfüllt. Geht das so auch?

Grüße,
Remake

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

Re: Übung 7.2

Beitrag von Tigger »

Also ich würde spontan sagen, dass das nicht so einfach geht. Es hängt ja ganz von der Algebra A ab. Es ist ja nicht gefordert, das A eine erzeugende Algebra ist. Folglich könnten dann in der Trägermenge von A auch Elemente sein, sie sich nicht durch Konstruktorgrundterme darstellen lassen, und dann gilt ja nicht zwangsläufig nicht-alpha?emty(k) = false => alpha?add(k) = true.

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

Re: Übung 7.2

Beitrag von Steven »

Die Methode aus der Musterlösung ist hier eine saubere Lösung, aber was ist mit einer Struktur mit drei Konstruktoren "c1", "c2" und "c3". Hier habe ich doch zwangsläufig ein "?c1(u)", "?c2(u)", "?c3(u)" in der Relationenbeschreibung stehen. Ich halte Tiggers Einwand für absolut korrekt, habe dann aber bei einem Programm "if ?c1(u) then ... else if ?c2(u) then ... else *** fi fi" ein Problem, Aussagen über ** zu treffen, da folgende Folgerung ja nicht machen kann: "nicht alpha?c1(u) AND nicht alpha?c2(u) => alpha?c3(u)". Demnach wäre die erfüllt-Beziehung aus der Aufgabe in einer solchen Situation nicht beweisbar, oder?

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:Die Methode aus der Musterlösung ist hier eine saubere Lösung, aber was ist mit einer Struktur mit drei Konstruktoren "c1", "c2" und "c3". Hier habe ich doch zwangsläufig ein "?c1(u)", "?c2(u)", "?c3(u)" in der Relationenbeschreibung stehen. Ich halte Tiggers Einwand für absolut korrekt, habe dann aber bei einem Programm "if ?c1(u) then ... else if ?c2(u) then ... else *** fi fi" ein Problem, Aussagen über ** zu treffen, da folgende Folgerung ja nicht machen kann: "nicht alpha?c1(u) AND nicht alpha?c2(u) => alpha?c3(u)". Demnach wäre die erfüllt-Beziehung aus der Aufgabe in einer solchen Situation nicht beweisbar, oder?
Allgemein gilt alpha?c1(u) AND nicht alpha?c2(u) => alpha?c3(u) nicht für jede Algebra, denn auch hier kann es ja Elemente in der Trägermenge geben, die sich nicht durch die 3 genannten Konstruktoren konstruieren lassen. Wenn man voraussetzt, dass es sich um eine erzeugende Algebra handelt, wäre die Folgerung meiner Meinung nach jedoch zulässig.

DanielR
Mausschubser
Mausschubser
Beiträge: 83
Registriert: 19. Feb 2008 13:15

Re: Übung 7.2

Beitrag von DanielR »

Tigger hat geschrieben:Allgemein gilt alpha?c1(u) AND nicht alpha?c2(u) => alpha?c3(u) nicht für jede Algebra, denn auch hier kann es ja Elemente in der Trägermenge geben, die sich nicht durch die 3 genannten Konstruktoren konstruieren lassen. Wenn man voraussetzt, dass es sich um eine erzeugende Algebra handelt, wäre die Folgerung meiner Meinung nach jedoch zulässig.
Dem würde ich zustimmen (ich denke du hast ein "not" for alpha?c1 vergessen?).

Allerdings reicht es meiner Meinung nach für den Beweis hier schon aus, dass unsere Algebra auf jedenfall AXlist erfüllt. Diese Axiomsmenge spendiert uns nämlich die unbedingte Gleichung all k' : Alist, x:Anat alpha?empty(add(x, k')) = alphafalse.
Es fehlt dann höchstens noch der kleine Hinweiß, dass (da ?add(k) gilt) k = add(x, k') für ein k' : Alist und ein x : Anat ist, um den Beweis korrekt zu halten. Oder?

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

Re: Übung 7.2

Beitrag von Tigger »

DanielR hat geschrieben: Allerdings reicht es meiner Meinung nach für den Beweis hier schon aus, dass unsere Algebra auf jedenfall AXlist erfüllt. Diese Axiomsmenge spendiert uns nämlich die unbedingte Gleichung all k' : Alist, x:Anat alpha?empty(add(x, k')) = alphafalse.
Es fehlt dann höchstens noch der kleine Hinweiß, dass (da ?add(k) gilt) k = add(x, k') für ein k' : Alist und ein x : Anat ist, um den Beweis korrekt zu halten. Oder?
Das Problem ist aber nach wie vor, dass wir von nicht-APLHAempty?(k)=true nicht automatisch schließen können, dass es sich bei k um ein add(x,k), also irgendwas was mit dem Konstruktor add() erzeugt wurde, ist. Es kann auch irgend ein Element sein, welches sich überhaupt nicht durch Konstruktorgrundterme darstellen lässt.

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

Re: Übung 7.2

Beitrag von Steven »

DanielR hat geschrieben:Es fehlt dann höchstens noch der kleine Hinweiß, dass (da ?add(k) gilt) k = add(x, k') für ein k' : Alist und ein x : Anat ist, um den Beweis korrekt zu halten. Oder?
Da bin ich mir nicht sicher, ob das reicht. Die Axiomenmenge sagt lediglich aus, dass die "?Typ" Funktion ("Prädikat") genau dann "true" wird, wenn sie auf den zugehörigen Konstruktor angewendet wird. Jetzt kann deine Algebra aber noch weitere Elemente der Trägermenge zur Sorte "list" haben, z.B. Alist = "add, empty, fußball", die nicht von der Signatur gefordert werden. Somit kann auch a?add(u) = atrue und a?empty(u) = atrue für ein solches u = fußball gelten. Die Axiomenmenge trifft ja nur Aussagen über die Elemente der Signatur, also add und empty. So ähnlich wurde auch in Aufgabe 6.1 gezeigt, dass PhiBool nicht für alle Algebren gilt, die AXp erfüllen.

@Tigger: Genau das meinte ich ja mit "nicht beweisbar". Wir können die Aussage nicht zeigen, da sie nicht zwingend in allen Algebren gilt.

DanielR
Mausschubser
Mausschubser
Beiträge: 83
Registriert: 19. Feb 2008 13:15

Re: Übung 7.2

Beitrag von DanielR »

Okay, da habe ich mich lückenhaft ausgedrückt.

Ich wollte dafür argumentieren, dass man den Beweis auch anhand der strukturellen Ordnung von List machen kann, wenn man die zugehörige Relationenbeschreibung mit ?empty und ?add "aufspannt". Es folgt dann nämlich trotzdem die für den Induktionsschritt nötige Behauptung "alpha?empty(ä(k)) = alphafalse".

Ansonsten stimme ich euch bis dahin zu. Ich sehe auch noch nicht, was uns darin hindert eine Algebra zu definieren für die List einen weiteren Konstruktor hat womit uns die nötige Behauptung nicht so einfach von der Hand geht.

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

Re: Übung 7.2

Beitrag von Steven »

DanielR hat geschrieben:Es folgt dann nämlich trotzdem die für den Induktionsschritt nötige Behauptung "alpha?empty(ä(k)) = alphafalse".
Imho. ist genau das nicht sichergestellt. Aus den Axiomen wissen wir:
1. alpha?empty(alphaempty) = atrue
2. alpha?add(alphaempty) = afalse
3. alpha?empty(alphaadd(n, q)) = afalse
4, alpha?add(alphaadd(n, q)) = atrue
OK, aber das ist keine totale Definition einer Funktion alpha?empty. Für Elemente nicht aus {alphaempty, alphaadd(n, q) für beliebiges n, q} wissen wir nämlich gar nichts, siehe mein Beispiel mit dem Element "fußball" oben. Es kann ja alpha?list (fußball) = alphatrue = alpha?empty (fußball) folgen.

Bislang einzige Korrektur meines Posts oben: Ich habe versehentlich einen einelementigen Konstruktor list statt dem zweielementigen add benutzt, das war Schlamperei meinerseits.
DanielR hat geschrieben:Ich sehe auch noch nicht, was uns darin hindert eine Algebra zu definieren für die List einen weiteren Konstruktor hat womit uns die nötige Behauptung nicht so einfach von der Hand geht.
Das ist eine andere Instanz des gleichen Problems.

DanielR
Mausschubser
Mausschubser
Beiträge: 83
Registriert: 19. Feb 2008 13:15

Re: Übung 7.2

Beitrag von DanielR »

Steven hat geschrieben:
DanielR hat geschrieben:Es folgt dann nämlich trotzdem die für den Induktionsschritt nötige Behauptung "alpha?empty(ä(k)) = alphafalse".
Imho. ist genau das nicht sichergestellt. Aus den Axiomen wissen wir:
3. alpha?empty(alphaadd(n, q)) = afalse
Genau. Und wenn man die Relationenbeschreibung von Rlist = {<{?empty(k)}, Ö>, <{?add(k)}, {{k/tl(k)}}>} verwendet um die Induktionshypothesen aufzustellen wird ä(k) = alpha add(x, alpha tl (ä(k)) gelten, und nicht = alpha fussball....

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

Re: Übung 7.2

Beitrag von tzeenie »

Mmh, ich verstehe das Problem nicht ganz: Wenn fußball außerhalb unseres Programms P liegt, interessiert fußball doch für den Beweis überhaupt nicht? Wir nehmen doch an, dass (A, quer_a) erfüllt AxP, damit insbesondere auch AxList. Nun kannst Du in Deinem Beweis doch jederzeit alle (in P!) möglichen Fälle von Konstruktoren aufzählen und einzeln beweisen.

Der Punkt ist doch: es gibt immer nur endlich viele Konstruktoren - damit auch nur endlich viele Fallunterscheidungen; wenn Du also weißt, dass nicht alpha empty(k) gilt, kommen nur endlich viele weitere Konstruktoren in Betracht. Ob in der Algebra zusätzlich fußball existiert ist irrelevant, da Du keine Aussagen über fußball triffst.

fl4$h g0rd0n
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 115
Registriert: 1. Okt 2007 22:20

Re: Übung 7.2

Beitrag von fl4$h g0rd0n »

Ich bin der Meinung, man kann in der Version mit \(\alpha_{?add}(\mathfrak{a}(k)) = \alpha_{true}\) davon ausgehen, dass \(\alpha_{?empty}(\mathfrak{a}(k)) = \alpha_{false}\) (unter der Annahme, \(\phi_{bool}\) gilt). Nach Definition von zusammengesetzten Relationenbeschreibungen wird die disjunkte Separierung der enthaltenen atomaren Relationenbeschreibungen gefordert. D. h. es gilt immer die Hypothesenmenge genau einer atomaren Relationenbeschreibung.
"Education is the path from cocky ignorance to miserable uncertainty" -- Mark Twain

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

Re: Übung 7.2

Beitrag von Tigger »

tzeenie hat geschrieben:Mmh, ich verstehe das Problem nicht ganz: Wenn fußball außerhalb unseres Programms P liegt, interessiert fußball doch für den Beweis überhaupt nicht? Wir nehmen doch an, dass (A, quer_a) erfüllt AxP, damit insbesondere auch AxList. Nun kannst Du in Deinem Beweis doch jederzeit alle (in P!) möglichen Fälle von Konstruktoren aufzählen und einzeln beweisen.
fußball triffst.
Du willst aber ganz P für eine beliebige Algebra die die Axiome erfüllt beweisen, und zwar für alle Elemente der Trägermenge, nicht nur für alle Elemente die die Konstruktorgrundterme bilden. Deswegen werden ja Programme in L mit Standartalgebrem bewiesen, weil hier ist es in der Tat so, dass die Trägermenge nur Werte enthält, die sich mit Konstruktorgrundtermen darstellen lassen (-> siehe Kapitel 12). Und da gelten dann automatisch auch Formeln wie "nicht(X) =true => x = false", die wir hier explizit angeben mussten.

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

Re: Übung 7.2

Beitrag von Steven »

DanielR hat geschrieben:Genau. Und wenn man die Relationenbeschreibung von Rlist = {<{?empty(k)}, Ö>, <{?add(k)}, {{k/tl(k)}}>} verwendet um die Induktionshypothesen aufzustellen wird ä(k) = alpha add(x, alpha tl (ä(k)) gelten, und nicht = alpha fussball....
Das verstehe ich nicht. Sei phi unsere Beweisverpflichtung. Der Basisfall ist trivial, beim Schrittfall haben wir folgende Voraussetzungen:
1. ?alphaadd(k) = alphatrue
2. A |= phi [k\tl(k)].
Jetzt müssen wir zeigen: A |= phi [k]. Eine Aussage über unsere Algebra haben wir nicht, d.h. wir haben lediglich A |= AXp und A erfüllt die beiden oben genannten Voraussetzungen. Woraus leitest du her, dass ä(k) = alpha add (...) ist? Eine Argumentation auf Basis der Relationenbeschreibung funktioniert m.E. nicht, da die Algebra ja noch über die Signatur hinausgehende Elemente definieren kann - solange sie die Axiome weiterhin erfüllt - , die also in der Relationenbeschreibung überhaupt nicht auftauchen können.
tzeenie hat geschrieben:Ob in der Algebra zusätzlich fußball existiert ist irrelevant, da Du keine Aussagen über fußball triffst.
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.

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

Re: Übung 7.2

Beitrag von tzeenie »

Aber für völlig beliebige Algebren ist Dein Beweis doch immer partiell, oder nicht? Du triffst eine Aussage über eine Teilmenge der Trägermenge, und diese Aussage soll immer gelten, wenn die Algebra AxP erfüllt. Und das ist ja gegeben, auch wenn die Aussage nicht mehr alle Elemente Deiner Trägermenge umfasst. So wie ich es verstanden habe, ist dass der Grund für die Art der Implementation von VeriFun - man will totale Beweise führen, deshalb Standardmodell.

Antworten

Zurück zu „Archiv“