ADT

Bachelor Algorithmen und Datenstrukturen
1

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

2

ADT
Hi, in der Lösung von der Aufgabe 6b WS 13/14
https://fsi.informatik.uni-erlangen.de/dw/pruefungen/bachelor/aud/loesungws13

steht:
concat(cons(47, l), cons(2, nil)) = cons(47, cons(l, cons(2, nil)));

heißt das nicht etwa: concat(cons(47, l), cons(2, nil)) = concat(cons(47,cons(2,nil))); ?

3

Ich vermute, die Zeile soll nicht

concat(cons(47, l), cons(2, nil)) = cons(47, cons(l, cons(2, nil)));

sondern

concat(cons(47, l), cons(2, nil)) = cons(47, concat(l, cons(2, nil)));

heißen, da die Signatur der Operation cons folgendermaßen definiert ist:

cons: T x FunList => FunList

Und so verwendet wurde:

cons(l, cons(2, nil))

Wobei l in diesem Kontext eine FunList ist und cons(2, nil) auch zu einer FunList auswertet.

Deine Version verwendet concat falsch:

concat(cons(47,cons(2,nil)))

concat nimmt zwei Argumente, du verwendest es allerdings nur mit einem Argument (“cons(47,cons(2,nil))”).

Ich würde concat mit folgenden Axiomen definieren:

concat(nil, a) = a
concat(a, nil) = a
concat(a, b)   = cons(head(a), concat(tail(a), b))

Die ersten beiden Axiome entsprechen sozusagen dem Basisfall, das dritte Axiom ist der Rekursionsschritt.

4

Dein zweites Axiom ist überflüssig.

5

Ich habe noch eine Frage zur Aufgabe 4 aus der letzten Probeklausur:
https://www2.cs.fau.de/teaching/WS2014/AuD/organisation/oldexams/secure/14-01-13_mini_klausur.pdf´

Als ops habe ich:

create: → AA
get: AA x int → T
set: AA x T x int → AA
delete: AA x int → AA
size: AA → int

kann mir jemand bitte sagen, wie die Axiome lauten?

6
7

Sei a vom Typ AA, t vom Typ T und i, j vom Typ int. Dann ist:

get(create, i) = null
get(set(a, t, i), j) = t für i = j
get(set(a, t, i), j) = get(a, j) sonst
get(delete(a, i), j) = get(set(a, null, i), j)
size(create) = 0
size(set(a, t, i)) = size(a) - 1 für t = null und get(a, i) != null
size(set(a, t, i)) = size(a) + 1 für t != null und get(a, i) = null
size(set(a, t, i)) = size(a) sonst
size(delete(a, i)) = size(set(a, null, i))

8

Delete ist in meinen Augen kein Primäronstruktor des ADTs, da alle möglichen Kombinationen des Objekts durch create und set ausgedrückt werden können. Somit müssen für delete selbst Axiome angegeben werden und delete darf nicht in den Axiomen verwendet werden. Außerdem darf in set null nicht eingefügt werden (siehe Aufgabenstellung), weshalb dieser Fall in size nicht beachtet werden muss.

Mein Vorschlag wäre also der Folgende:

set( L, idx, null ) = L

get(create, idx) = null
get(set(L, idx1, val), idx2) = val falls idx1 == idx2
                             = get(L, idx2) sonst

delete(create, idx) = create                      
delete(set(L, idx1, val), idx2) = L falls idx1 == idx2
                                = set( delete(L,idx2), idx1, val) sonst

size( create ) = 0
size( set(L, idx1, val) ) = 1 + size(L)*

*Die Fallunterscheidung falls val != null oder get(L, idx1) == null, size(L) sonst würde ich an dieser Stelle weglassen, weil man beim Aufstellen der Axiome in der Regel von ADTs in Normalform ausgeht. D.h. die Ausdrücke wurden bereits vereinfacht, so dass nur noch die nötigsten Konstruktoren ausgeführt werden (sonst müsste man ja für jeden Spezialfall von get und set Axiome in size und delete haben). set(L, idx, null) wird daher vereinfach zu L (wie in der Aufgabenstellung angegeben, dass nur Werte != null eingefügt werden können).

9

Mit welchen Axiomen vereinfachst du den Fall, dass get(L, idx1) != null ist?

10

Ich verstehe die Frage nicht ganz bzw. kann nicht zuordnen worauf du dich beziehst.

Meine Aussage ist, dass für size get(L, idx) nicht relevant ist, weil null nicht in das Array eingefügt werden darf. D.h. [m]set( create, 0, null)[/m] würde vereinfacht zu [m]create[/m] oder [m]set( set( create, 0, a), 1, null)[/m] würde vereinfacht zu [m]set(create, 0, a)[/m]. Auf dieser Normalform basieren meine Axiome und somit weiß ich, dass jedes set auch ein Element != null einfügt und ich muss bei size im Wesentlichen nur zählen, wie viele set-Aufrufe ich hatte.

Mir ist gerade aufgefallen, dass ich bei mir
set: AA x int x T → AA
verwendet habe, was nicht dem entspricht, was der Threadersteller gepostet hat. Aber das macht keinen großen Unterschied.

11

Der Grund, wieso ich get(l, idx) auf null prüfen will, ist, dass

set(set(create, 0, a), 1, b)

eine Größe von 2 hat, während die Größe von

set(set(create, 0, a), 0, b)

1 ist. Ist dieser Fall in deiner Normalform auch enthalten?