Abstrakte Datentypen

[Plauzi92]

Hallo Community,

ich bräuchte einen Denkanstoß zu folgender Aufgabe:

Gegeben ist die Spezifikation eines Listen-ADTs in List.asl

specification list
imports
bool
nat
sorts
List
Elem
constructors
nil : -> List // Empty list
cons : Elem x List -> List // Head element and tail list
functions
head : List -> Elem? // Head element
tail : List -> List? // List without head
isNil : List -> Bool // Test for nil list
length : List -> Nat // Number of elements in the list
append : List x List -> List // Append two lists
snoc : List x Elem -> List // Friend of cons
last : List -> Elem? // Last element
init : List -> List? // List without last
variables
e : Elem
l : List
l1 : List
l2 : List
equations
head(cons(e, l)) = e
tail(cons(e, l)) = l
isNil(nil) = true
isNil(cons(e, l)) = false
length(nil) = zero
length(cons(e, l)) = succ(length(l))
append(nil, l) = l
append(cons(e, l1), l2) = cons(e, append(l1, l2))
snoc(l, e) = append(l, cons(e, nil))
last(cons(e,l)) = if isNil(l) then e else last(l)
init(cons(e,l)) = if isNil(l) then nil else cons(e, init(l))

Ich soll nun noch zwei Funktionen hinzufügen:

- remove: Nat x List -> List
// entfernt an einer Stelle ein Element. Bsp.: remove(2,[5,6,8,42]) = [5,6,42]
- revert: List -> List
// kehrt die Liste um. Bsp.: revert([5,6,8,42]) = [42,8,6,5]

Die Funktionen übernehme ich ja erstmal so wie sie beschrieben sind und schreibe sie unter functions. Also muss ich "nur noch" die equations und variables einfügen.

Bei den equations komme ich aber schon nicht wirklich weiter.

Die equations sollen ja alle Abfragen abdecken. Fehlerfälle müssen nicht reingeschrieben werden. Bis jetzt hatten wir schon mal die Methode "get" hinzugefügt, die eine natürliche Zahl und eine Liste erhält, und dann das Element in der Liste mit dem entsprechenden Index (also die natürliche Zahl) zurück gibt.

Die Funktion hieß: get : Nat x List → Elem?

variables: n: Nat

und die ecuations:
get(zero, cons(e, l)) = e
get(succ(n), cons(e, l)) = get(n, l)

Also falls die natürliche Zahl null ist, geben wir einfach das erste Element zurück, andernfalls geben wir das Element an der Stelle n zurück. Sieht für mich so aus, als würde er rekursiv durchlaufen bis n getroffen wurde.

Bei den jetzigen Funktionen soll ich aber ja nicht einfach irgendwas ausgeben, sondern muss vorher noch etwas verändern. In Java wären die Methoden in zwei Minuten geschrieben aber mir ist die Nummer einfach (achtung Witz) zu abstrakt.

Die Funktionen an sich kann ich ja noch nachvollziehen, da man ja einfach nur die Datentypen die "rein und rausgehen" aufschreibt.
Für die Remove Funktion dachte ich daran die Zahl mit dem entsprechenden Index an das Ende zu setzen und mir dann die Liste ohne "tail" ausgeben zu lassen. Wie ich das aufschreiben soll ist mir aber auch nicht ganz klar.

Wäre super wenn mir jemand helfen könnte

 

[mihe7]

Vielleicht so in der Art:

remove(zero, cons(e, l)) = l
remove(succ(n), cons(e, l)) = cons(e, remove(n, l))

 

[Plauzi92]

Also die equations sind ja Axiome. Das heißt ja, dass sie nur Bedingungen sind die gelten müssen aber nicht wirklich Ergebnisse liefern oder? Ich glaube ich denke zu kompliziert.

- Für die Remove Funktion wär ja eine Bedingung, dass wenn ich eine 0 einsetze, das erste Element gestrichen wird.
Wie du schon sagtest: remove(zero, cons(e, l)) = l

- Eine Weitere Bedingung wäre, dass wenn der Parameter gleich der Länge der Liste ist, das letzte Element gestrichen wird. Dafür wird die Methode init(cons(e,l)) genutzt, da sie die Liste ohne das letzte Element ausgibt.

Überlegung: remove(length(cons(e, l), (cons(e, l)) = init(cons(e,l))

Außerdem muss die Liste nach der Methode um 1 kürzer sein als vorher.
Da weiß ich aber nicht wie ich das schreiben soll, da ich ja schlecht length-1 in die Abstraktion schreiben kann.

Die Letzte wäre deine Zweitgenannte:

remove(succ(n), cons(e, l)) = cons(e, remove(n, l))

Also ruft man remove auf und übergibt dann den Nachfolger von n und die Liste mit e als Anfang und l als Rest. Das soll dann das gleiche sein wie die Liste zwischen e und remove(n,l).. ich bin komplett verwirrt..

 

[Plauzi92]

Zu der Länge ist mir noch was eingefallen:

succ(length(remove(n , cons(e, l))))) = length(cons(e,l))

Also der Nachfolger der Länge der Liste nach remove muss so groß sein wie die Länge der Liste..

 

[mihe7]

Zum remove: die Funktion liefert eine "modifizierte Liste", die alle Elemente der Ursprungsliste mit Ausnahme des n-ten Elements enthält.

Ist die Liste nil, ist die modifizierte Liste auch nil:

remove(n, nil) = nil

Ist die Liste dagegen nicht nil, dann kann man sie in Form von Kopfelement und Rest darstellen, wobei der Rest wieder eine Liste ist: cons(e, l) = Liste mit Kopfelement e und Rest-Liste l. Eine Liste mit einem Element wäre dann also cons(e, nil).

Wird das erste Element entfernt, bleibt einfach die Rest-Liste übrig:

remove(zero, cons(e,l)) = l

Bis dahin alles recht einfach. Jetzt überlegt man sich folgendes: wird nicht das erste Element entfernt, muss das Entfernen in der Rest-Liste geschehen. Das Ergebnis ist also eine Liste, die aus dem ersten Element und einer modifizierten Rest-Liste besteht:

remove(succ(n), cons(e, l)) = cons(e, remove(n, l))

Fertig.

Eine Weitere Bedingung wäre, dass wenn der Parameter gleich der Länge der Liste ist, das letzte Element gestrichen wird.

Das ist zunächst einmal falsch, da das erste Element sich an Stelle 0 befindet. In einer Liste der Länge n belegen die Elemente die Stellen 0 bis n-1. Daneben ist die Behandlung des letzten Elements auch überflüssig, weil das oben schon enthalten ist.

Nehmen wir mal die Liste aus Deinem Beispiel und entfernen das letzte Element: remove(3,[5,6,8,42]). Es ist 3 = succ(succ(succ(zero))) betrachten, also

remove(succ(succ(succ(zero))), [5,6,8,42]) =
cons(5, remove(succ(succ(zero)), [6,8,42])) =
cons(5, cons(6, remove(succ(zero), [8, 42]))) =
cons(5, cons(6, cons(8, remove(zero, [42])))) =
cons(5, cons(6, cons(8, remove(zero, cons(42, nil)))))

Das Ergebnis von remove(zero, cons(42, nil)) = nil (per Definition), es folgt:

cons(5, cons(6, cons(8, nil))) =
cons(5, cons(6, [8]) =
cons(5, [6, 8]) =
[5, 6, 8])

 

[Plauzi92]

Erstmal vielen Dank für deine Mühe!

Dann hab ich tatsächlich einfach zu kompliziert gedacht. Man könnte demnach sagen, dass die Equations alle Ausgaben abfangen, aber nicht für jede einzelne Eingabe definiert sind. (Klingt so auch logischer, aber es dauerte einen Moment)

Also da remove(succ(n), cons(e, l)) = cons(e, remove(n, l)) alle Ausgaben bis auf die Null enthält, muss ich die Länge nicht mehr testen.
Kam mir irgendwie merkwürdig vor, dass die drei Equations ausreichen. Dann versuche ich mich mal an der Reverse Funktion.

 

[Plauzi92]

Ich hab nochmal in meinen Unterlagen nachgeschaut. Ich gebe in beiden Funktionen Listen aus. Diese haben zwei Konstruktoren welche jeweils zwei "zustände" haben. List ist entweder nil, oder cons(e,l) und Element ist entweder null(zero) oder eine folgende Zahl von null.

Demnach gibt es für die Remove Funktion 4 Equations:

remove(n,nil) = nil; // Ist ein Fehler und kann gestrichen werden.
remove(zero,nil) = nil; // Ist ein Fehler und kann gestrichen werden.

Bleiben nur noch zwei über die eingetragen werden müssen.

1. remove(zero, cons(e,l)) = l

2. remove(succ(n), cons(e, l)) = cons(e, remove(n, l))

Der Revert Funktion übergebe ich ja nur eine Liste. Also können es nur zwei Equations sein.

1. revert(nil) = nil // Kann gestrichen werden wie oben

2. revert(cons(succ(e),l)) = cons(last(cons(e,l), revert(l))

Die Idee hinter der Zweiten: Nachfolger vom Head da ich beim Aufruf später ja weiter zählen muss. Auf der rechten Seite erstelle ich die neue Liste deren Head die Letzte aus dem Vorgänger war und rufe für den Tail die Methode erneut auf.
Da in der Aufgabenstellung aber auch explizit steht, dass man Variablen erstellen soll und ich nicht mal die vorhandenen alle genutzt habe, bin ich mir dann doch nicht mehr allzu sicher ob meine Überlegung stimmt.

 

[mrBrown]

Da in der Aufgabenstellung aber auch explizit steht, dass man Variablen erstellen soll und ich nicht mal die vorhandenen alle genutzt habe, bin ich mir dann doch nicht mehr allzu sicher ob meine Überlegung stimmt.

In remove nutzt du eine neue Variable

Der Revert Funktion übergebe ich ja nur eine Liste. Also können es nur zwei Equations sein.
[...]
Die Idee hinter der Zweiten: Nachfolger vom Head da ich beim Aufruf später ja weiter zählen muss. Auf der rechten Seite erstelle ich die neue Liste deren Head die Letzte aus dem Vorgänger war und rufe für den Tail die Methode erneut auf.

Revert sieht deutlich zu kompliziert aus. Kleiner Hint: Es gibt da so einen "Friend of cons", den man da ziemlich gut nutzen kann

 

[Plauzi92]

In remove nutzt du eine neue Variable

Ist ein Argument..

snoc(l, e) = append(l, cons(e, nil))

snoc bedeutet ja, dass ich das Element "e" hinten an die Liste von "l" hänge.

revert(snoc(cons(e, l), succ(e)) = cons(e, revert(l, e))

Idee: Ich setze den Nachfolger von e an die erste Stelle der Liste. Auf der rechten Seite erstelle ich eine modifizierte Liste die einen Head hat und deren Tail nochmal die Methode durchläuft. So setze ich in jedem Durchlauf den Head an die letzte Position.

 

[mrBrown]

Immer noch zu kompliziert gedacht (und afaik ist der Ausdruck auf der linken Seite auch gar nicht möglich)


zum umdrehen musst du doch nur das erste Element an die umgedrehte Rest-Liste hängen. Auf der linken Seite brauchst du da nicht mehr als revert(cons(e, l))

 

[Plauzi92]

Danke nochmal für die vielen Tipps!

Auf der rechten Seite brauche ich aber doch in jedem Fall nochmal den Funktionsaufruf von revert. Andernfalls würde ich insgesamt ja nur ein Element verschieben. Ich denke, dass ich bei einem snoc auch keinen succ brauche. Ich suche ja nicht nach einem bestimmten Element in der kompletten Liste sondern tausche sie einmal komplett. Das macht snoc ja sowieso wenn er mehrmals durch erneuten Aufruf von revert durchläuft.

revert(cons(e, l)) = snoc(e, revert(cons(e, l) ))

Bin mir aber auch nicht sicher ob ich ein Element mit einem Funktionsaufruf durch snoc verbinden kann. Da ich aber wohl durchgehend zu kompliziert denke, habe ich das jetzt so kurz wie (mir) möglich gemacht..

 

[mrBrown]

Da ich aber wohl durchgehend zu kompliziert denke, habe ich das jetzt so kurz wie (mir) möglich gemacht..

Ist immer noch zu lang

Du hast jetzt auf beiden Seiten einen identischen Teil stehen, das führt nur zu endloser Rekursion

 

[Plauzi92]

Jetzt rufe ich in der revert nur noch den Tail auf: Wollte erst einen succ reinschreiben weil du sagtest endlos. Wäre dann aber vermutlich wieder zu lange

revert(cons(e, l)) = snoc(e, revert(l))