3.7.1 Symbolische Manipulation

Wir zeigen in diesem Abschnitt anhand von drei Beispielen, wie mittels der SML-Konzepte Konstruktorterme und regelorientierte Funktionsdefinition, symbolische Manipulation von Daten klar und knapp formuliert werden kann.

Symbolisches Differenzieren. Der folgende Typ beschreibt die abstrakte Syntax der Klasse von Funktionen, die wir differenzieren können wollen.

dataype expr = constant of int
             | variable of string
             | sum of exp list
             | product of expr list

Es folgen ein paar Beispiele von Funktionsausdrücken:

val u = variable("u")
val v = variable("v")
val w = variable("w")
val e = product [v, sum [u,v,w]];
val zero = constant(0)
val one = constant(1);

Das Differenzieren erfolgt nach den üblichen Regeln:

fun d x (constant _) = zero
  | d (variable s) (variable t) = if s=t then one else zero
  | d x (sum Elist) = sum (map (d x) Elist)
  | d x (product []) = zero
  | d x (product [E]) = d x E
  | d x (product (E1::Elist)) =
    let val EP = product(Elist)
        val T1 = product [d x E1, EP]
        val T2 = product [E1, d x EP]
    in sum [T1, T2]
    end;

Man beachte die Verwendung von map, welches eine Funktion auf eine Liste elementweise fortsetzt, und wie folgt definiert ist:

fun map _nil = nil
  | map f (x::l) = (f x)::(map f l)

Da wir d als eine Funktion vom Typ d : exp → exp → exp geschrieben haben, können wir sie partiell auf die Variable x applizieren, nach der differenziert werden soll. Es ergibt sich eine Funktion (dx) : exp → exp, die Ausdrücke speziell nach x differenziert. In der Regel

                 d x (sum Elist) = sum (map (d x) Elist)

wird daher die Liste Elist der Summanden einer Summe in gewünschter Weise differenziert. Man beachte, daß map (d x) die Spezialisierung von map ist, die die Fortsetzung von (dx) auf Listen repräsentiert. Hier ein Beispiel für die Anwendung von d, wobei der Audruck e nach der Variablen u differenziert wird.

- val e' = d u e;
val e' =
  sum
    [product
       [constant 0,product [sum [variable "u",variable "v",variable "w"]]],
     product [variable "v",sum [constant 1,constant 0,constant 0]]] : expr

Da dies noch stark vereinfacht werden kann, schreiben wir noch einen Vereinfacher. Wir brauchen folgende Hilfsfunktionen:

fun member _nil = false
  | member x (y::l) = if x=y then true else member x l;
exception Delete;
fun delete _nil = raise Delete
  | delete x (y::l) = if x=y then l else y::(delete x l);

Dann schreiben wir zunächst alle Simplifikationsregeln als Funktion rule auf.

exception NotSimplifiable;
fun rule (sum [E]) = E
  | rule (product [E]) = E
  | rule (sum []) = zero
  | rule (product []) = one
  | rule (sum Elist) =
    (sum (delete (constant 0) Elist) handle Delete => raise NotSimplifiable)
  | rule (product Elist) =
    if member (constant 0) Elist
       then (constant 0)
       else (product (delete (constant 1) Elist)
            handle Delete => raise NotSimplifiable)
  | rule _= raise NotSimplifiable;

Hierbei verwenden wir den Ausnahmeindikator NotSimplifiable um anzuzeigen, wenn keine Regel (an der Spitze) des gegebenen Ausdrucks anwendbar ist. Man beachte die Umsetzung des Ausnahmeindikators Delete zu NotSimplifiable, wie sie beispielsweise in der Regel

rule (sum Elist) =
 (sum (delete (constant 0) Elist) handle Delete => raise NotSimplifiable)

stattfindet. Auf die Summe (sum Elist) ist keine Simplifikationsregel anwendbar, wenn keiner der Summanden die Form (constant 0) hat. Dieses wird von der Funktion delete durch den Ausnahmewert Delete angezeigt. Andernfalls wird das erste Auftreten von (constant 0) gelöscht, was der Anwendung einer Simplifikationsregel x+0 → x oder0 + x → x entspricht.

rule wendet immer höchstens eine Regel auf einen Ausdruck an, und zwar nur an seiner Spitze. Um einen Ausdruck vollständig zu reduzieren, müssen wir rule iteriert und an allen Teiltermen aufrufen. Damit schreiben wir also:

fun simplify (sum Elist) =
    let val E1 = sum (map simplify Elist)
    in simplify (rule E1) handle NotSimplifiable => E1
    end
  | simplify (product Elist) =
    let val E1 = product (map simplify Elist)
    in simplify (rule E1) handle NotSimplifiable => E1
    end
  | simplify E = E;

Wie gewünscht erhalten wir damit

- simplify (d u e);
val it = variable "v" : expr

Merke:

• Spezialisierte Varianten von mehrstelligen Funktionen erhält man durch partielle Applikation. Dazu muß die mehrstellige Funktion in currifizierter Form geschrieben werden. Spezialisierung ist dann besonders nützlich, wenn ein Parameter eine eher globale Bedeutung hat, also weniger dynamisch agiert, als andere Parameter.

• map verwendet man zur Fortsetzung von (spezialisierten) Funktionen auf Listen.

• Speziellere Regeln bei Funktionsdefinitionen werden zuerst geschrieben.

• Bei Reduktion durch Termersetzung durch die Verwendung von Ausnahmeindikatoren als Abbruchsbedingung für Termination sorgen.

Übersetzerbau. Wir schreiben einen Übersetzer für eine einfache Programmiersprache für while-Programme. Die abstrakte Syntax der Quellsprache sei wie folgt gegeben:

datatype
    ('id,'op,'type) prog =
    program of ('id,'op,'type) stat
and ('id,'op,'type) stat =
    & of ('id,'op,'type) stat * ('id,'op,'type) stat
  | decl of 'id * 'type
  | assign of 'id * ('id,'op) exp
  | ifstat of ('id,'op) exp * ('id,'op,'type) stat * ('id,'op,'type) stat
  | whilestat of ('id,'op) exp * ('id,'op,'type) stat
  | skip
and ('id,'op) exp =
    unop of 'op * ('id,'op) exp
  | binop of ('id,'op) exp * 'op * ('id,'op) exp
  | var of 'id
  | bconst of bool
  | const of int;
infix &;

Konkrete Instanziierungen für die oben noch offengelassenen Typen für arithmetische und logische Operatoren sowie für Typen in der Quellsprache könnten sein:

datatype types = intType | boolType;
datatype ops   = minus | not | plus | logicalOr | less | greater;

Damit wäre ein einfaches Quellprogramm, welches y = 2 ∗ x berechnet, durch

val p = program (decl("x",intType) & decl("y",intType) &
 whilestat(binop(var "x",greater, const 0),
 assign("x",binop(var "x",minus,const 1)) &
 assign("y",binop(var "y",plus, const 2))
  )
);

gegeben. Als Zielsprache wählen wir eine Kellermaschinensprache.

datatype 'op ins =
    ^of 'op ins * 'op ins
  | store of int
  | load of int
  | loadConst of int
  | loadBConst of bool
  | uop of 'op
  | bop of 'op
  | define of int
  | goto of int
  | jumpF of int
  | nop;

^ist die sequentielle Komposition von Befehlen. load i lädt den Wert der Zelle i in den Keller. store i speichert den Inhalt des obersten Kellerelementes in die Zelle i. uop o bzw. bop i wendet die Operation o auf das oberste (die obersten beiden) Kellerelement(e) an, löscht diese Kellerelemente und speichert das Ergebnis auf dem Keller. loadConst c bzw. loadBConst c bringen die Konstante c auf den Keller. goto l und jumpF l sind Sprungbefehle an die Marke l. Im letzteren Fall wird nur gesprungen, falls das oberste Kellerelement den Wert false enthält. define l dient zur Definition von Marken.

Es folgen einige Hilfsstrukturen für Symboltabellen und Typprüfung.

type 'id symtab = 'id * types * int list;
exception undeclared_id;
fun lookup(nil,x) = raise undeclared_id
  | lookup((y,ty,addr)::st,x)   = if x=y then (ty,addr) else lookup(st,x);
(* Funktionen zur Typpr"ufung bei Operatoren *)
exception type_error;

fun resultType1(minus,intType) = intType
  | resultType1(not,boolType) = boolType
  | resultType1(_,_) = raise type_error;
fun resultType2(plus,intType,intType)   = intType
  | resultType2(minus,intType,intType)   = intType
  | resultType2(less,intType,intType)   = boolType
  | resultType2(greater,intType,intType)  = boolType
  | resultType2(_,_,_)   = raise type_error;

Schließlich definieren wir den Übersetzer durch rekursiven Abstieg über das Quellprogramm. Dabei wird jedes Konstrukt in einer Umgebung übersetzt, die durch verschiedene zusätzliche Parameter gegeben wird. st, die Symboltabelle, enthält die jeweils sichtbaren Bindungen. Bindungsinformation für jede Variable ist ihre Speicheradresse. Speicheradressen werden durch den Zähler az gezählt. entsprechend zählt lz die bereits vergebenen Markennummern. Ergebnisparameter sind der erzeugte Code code sowie die veränderten Umgebungsbestandteile, die sich durch die Übersetzung eines Programmkonstruktes ergeben haben. Hinzukommt Typinformation für Ausdrücke.

fun compileExp(const i,st) = (intType, loadConst i)
  | compileExp(bconst b,st) = (boolType,loadBConst b)
  | compileExp(var x,st) =
let val (ty,addr) = lookup(st,x) in (ty,load addr) end
  | compileExp(unop(oper,e),st) =
let val (ty_e,code_e) = compileExp(e,st)
in (resultType1(oper,ty_e),code_e^uop(oper))
end
  | compileExp(binop(e1,oper,e2),st) =
let val (ty_e1,code_e1) = compileExp(e1,st);
    val (ty_e2,code_e2) = compileExp(e2,st)
in  (resultType2(oper,ty_e1,ty_e2),code_e1^code_e2^bop(oper))
end
and
    compileStat(whilestat (e,s),st,az,lz) =
let val (typ_e,code_e) = compileExp(e,st);
    val (st1,az1,lz1,code_s) = compileStat(s,st,az,lz+2)
in if typ_e = boolType then
      (st1,az1,lz1,define(lz+1)^code_e^jumpF(lz)^code_s^goto(lz+1)^define(lz))
   else raise type_error
end
  | compileStat(skip,st,az,lz) = (st,az,lz,nop)
  | compileStat(ifstat(e,p,q),st,az,lz) =
let val (typ_e,code_e) = compileExp(e,st);
    val (st1,az1,lz1,code_p) = compileStat(p,st,az,lz+2)
    val (st2,az2,lz2,code_q) = compileStat(q,st1,az1,lz1)
in  if typ_e = boolType then

    (st2,az2,lz2,code_e^jumpF(lz+1)^code_p^goto(lz)^
              define(lz+1)^code_q^define(lz))
    else raise type_error
end
  | compileStat(assign(v,e),st,az,lz) =
let val (ty_v,addr) = lookup(st,v);
    val (ty_e,code_e) = compileExp(e,st)
in  if ty_v = ty_e then (st,az,lz,code_e^store(addr))
    else raise type_error
end
  | compileStat(decl(x,ty),st,az,lz) = ((x,ty,az)::st,az+2,lz,nop)
  | compileStat(s1 & s2,st,az,lz) =
let val (st1,az1,lz1,code_s1) = compileStat(s1,st,az,lz);
    val (st2,az2,lz2,code_s2) = compileStat(s2,st1,az1,lz1)
in  (st2,az2,lz2,code_s1^code_s2)
end
and
    compileProgram(program  s) =
let val (_,_,_,code) = compileStat(s,[],0,0)
in code
end;

Wenn wir das Beispielprogramm p übersetzen, so erhalten wir das nachfolgende Zielprogramm.

- compileProgram(p);
val it =
  nop ^nop ^
  (define 1 ^(load 0 ^loadConst 0 ^bop greater) ^jumpF 0 ^
   (load 0 ^loadConst 1 ^bop minus ^store 0 ^
    (load 2 ^loadConst 2 ^bop plus ^store 2)) ^goto 1 ^define 0) : ops ins

Tautologietest. In diesem Abschnitt schreiben wir ein Programm, welches aussagenlogische Formeln auf Tautologieeigenschaft testet. Hier zunächst die abstrakte Syntax von aussagenlogischen Ausdrücken mit Konjunktion, Disjunktion und Negation. Aussagenvariablen werden durch Zeichenreihen benannt.

datatype prop = Atom of string
  | Neg  of prop
  | Conj of prop * prop
  | Disj of prop * prop;

Hier eine Druckfunktion.

fun show (Atom a) = a
| show (Neg p) = "(~" ^(show p) ^")"
| show (Conj(p,q)) = "(" ^(show p) ^" & " ^(show q) ^")"
| show (Disj(p,q)) = "(" ^(show p) ^" | " ^(show q) ^")";

Der erste Schritt besteht darin, daß die Formeln in Negationsnormalform gebracht werden, wobei die Negationssymbole zu den Atomen geschoben werden. Grundlage hierfür sind im wesentlichen die De Morganschen Gesetze.

fun nnf (Atom a)   = Atom a
| nnf (Neg (Atom a))   = Neg (Atom a)
| nnf (Neg (Neg p))   = nnf p
| nnf (Neg (Conj(p,q))) = nnf(Disj(Neg p, Neg q))
| nnf (Neg (Disj(p,q))) = nnf(Conj(Neg p, Neg q))
| nnf (Conj(p,q))   = Conj(nnf p, nnf q)
| nnf (Disj(p,q))   = Disj(nnf p, nnf q);

Hier eine optimierte Variante, die durch zwei Funktionen für positive bzw. negierte Ausdrücke repräsentiert wird.

fun nnfpos (Atom a)   = Atom a
| nnfpos (Neg p)   = nnfneg p
| nnfpos (Conj(p,q))   = Conj(nnfpos p,nnfpos q)
| nnfpos (Disj(p,q))   = Disj(nnfpos p,nnfpos q)
and nnfneg (Atom a)   = Neg (Atom a)
| nnfneg (Neg p)   = nnfpos p
| nnfneg (Conj(p,q))   = Disj(nnfneg p,nnfneg q)
| nnfneg (Disj(p,q))   = Conj(nnfneg p,nnfneg q);

Ist eine Formel in Negationsnormalform, so muß nur noch das Distributivgesetz angewendet werden, um sie auf konjunktive Normalform zu bringen.

fun distrib (p, Conj(q,r)) = Conj(distrib(p,q), distrib(p,r))
| distrib (Conj(q,r), p) = Conj(distrib(q,p), distrib(r,p))
| distrib (p, q)    = Disj(p,q)  (*no conjunctions*);

so daß die konjunktive Normalform cnf (einer Formel in Negationsnormalform) nun wie folgt programmiert werden kann:

fun cnf (Conj(p,q)) = Conj (cnf p, cnf q)
| cnf (Disj(p,q)) = distrib (cnf p, cnf q)
| cnf p     = p (*a literal*)

Diese Hilfsfunktionen filtern die positiven bzw. negativen Literale aus einer konjunktiven Normalform heraus:

exception NonCNF;
fun positives (Atom a) = [a]
| positives (Neg(Atom _)) = []
| positives (Disj(p,q)) = positives p @ positives q
| positives  _= raise NonCNF;

fun negatives (Atom _) = []
  | negatives (Neg(Atom a)) = [a]
  | negatives (Disj(p,q)) = negatives p @ negatives q
  | negatives  _= raise NonCNF;

Wir brauchen noch eine Funktion inter, die den Durchschnitt zweier als Listen repräsentierter Mengen berechnet. Unsere Lösung verwendet Funktionen höherer Ordnung.

fun member nil _= false
  | member (y::l) x = if x=y then true else member l x;
fun filter _nil = nil
  | filter p (x::l) = if p x then (x::(filter p l)) else (filter p l);

fun inter l1 l2 = (filter (member l1) l2);

Schließlich ist eine Formel in konjunktiver Normalform genau dann eine Tautologie, wenn in jeder ihrer Klausel ein Atom sowohl positiv als auch negativ vorkommt.

fun taut (Conj(p,q)) = taut p andalso taut q
  | taut p      = ([] <> inter (positives p) (negatives p));