Abstrakte Datentypen (3)

Bereits in der Termalgebra können wir mit Listen rechnen und auch zusätzliche Funktionen definieren, wie etwa zum Verketten von zwei Listen:
OPERATIONS:
append: list list list
RULES:
append(newlist, l) = l
append(cons(x, l1), l2) = cons(x, append(l1, l2))
Durch diese rekursive Definition ist die Funktion vollständig festgelegt; ihr Ergebnis läßt sich immer auf Grundterme reduzieren. Nach dem gleichen Schema lassen sich weitere nützliche Funktionen aufbauen.

Algebraische Spezifikationen sind schon lange bekannt. So sind die Grundterme des folgenden abstrakten Datentyps

ADT Nat IS
SORTS: Nat
OPERATIONS:
eins: Nat
nach: Nat Nat
RULES:
nach(x) = nach(y) x = y
END Nat .
gerade die natürlichen Zahlen; dieses System hat darüberhinaus noch andere Modelle. Die Forderung, daß die Zahl 1 nicht Nachfolger  ist, und auch das Induktionsaxiom,  das wir in unserem Formalismus nicht formulieren können, ergeben sich gerade durch die Beschränkung auf die Grundterme. Die arithmetischen Operationen erhalten wir in gewohnter Weise durch
OPERATIONS:
add: Nat Nat Nat
mult: Nat Nat Nat
RULES:
add(x, eins) = nach(x)
add(x, nach(y)) = nach(add(x, y))
add(x, y) = add(y, x)
mult(x, eins) = x
mult(x, nach(y)) = add(mult(x, y), x)
mult(x, y) = mult(y, x)

zurück | Inhalt | Index | vor | Vorlesung
Klaus Lagally, 22. Februar 2000, 19:35