Datentyp "doppeltverkettete Liste"

Trägermengen (alle mit der Relation = ) :

A (intuitiv Menge der Listenelemente)

W (intuitiv Menge der Listen)

N (intuitiv Menge der Pointernamen)

based on Typ Boolean (wenn wir Abfragen wie islast oder isfirst haben möchten)

Wir nehmen an, daß jede Trägermenge den Wert # (Fehler) enthält und jeder Term, der # enthält als # ausgewertet werden kann.

Operationen:		Abk.	Intuition
leere Liste -> W	e		es existiert kein Listenelement
append AxW -> W	append(a,w)	aw	vor die Liste wird ein Element mit Wert a gehängt
create NxW ->W	create(i,w)	ciw	Pointer i wird auf erstem Listenelement kreiert
delete NxW -> W	delete(i,w)	diw	Pointer i wird von der Liste entfernt
before NxW -> W	before(i,w)	biw	Pointer i wandert ein Element nach vorn
next Nx W ->W	next(i,w)	niw	Pointer i wandert ein Element weiter
put NxWxA -> W	put(i,w,a)	pi,aw	Element mit Wert a wird rechts von Pointer i eingefügt
cut Nx W -> W	cut(i,w)	siw	Element, auf das Pointer i zeigt, wird entfernt samt aller Pointer, die darauf zeigen.
double NxWxN -> W	double(i,w,j)	vi,jw	Pointer j wird kreiert und auf die Stelle gesetzt, auf der Pointer i zeigt.
select NxW ->A	select(i,w)	riw
first W -> A	first(w)	fw	gibt den Wert des ersten Elements
last W -> A	last(w)	lw	gibt den Wert des letzten Elements
isfirst NxW -> B	isfirst(i,w)	fiw	wahr, wenn Pointer i auf das erste El. zeigt
islast NxW -> B	islast(i,w)	liw	wahr, wenn Pointer i auf das letzte El. zeigt

Modelle:

Wir betrachten 2 Modelle. Einmal das Modell aller Terme (Grundmodell), die sich aus den Elementen von N, W,A und B mithilfe der obigen Operationen (öffentlichen und hidden) bilden lassen (Definition über den korrekten Aufbau der Terme) zusammen mit den Axiomen (Axiomenschemata), die angeben welche Terme als äquivalent zu betrachten sind, wie also aus den Termen der freien Termalgebra über diesen Elementen und Operationen, die Elemente unseres Grundmodells als Termklassen entstehen.

Dann das Teilmodell (Listenmodell) der Termklassen aus dem Grundmodell, die einen Standardterm enthalten. Dabei ist ein Standardterm ein Term, der nur aus den Operationen e, append und create aufgebaut ist, d.h. - in unserer abgekürzten Schreibweise - eine Folge ist über den Symbolen e, a, c_i (a in A, i in N), die e nur als Schlußzeichen enthält. Diesen können wir als eine Liste mit Pointern interpretieren. Die Operationen in dem Listenmodell sind nur die öffentlichen Operationen, die allerdings über das Grundmodell definiert werden müssen.

(Zum Vergleich: man kann innerhalb der rationalen Zahlen ein Teilmodell definieren, welches nur die natürlichen Zahlen enthält und die Operation n auf n²+1).

Gleichungen:

Man kann sich die Gleichungen wie Ersetzungsregeln vorstellen, wenn man nur bedenkt, daß sie bidirektional wirken, d.h. man kann die linke Seite durch die rechte Seite ersetzen aber auch umgekehrt die rechte durch die linke. Darum muß man vor allem bei dem Wert "Fehler" # aufpassen, daß man nicht aus dem Term # einen Standardterm zurückerzeugen kann, der nicht gewollt ist (vgl. before oder cut). Dies ist mit ein Grund, warum "hidden operations" nötig werden können.

Hidden Operationen:

Die hidden Operationen kann man sich vorstellen als die zugehörigen öffentlichen Operationen, die nur einen anderen Modus oder Zustand angenommen haben, die also eine (endliche) Information mit sich tragen.

Axiome:

		Bemerkung
delete	die = # diaw = adiw dicjw = cjdiw (i/=j) diciw = w	Pointer nicht gefunden (Fehler) der Operator sucht seinen Pointer der Operator sucht seinen Pointer Pointer gefunden, wird gelöscht, der Operator verschwindet
create	cie = # cicjw = cjciw ciw = cieiw	Kein Pointer kann auf die leeren Liste zeigen (Fehler) die Reihenfolge von Pointern auf demselben Element ist egal der neue Pointer i muß ev. vorher gelöscht werden
hidden delete	eiaw = aeiw eicjw = cjeiw (i/=j) eiciw = w eie = e	der Operator sucht seinen Pointer falsche Pointer werden überlaufen der richtige Pointer wird gelöscht, der Operator verschwindet Pointer nicht gefunden (kein Fehler!), es ändert sich nichts.
next	nie = # niaw = aniw nicjw = cjniw niciaw = aciw	Pointer nicht gefunden (Fehler) der Operator sucht seinen Pointer der Operator sucht seinen Pointer Pointer gefunden, wird versetzt, der Operator verschwindet
before	bie = # biae = # biciw = # biaciw = ciaw bicjw = cjbiw (i/=j) biaw = aBiw	Pointer nicht gefunden (Fehler) Pointer nicht gefunden (Fehler) Pointer auf Start kann nicht verschoben werden (Fehler) (Anfangsbedingung. Im Innern des Terms nicht anwendbar!) Pointer gefunden, wird versetzt, der Operator verschwindet der Operator sucht seinen Pointer Operator sucht weiter, weiß aber, daß er nicht mehr am Anfang der Liste steht.
hidden before	Bie = # Biae = # Biciw Biaciw = ciaw Bicjw = cjBiw (i/=j) Biaw = aBiw	Pointer nicht gefunden (Fehler) Pointer nicht gefunden (Fehler) keine Gleichung, kein Fehler, aber der Operator verschwindet nicht, der Term ist zu keinem Standardterm äquivalent Pointer gefunden, wird versetzt, Operator verschwindet der Operator sucht seinen Pointer der Operator sucht seinen Pointer
put	pibe = # pibaw = apibw pibcjw = cjpibw (i/=j) pibaciw = ciabw	Pointer nicht gefunden (Fehler) der Operator sucht seinen Pointer der Operator sucht seinen Pointer Pointer gefunden, Element eingefügt, Operator absorbiert
cut	sie = # siaw = asiw siciw = Tw Tcjw = Tw Taw = w sicjw = cjtiw (i/=j)	Pointer nicht gefunden (Fehler) der Operator sucht seinen Pointer Pointer gefunden, hidden Operator T löscht alle übrigen Pointer, die auf dieses Element zeigen. Operator trifft auf einen anderen Pointer und merkt sich das (Der Operator löscht seinen Pointer nur wenn er ihn als ersten in der Pointerliste findet, um sicherzustellen, daß alle Pointer auf demselben Element durch T mitgelöscht werden.)
hidden cut	tie = # ticjw = citiw (i/=j) tiaw = asiw ticiw	Pointer nicht gefunden (Fehler) der Operator sucht seinen Pointer Operator steht ev. wieder am Anfang einer Pointerliste keine Gleichung, der Operator verschwindet nicht, der Term ist zu keinem Standardterm äquivalent
dopple	viiw = # vije = # vijaw = avijw vijckw = ckvijw (i/=k,j/=k) vijcjw = vijw vijciw = cjciejw (i/=j)	Pointer i verdoppel ist nicht erlaubt Pointer nicht gefunden (Fehler) der Operator sucht seinen Pointer der Operator sucht seinen Pointer Pointer j gefunden, wird gelöscht Pointer i gefunden, Pointer j gesetzt, hidden Löschoperator für ev. späteren Pointer j erstellt.
select	rie = # riaw = riw ricjw = cjriw (i/=j) riciaw = a ricicjw	Pointer nicht gefunden (Fehler) der Operator sucht seinen Pointer der Operator sucht seinen Pointer Pointer gefunden, Wert wird ausgegeben keine Gleichung, Pointer müssen getauscht werden
first	fe = # fciw = fw faw = a	Liste leer (Fehler) der Operator sucht erstes Element erstes Element gefunden
last	le = # labw = lbw laciw = law lciw = lw lae = a	Liste leer (Fehler) der Operator sucht letztes Element der Operator sucht letztes Element der Operator sucht letztes Element letztes Element gefunden
isfirst	ficiaw = true ficjw = fiw (i/=j) fiaw = false fie = false	Pointer auf erstem Element gefunden der Operator sucht seinen Pointer Pointer nicht an erstem Element gefunden Pointer i existiert nicht, zeigt also nicht auf erstes Element
islast	liciae = true liciabw = false liciacjw = liciaw lie = false licjw = liw (i¹j) liaw = liw	Pointer auf letztem Element gefunden Pointer gefunden, aber nicht auf letztem Element Pointer gefunden, die Pointer auf nächstem Element gelöscht Pointer i existiert nicht, zeigt also nicht auf letztes Element Operator sucht seinen Pointer Operator sucht seinen Pointer