Algebraische Definition eines ADT

RedWing

Hallo,
ich hoffe ich bin hier richtig und mir kann jemand helfen.

Folgender Datentyp sei zu definieren:

queue // Liste

Mit folgenden Operationen:

create: --> queue /* Erzeugen */ 
enqeue: queue x element --> queue /* Hinten anfügen */
dequeue: queue --> queue /* 1. Element entfernen*/ 
front: queue --> element /* 1. Element liefern */ 
empty: queue -- > boolean /*Schlange leer?*/

Unser Prof hat nun folgende Eigenschaften fest gelegt:

Es existieren:
q: queue ; x: element

=> folgende Eigenschaften der Operationen:

empty(create()) = true 
empty ( enqueue(q,x)) = false 
front(create()) = undefiniert
front ( enqueue (q,x)) = if (empty (q)) then x else front (q) 
dequeue( create) = undefiniert
dequeue(enqueue(q,x))= if ( empty(q)) then q else enqueue (dequeue(q), x)

Da aber weder if noch then noch else als Operationen des ADT
festgelegt wurden, frag ich mich ob die Definition gültig ist?

Kann man das vielleicht auch ohne diese vom Himmel herkommenden
Operationen definieren?

Danke und Gruß

RedWing

Vertexwahn

BTW: was ist ein ADT?
ist das ne formale Sprache zur Beschreibung der Semantik einer Programmiersprache?

interpreter

Vertexwahn schrieb:

BTW: was ist ein ADT?
ist das ne formale Sprache zur Beschreibung der Semantik einer Programmiersprache?

Vermutlich "abstrakter Datentyp". Allerdings habe ich keine Ahnung, was diese Konstrukte darstellen sollen (auch wenns irgendwie wie eine funktionale Programmiersprache aussieht).

{\Large
hmm ich denke bei front k"onnte man auch schreiben:\
$front(enque(create(),x)) = x$ \
front(enque(\dots enque(enque(create(),x\_0),x\_1)\dots x\_n))=x\_0\
aber warum sollte man "`if--then--else"' nicht benutzen? es ist schliesslich keine richtige sprache, sondern du definierst bloss die axiome, also damit man weiss in welchem fall die funktion, definiert ist und wie sie in diesem fall definiert ist.
}$$

Betrache den if-then-else Operator als Teil der Sprache (aufgeblähte Prädikatenlogik), mit der die Axiome definiert werden. Zu dieser Sprache gehören doch auch Ausdrücke für Abbildungen, Gleichungen, Wahrheitswerte, Junktoren, etc.

if-then-else ist also KEINE Operation des jeweiligen Datentyps sondern kann in eurem Fall als gegeben angesehen werden. Hat aber der Prof bestimmt irgendwo definiert, oder?

ADT steht wirklich für Abstrakter Datentyp. Es ist keine (funktionale) Programmiersprache!
Auf eine konkrete Realisierung des Datentyps wird verzichtet. Man interessiert sich vorerst nur für die Eigenschaften der Operationen und welche Auswirkungen ihre Verknüpfung hat.
Ob weitere Eigenschaften gelten kann man dann z.B. mit automatischen Beweisern prüfen. Schwierig ist es aber eben sicherzustellen, ob mit den wenigen Axiomen wirklich alles abgedeckt wird.

RedWing

space schrieb:

Betrache den if-then-else Operator als Teil der Sprache (aufgeblähte Prädikatenlogik), mit der die Axiome definiert werden. Zu dieser Sprache gehören doch auch Ausdrücke für Abbildungen, Gleichungen, Wahrheitswerte, Junktoren, etc.

if-then-else ist also KEINE Operation des jeweiligen Datentyps sondern kann in eurem Fall als gegeben angesehen werden. Hat aber der Prof bestimmt irgendwo definiert, oder?

ADT steht wirklich für Abstrakter Datentyp. Es ist keine (funktionale) Programmiersprache!
Auf eine konkrete Realisierung des Datentyps wird verzichtet. Man interessiert sich vorerst nur für die Eigenschaften der Operationen und welche Auswirkungen ihre Verknüpfung hat.
Ob weitere Eigenschaften gelten kann man dann z.B. mit automatischen Beweisern prüfen. Schwierig ist es aber eben sicherzustellen, ob mit den wenigen Axiomen wirklich alles abgedeckt wird.

Erstmal danke für die vielen Antworten.
@space
@.wasiliy:
Ihr habt das alles schon richtig erfasst.
Deine Erklärung scheint mir einleuchtend, aber irgendwie trotzdem unbefriedigend
da es ja eine "algebraische" Definition eines ADT ist, und meiner Meinung
nach if then else nicht zur Definition gehören da sie auch nicht festglegt
wurden.
Mein Prof hat if, then, else einfach nur in die Lösung geschrieben ohne
zu klären woher die kommen.
Das mit den Werten true, false etc is natürlich ein Argument...

Zu dieser Sprache gehören doch auch Ausdrücke für Abbildungen, Gleichungen, Wahrheitswerte, Junktoren, etc.

Mhm das wurde uns in der Vorlesung nicht gelehrt.
Naja wie auch immer ich werds in der Prüfung einfach mal als gegeben
dahinnehmen, falls ich drauf zurück greifen muss.

Danke und Gruß

RedWing