Hausübung 4.2 (b)

s_n
Windoof-User
Windoof-User
Beiträge: 37
Registriert: 24. Aug 2009 16:43
Wohnort: Darmstadt
Kontaktdaten:

Hausübung 4.2 (b)

Beitrag von 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-
Neuling
Neuling
Beiträge: 5
Registriert: 25. Jan 2009 21:34

Re: Hausübung 4.2 (b)

Beitrag von -me- »

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

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

Re: Hausübung 4.2 (b)

Beitrag von Simon Siegler »

s_n hat geschrieben: 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
Windoof-User
Windoof-User
Beiträge: 37
Registriert: 24. Aug 2009 16:43
Wohnort: Darmstadt
Kontaktdaten:

Re: Hausübung 4.2 (b)

Beitrag von 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
Nerd
Nerd
Beiträge: 673
Registriert: 29. Sep 2008 19:17

Re: Hausübung 4.2 (b)

Beitrag von robert.n »

s_n hat geschrieben: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\)

Benutzeravatar
oren78
BSc Spammer
BSc Spammer
Beiträge: 1373
Registriert: 17. Nov 2006 17:47
Wohnort: Darmstadt

Re: Hausübung 4.2 (b)

Beitrag von oren78 »

robert.n hat geschrieben:
s_n hat geschrieben: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...?
"Unter allen menschlichen Entdeckungen sollte die Entdeckung der Fehler die wichtigste sein.", Stanisław Jerzy Lec

Ro-
Erstie
Erstie
Beiträge: 15
Registriert: 1. Apr 2008 21:58

Re: Hausübung 4.2 (b)

Beitrag von Ro- »

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.

robert.n
Nerd
Nerd
Beiträge: 673
Registriert: 29. Sep 2008 19:17

Re: Hausübung 4.2 (b)

Beitrag von 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
Windoof-User
Windoof-User
Beiträge: 37
Registriert: 24. Aug 2009 16:43
Wohnort: Darmstadt
Kontaktdaten:

Re: Hausübung 4.2 (b)

Beitrag von s_n »

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

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

Re: Hausübung 4.2 (b)

Beitrag von 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.

Antworten

Zurück zu „Archiv“