Hausübung 4.2 (b)

[s_n]

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.

[-me-]

Wie auf Seite 18 von Kapitel 9 steht wird * durch den Prozeduraufruf mit gleichen Parametern ersetzt.

[Simon Siegler]

Wie behandelt man die Stuck Terme wenn man die Sequenzen bauen will?
Lässt man die weg ?.

In Aufgabe 4.2 (b) spielen Stuck-Terme keine Rolle. Wie in Teilaufgabe (a) vorzugehen ist, wurde bereits erläutert.

[s_n]

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>

[robert.n]

Wie sehen sieht denn die 2. HPL-Sequenz mit der IH aus?
Ich komm einfach auf keine brauchbare Sequenz.

Mein Vorschlag:
\(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\)

[oren78]

Wie sehen sieht denn die 2. HPL-Sequenz mit der IH aus?
Ich komm einfach auf keine brauchbare Sequenz.

Mein Vorschlag:
\(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\)

müsste es nicht:

\(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...?

[Ro-]

Edit: ok das stimmte dann natuerlich nicht, wenn das in der MuLoe falsch ist. Zumindest ist es jetzt eindeutig

[robert.n]

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

[s_n]

Warum kommen die anderen Hypothesen "not ?ø(l)" und "eq(hd(l),hd(k))" nicht mit in die Sequenz?

[Simon Siegler]

Wie in Kapitel 6 auf Folie 19 definiert werden die Induktionsformeln aus einer Relationenbeschreibung konstruiert. Dabei werden nur die Hypothesen der Relationenbeschreibung berücksichtigt.