MuLö und Beiblatt der Probeklausur

tigris
Mausschubser
Mausschubser
Beiträge: 89
Registriert: 2. Okt 2008 13:49

MuLö und Beiblatt der Probeklausur

Beitrag von tigris »

Hallo,
gibt es irgendwo eine Musterlösung der Probeklausur?
Und außerdem soll für die Aufgabe 3 ein ”Beiblatt zur Klausur Einführung in Foundations of Computing“ verfügbar sein. Wo findet man dieses? Würde es nämlich schon gerne schon einmal vor der Klausur sehen.
LG

fetzer
Kernelcompilierer
Kernelcompilierer
Beiträge: 522
Registriert: 1. Okt 2008 17:18

Re: MuLö und Beiblatt der Probeklausur

Beitrag von fetzer »

Wir können auch gern die Lösungen hier einfach mal sammeln:

Aufgabe 1:

\(filter((lv,lvl),g) = \begin{cases}

(lv, filter(lvl,g)), & \text{wenn }gebiet(lv)=g\\
filter(lvl,g), & \text{wenn }gebiet(lv)\neq g
\end{cases}\)

\(filter((),g) = ()\)

\(gebpoints(lv,g) = \begin{cases}

points(filter(lv,g)), & \text{wenn }lv \neq ()\\
0, & \text{sonst}
\end{cases}\)


Aufgabe 2:

\(\Phi_1 := \forall s \in STD: 19 \leq points(prüfungen(s)) \leq 22\)
\(\Phi_2 := \forall s \in STD, g \in GEB: gebpoints(prüfungen(s), g) \leq 9\)
\(\Phi_3 := \forall s \in STD \exists l_1,l_2: studleist(s,l_1) \land studleist(s,l_2) \land l_1 \neq l_2 \land form(l_1) \neq form(l_2)\)
Bei \(\Phi_4\) sind es Nr. 2 und 3, die angemessen sind.
Darüber hinaus muss man wahrscheinlich \(\Phi_1\) mittels \(\land\) schreiben, oder?

Aufgabe 3 folgt bald :)

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: MuLö und Beiblatt der Probeklausur

Beitrag von dschneid »

Bei Aufgabe 1 habe ich einfach \(gebpoints(lv, geb) = sum(map(points, filter(lv, geb)))\) definiert.

Bei Aufgabe 2.4 muss ich widersprechen: Meiner Meinung nach sind 3 und 4 angemessen. 2 ist nicht angemessen, weil immer falsch: Wenn \(i = j\), so sind die beiden Lehrveranstaltungen gleich, also ist die allquantifizierte Formel nie erfüllt, weil es immer ein Gegenbeispiel gibt. Außerdem ist 4 meiner Meinung nach angemessen, weil das aussagt, dass für alle Lehrveranstaltungen die Menge der Indizes, unter denen die Veranstaltung in der Folge steht, nur 0 oder 1 Element groß ist. Die Veranstaltung kann also gar nicht, maximal aber einmal vorkommen.

Aufgabe 3 würde mich auch mal interessieren. Ich habe da zwar eine Lösung, bin aber nicht ganz überzeugt, weil ich nämlich scheinbar auch ohne das Argument der deterministischen Auswertung zum Ziel komme.

fetzer
Kernelcompilierer
Kernelcompilierer
Beiträge: 522
Registriert: 1. Okt 2008 17:18

Re: MuLö und Beiblatt der Probeklausur

Beitrag von fetzer »

dschneid hat geschrieben:Bei Aufgabe 1 habe ich einfach \(gebpoints(lv, geb) = sum(map(points, filter(lv, geb)))\) definiert.
Die Frage ist, ob sum und map ebenfalls zur Verfügung stehen. Umständlicher ists auf jeden Fall, da points als \(LV^* \rightarrow \mathbb{N}\) definiert ist und damit direkt auf die Liste angewendet werden könnte.
2 ist nicht angemessen, weil immer falsch: Wenn \(i = j\), so sind die beiden Lehrveranstaltungen gleich, also ist die allquantifizierte Formel nie erfüllt, weil es immer ein Gegenbeispiel gibt.
Stimmt, es müsste ein \(\land i \neq j\) dazu!
Bei 4 geb ich dir nach deiner Argumentation ebenfalls recht.
Aufgabe 3 würde mich auch mal interessieren. Ich habe da zwar eine Lösung, bin aber nicht ganz überzeugt, weil ich nämlich scheinbar auch ohne das Argument der deterministischen Auswertung zum Ziel komme.
Ich versuchs mal:
Beim Auswerten des If-Teils bekommst du ja einmal \(<x=x,\sigma>\Downarrow t\). Wenn du hier nun r=t anwendest folgt daraus \(<x,\sigma>\Downarrow n\) und \(<x,\sigma>\Downarrow n'\). Würdest du hier nun annehmen, dass eine nichtdeterministische Auswertung erfolgt könntest du nicht sagen, dass n=n'. Da du jedoch davon ausgehen kannst, dass eine deterministische Auswertung erfolgt, d.h. n=n', kannst du von Gleichheit ausgehen und würdest keinen Widerspruch in der Auswertung von x=x nach t erhalten.
Könnte das jemand bestätigen, oder bin ich aufm völlig falschen Dampfer?

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: MuLö und Beiblatt der Probeklausur

Beitrag von dschneid »

fetzer hat geschrieben:Die Frage ist, ob sum und map ebenfalls zur Verfügung stehen.
Achso, stimmt. Ich hatte jetzt "alle mathematischen Konzepte aus der Vorlesung" auf die Schnelle so aufgefasst, aber das war ja erstens kein Konzept und zweitens aus der Übung, nicht aus der Vorlesung. Guter Punkt.
fetzer hat geschrieben:Stimmt, es müsste ein \(\land i \neq j\) dazu!
Selbst dann geht es aber nicht, ist mir nach meinem letzten Post aufgefallen, weil für alle natürlichen Zahlen nach dem Ende der Folge ja einfach der Index selbst zurückgegeben wird, also gibt es auf jeden Fall unendlich viele Paare, für die hier gleiche Dinge von elem zurückgegeben werden.

Ich hätte dann auch mal eine Frage zur Aufgabe 3: Und zwar muss man da ja unter anderem zeigen, dass x := 7; y := 5 äquivalent zu y := 5; x := 7 ist. Sehe ich das richtig, dass die Sache von der Syntax der Herleitung her irgendwie trivial ist, und der ganze Inhalt hier in den semantischen Seitenbedingungen "versteckt" ist, nämlich einfach durch die Tatsache, dass derselbe Zustand \(\sigma'\) entsteht, wenn man zuerst aus \(\sigma\) durch Veränderung von x einen Zustand \(\sigma''\) bildet und dann y ändert (das ist ja mit der Regel r; Teil der gegebenen Herleitung), oder ob man zuerst y verändert und einen anderen Zwischenzustand \(\sigma'''\) bekommt und dann x verändert (das wäre Teil der Herleitung, die man konstruieren will). In beiden Fällen kommt man ja auf denselben Zustand \(\sigma'\), in dem \(\sigma(x) = 7\) und \(\sigma(y) = 5\) gilt, und kann deswegen mit r; das Urteil \(\langle y := 5; x := 7, \sigma \rangle \rightarrow \sigma'\) herleiten, das man für die zu konstruierende Herleitung braucht. Ist das wirklich der Knackpunkt, oder braucht man an dieser Stelle vielleicht die deterministische Auswertung?

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: MuLö und Beiblatt der Probeklausur

Beitrag von dschneid »

Okay, meine komplette Antwort auf Aufgabe 3:

Wir nehmen an, es gibt eine Herleitung für \(\langle \text{if } x = x \text{ then } x := 7; y := 5 \text{ else skip fi}, \sigma \rangle \rightarrow \sigma'\). Die letzte Regel in der Herleitung muss aufgrund der Syntax des Ausdruckes rift oder riff sein. Also Fallunterscheidung:

Fall rift: Dann gibt es als Prämissen für das Urteil die beiden Urteile \(\langle x = x, \sigma \rangle \Downarrow true\) und \(\langle x := 7; y := 5 , \sigma \rangle \rightarrow \sigma'\). Aus \(\langle x = x, \sigma \rangle \Downarrow true\) kann man mit r\(\neg\)f unmittelbar \(\langle \neg (x = x), \sigma \rangle \Downarrow false\) herleiten. Wie ich schon beschrieben hatte, kann man auch \(\langle y := 5; x := 7 , \sigma \rangle \rightarrow \sigma'\) herleiten. Mit der Regel riff kann man damit schließlich wie gewünscht das Urteil \(\langle \text{if } \neg (x = x) \text{ then skip else } y := 5; x := 7 \text{ fi}, \sigma \rangle \rightarrow \sigma'\) herleiten.

Fall riff: Hier kann man entweder direkt vorgehen, oder man zeigt, dass der Fall gar nicht eintreten kann. Dafür macht man einen Widerspruchsbeweis: Wenn dieser Fall tatsächlich eintreten könnte, so wäre eine der Prämissen der Regel in diesem Fall riff \(\langle x = x, \sigma \rangle \Downarrow false\). Dies ist aber nur über die Regel r=f herleitbar, wenn \(\langle x, \sigma \rangle \Downarrow n_1\) und \(\langle x, \sigma \rangle \Downarrow n_2\) herleitbar sind, wobei \(n_1 \neq n_2\). Wegen der deterministischen Auswertung von Aexp wird aber im Zustand \(\sigma\) der arithmetische Ausdruck \(x\) in beiden Fällen gleich ausgewertet, also \(n_1 = n_2\); Widerspruch!
Die direkte Konstruktion einer Herleitung ist aber hier auch nicht viel schwerer (daher auch meine Aussage, man bräuchte die deterministische Auswertung von Aexp eigentlich gar nicht). Man benutzt einmal die Regel r\(\neg\)t, um \(\langle \neg (x = x), \sigma \rangle \Downarrow true\) herzuleiten, weiterhin ist eine Herleitung von \(\langle \text{skip}, \sigma \rangle \rightarrow \sigma\) trivial, und man kann aus den beiden Urteilen mit der Regel rift das gewünschte Urteil herleiten. (Man muss beachten, dass hier zwangsläufig \(\sigma' = \sigma\) ist, weil das \(\text{skip}\), das im else-Zweig ausgeführt wird, keine Zustandsänderung nach sich zieht.)

So ganz glaube ich mir das aber selbst nicht, deswegen bitte ich um Meinungen.

tigris
Mausschubser
Mausschubser
Beiträge: 89
Registriert: 2. Okt 2008 13:49

Re: MuLö und Beiblatt der Probeklausur

Beitrag von tigris »

Vielen Dank für die ganzen Hinweise.
Mir ging's primär halt auch um die 3. Aufgabe, schade, dass es hier keine Musterlösung zu geben scheint, denn hier hätte ich halt gerne mal einen 'offiziellen' Lösungsweg gesehen.
@Dr. Starostin: Was ist mit dem Beiblatt, kann man sowas schon vorher sehen?

Benutzeravatar
JanM
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 157
Registriert: 24. Aug 2010 10:58

Re: MuLö und Beiblatt der Probeklausur

Beitrag von JanM »

dschneid hat geschrieben: Ich hätte dann auch mal eine Frage zur Aufgabe 3: Und zwar muss man da ja unter anderem zeigen, dass x := 7; y := 5 äquivalent zu y := 5; x := 7 ist. Sehe ich das richtig, dass die Sache von der Syntax der Herleitung her irgendwie trivial ist, und der ganze Inhalt hier in den semantischen Seitenbedingungen "versteckt" ist, nämlich einfach durch die Tatsache, dass derselbe Zustand \(\sigma'\) entsteht, wenn man zuerst aus \(\sigma\) durch Veränderung von x einen Zustand \(\sigma''\) bildet und dann y ändert (das ist ja mit der Regel r; Teil der gegebenen Herleitung), oder ob man zuerst y verändert und einen anderen Zwischenzustand \(\sigma'''\) bekommt und dann x verändert (das wäre Teil der Herleitung, die man konstruieren will). In beiden Fällen kommt man ja auf denselben Zustand \(\sigma'\), in dem \(\sigma(x) = 7\) und \(\sigma(y) = 5\) gilt, und kann deswegen mit r; das Urteil \(\langle y := 5; x := 7, \sigma \rangle \rightarrow \sigma'\) herleiten, das man für die zu konstruierende Herleitung braucht. Ist das wirklich der Knackpunkt, oder braucht man an dieser Stelle vielleicht die deterministische Auswertung?
Der Knackpunkt liegt in der Aussage der Nebenbedingung von r:= "Jeder anderen Programmvariablen y [in sigma'] wird der Wert sigma(y) zugewiesen" Modul 5, Folie 30. So gilt also bei der einen Herleitung sigma''(x) = 7 und sigma''(y) = unbekannt und bei der anderen sigma''(x)=unbekannt und sigma''(y)=5, aber in sigma' gilt sigma'(x)=7 und sigma'(y)=5.
Damit enden beide im selben Zustand, da allen Programmvariablen dieselben Werte zugewiesen wurden. Es handelt sich bei den beiden Ausdrücken allerdings nur um semantische Äquivalenz und nicht um Gleichehit.

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: MuLö und Beiblatt der Probeklausur

Beitrag von dschneid »

Ja, genau das meinte ich damit, dass der ganze Inhalt in den semantischen Seitenbedingungen liegt. Dann passt das ja.

kruse
Mausschubser
Mausschubser
Beiträge: 49
Registriert: 15. Okt 2009 15:10
Kontaktdaten:

Re: MuLö und Beiblatt der Probeklausur

Beitrag von kruse »

Hi,
mich würde auch das Beiblatt, wenn es eins gibt interessieren. Was ist denn da so drauf?

TmOwOw
Neuling
Neuling
Beiträge: 5
Registriert: 25. Sep 2009 19:59

Re: MuLö und Beiblatt der Probeklausur

Beitrag von TmOwOw »

Frage zurückgezogen.

h4ck4
Mausschubser
Mausschubser
Beiträge: 91
Registriert: 18. Mai 2009 20:50
Kontaktdaten:

Re: MuLö und Beiblatt der Probeklausur

Beitrag von h4ck4 »

Beiblatt der Klausur:

Was wird alles drauf stehen bzw. von was können wir ausgehen? Was stand denn auf dem der Probeklausur drauf? Hat das jmd.? Bzw. wird noch eins im Vorfeld veröffentlicht?!

Fragen über Fragen ;-P

Schonmal Danke im Voraus!

Benutzeravatar
hymGo
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 209
Registriert: 4. Okt 2009 23:17

Re: MuLö und Beiblatt der Probeklausur

Beitrag von hymGo »

Also ich wüsste da auch gerne genaueres.
Ich verlasse mich jetzt einfach darauf, dass man die Kalkülregeln bekommt, denn diese habe ich nicht auf meinem Blatt geschrieben.

Benutzeravatar
olg
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 297
Registriert: 1. Okt 2008 19:24

Re: MuLö und Beiblatt der Probeklausur

Beitrag von olg »

Habe vorhin einfach mal eine Mail bzgl. des Beiblattes mit den IMP-Regeln an den Assistenten geschickt:
Hallo,

morgen bekommen Sie dieses Beiblatt mit den Kalkülregeln. Viel Erfolg!

Mfg,
Artem Starostin
"To Perl, or not to Perl, that is the kvetching." ~Larry Wall

Weishaupt
Windoof-User
Windoof-User
Beiträge: 37
Registriert: 7. Okt 2009 20:20

Re: MuLö und Beiblatt der Probeklausur

Beitrag von Weishaupt »

War da auch ein Angang bei der Mail dabei? Dann kannst du den ja mal hochladen.

Antworten

Zurück zu „Archiv“