Hausübung 4.2 (b)
Hausübung 4.2 (b)
Hi,
Wie behandelt man die Stuck Terme wenn man die Sequenzen bauen will?
Lässt man die weg ?
Ich hab im Skript gesucht und mir die Übungen angeschaut, aber nichts dazu gefunden.
Wie behandelt man die Stuck Terme wenn man die Sequenzen bauen will?
Lässt man die weg ?
Ich hab im Skript gesucht und mir die Übungen angeschaut, aber nichts dazu gefunden.
Re: Hausübung 4.2 (b)
Wie auf Seite 18 von Kapitel 9 steht wird * durch den Prozeduraufruf mit gleichen Parametern ersetzt.
-
- Computerversteher
- Beiträge: 369
- Registriert: 16. Apr 2007 09:12
Re: Hausübung 4.2 (b)
In Aufgabe 4.2 (b) spielen Stuck-Terme keine Rolle. Wie in Teilaufgabe (a) vorzugehen ist, wurde bereits erläutert.s_n hat geschrieben: Wie behandelt man die Stuck Terme wenn man die Sequenzen bauen will?
Lässt man die weg ?.
Re: Hausübung 4.2 (b)
Wie sehen sieht denn die 2. HPL-Sequenz mit der IH aus?
Ich komm einfach auf keine brauchbare Sequenz.
Für die erste habe ich seqI1 = <{?ø(k)}, ø ||- f(k, append(k, l)) = l>
Ich komm einfach auf keine brauchbare Sequenz.
Für die erste habe ich seqI1 = <{?ø(k)}, ø ||- f(k, append(k, l)) = l>
Re: Hausübung 4.2 (b)
Mein Vorschlag:s_n hat geschrieben:Wie sehen sieht denn die 2. HPL-Sequenz mit der IH aus?
Ich komm einfach auf keine brauchbare Sequenz.
\(seq_{I2} = \left\langle \{ ?::(k) \}, \{ \forall l : list[\text{@I}] \;\; f(tl(k), append(tl(k), l)) = l \} \models f(k, append(k, l)) = l \right\rangle\)
Re: Hausübung 4.2 (b)
müsste es nicht:robert.n hat geschrieben:Mein Vorschlag:s_n hat geschrieben:Wie sehen sieht denn die 2. HPL-Sequenz mit der IH aus?
Ich komm einfach auf keine brauchbare Sequenz.
\(seq_{I2} = \left\langle \{ ?::(k) \}, \{ \forall l : list[\text{@I}] \;\; f(tl(k), append(tl(k), l)) = l \} \models f(k, append(k, l)) = l \right\rangle\)
\(seq_{I2} = \left\langle \{ \neg \emptyset(k) \}, \{ \forall l : list[\text{@I}] \;\; f(tl(k), append(tl(k), l)) = l \} \models f(k, append(k, l)) = l \right\rangle\)
lauten...?
"Unter allen menschlichen Entdeckungen sollte die Entdeckung der Fehler die wichtigste sein.", Stanisław Jerzy Lec
Re: Hausübung 4.2 (b)
Edit: ok das stimmte dann natuerlich nicht, wenn das in der MuLoe falsch ist. Zumindest ist es jetzt eindeutig 

Zuletzt geändert von Ro- am 25. Mär 2010 15:35, insgesamt 1-mal geändert.
Re: Hausübung 4.2 (b)
Nein, das ist nicht ganz richtig wie es in der MuLö gemacht wurde. In der Aufgabenstellung ist angegeben, dass die Induktion der Relationenbeschreibung von list[@I] folgen soll. Und die sieht nunmal so aus:
\(\large R_{list[@I]} = \begin{align} \{ & \langle \{ ?\emptyset(k) \}, \; \emptyset \} \rangle \\ & \langle \{ ?::(k) \}, \; \{\{k/tl(k)\}\} \rangle \} \end{align}\)
Siehe auch hier: http://www.fachschaft.informatik.tu-dar ... 54#p113054
\(\large R_{list[@I]} = \begin{align} \{ & \langle \{ ?\emptyset(k) \}, \; \emptyset \} \rangle \\ & \langle \{ ?::(k) \}, \; \{\{k/tl(k)\}\} \rangle \} \end{align}\)
Siehe auch hier: http://www.fachschaft.informatik.tu-dar ... 54#p113054
Re: Hausübung 4.2 (b)
Warum kommen die anderen Hypothesen "not ?ø(l)" und "eq(hd(l),hd(k))" nicht mit in die Sequenz?
-
- Computerversteher
- Beiträge: 369
- Registriert: 16. Apr 2007 09:12
Re: Hausübung 4.2 (b)
Wie in Kapitel 6 auf Folie 19 definiert werden die Induktionsformeln aus einer Relationenbeschreibung konstruiert. Dabei werden nur die Hypothesen der Relationenbeschreibung berücksichtigt.