home Funktionale Programmierung: Transformation aussagenlogischer Ausdrücke Prof. Dr. Uwe Schmidt FH Wedel
Alte Übungen
Ein- und AusgabeInhaltsverzeichnisAbleitung von regulären Ausdrücken

Transformation aussagenlogischer Ausdrücke

weiter
weiter

Aufgabe

Aussagenlogische Ausdrücke mit Rhododendron-Bäumen
als Trainingslager für die Verarbeitung und Transformation von Bäumen.
Rhododendron-Bäume können genutzt werden zur Darstellung von aussagenlogischen Ausdrücken, wenn man für den Knotentyp einen Datentyp definiert, der die logischen Operatoren, die Konstanten für wahr und falsch und für Variablen repräsentiert.
 
Die hier verwendeten Datentypen seien wie folgt definiert:
weiter
module DataTypes
where
 
import Prelude hiding (and, or)
 
data RoseTree a
    = RT a [RoseTree a]
    deriving (Eq, Ord, Show, Read)
 
data BoolOp
    = F
    | T
    | V Name
    | NOT
    | AND
    | OR
    | IMPL
    | EQUIV
    | XOR
    | NAND
    | NOR
    deriving (Eq, Ord)
 
instance Show BoolOp
    where
    show = showOp
 
type BoolExpr = RoseTree BoolOp
 
type Name = String
 
type Env = [(Name, Bool)]
 
type Names = [Name]
 
-- ------------------------------
 
-- useful rosetree visitors
 
foldRT  :: (a -> [b] -> b) -> RoseTree a -> b
foldRT f (RT op al)
    = f op (map (foldRT f) al)
 
 
mapRT   :: (a -> b) -> (RoseTree a -> RoseTree b)
mapRT f (RT e al)
    = RT (f e) (map (mapRT f) al)
 
-- ------------------------------
 
-- consistency
 
invBoolEx :: BoolExpr -> Bool
invBoolEx (RT op al)
    | op `elem` [F, T]
        = null al
invBoolEx (RT (V _) al)
    = null al
invBoolEx (RT NOT al)
    = length al == 1
invBoolEx (RT IMPL al)
    = length al == 2
invBoolEx (RT op al)
    | op `elem` [AND, OR, EQUIV, XOR, NAND, NOR]
        = length al >= 2
 
-- ------------------------------
 
opr     :: BoolExpr -> BoolOp
opr (RT op _) = op
 
args    :: BoolExpr -> [BoolExpr]
args (RT _ al) = al
 
-- ------------------------------
 
-- constants
 
true    :: BoolExpr
true
    = RT T []
 
false   :: BoolExpr
false
    = RT F []
 
var     :: Name -> BoolExpr
var n
    = RT (V n) []
 
-- ------------------------------
 
-- smart constructor function
 
boolEx  :: BoolOp -> [BoolExpr] -> BoolExpr
boolEx op []
    | op `elem` [AND, EQUIV, NOR]
        = true
    | op `elem` [OR, XOR, NAND]
        = false
 
boolEx op [e1]
    | op `elem` [AND, OR, EQUIV]
        = e1
    | op `elem` [XOR, NAND, NOR]
        = boolEx NOT [e1]
 
boolEx op al
    | op `elem` [F,T]
      &&
      not (null al)
        = error ( "boolEx: Illegal constant expression "
                  ++ show (RT op al)
                )
boolEx (V n) al
    | not (null al)
        = error ( "boolEx: Illegal variable expression "
                  ++ show (RT (V n) al)
                )
boolEx NOT al
    | length al /= 1
        = error ( "boolEx: Illegal NOT expression "
                  ++ show (RT NOT al)
                )
boolEx IMPL al
    | length al /= 2
        = error ( "boolEx: Illegal IMPL expression "
                  ++ show (RT IMPL al)
                )
 
boolEx op al
    = RT op al
 
 
-- some useful unary and binary constructors
 
neg     :: BoolExpr -> BoolExpr
neg e
    = boolEx NOT [e]
 
impl    :: BoolExpr -> BoolExpr -> BoolExpr
a `impl` b
    = boolEx IMPL [a, b]
 
and     :: BoolExpr -> BoolExpr -> BoolExpr
a `and` b
    = boolEx AND [a, b]
 
or      :: BoolExpr -> BoolExpr -> BoolExpr
a `or` b
    = boolEx OR [a, b]
 
equiv   :: BoolExpr -> BoolExpr -> BoolExpr
a `equiv` b
    = boolEx EQUIV [a, b]
 
xor     :: BoolExpr -> BoolExpr -> BoolExpr
a `xor` b
    = boolEx XOR [a, b]
 
nand    :: BoolExpr -> BoolExpr -> BoolExpr
a `nand` b
    = boolEx NAND [a, b]
 
nor     :: BoolExpr -> BoolExpr -> BoolExpr
a `nor` b
    = boolEx NOR [a, b]
 
-- ------------------------------
 
-- show functions
 
prio :: BoolOp -> Int
prio NOT   = 1
prio AND   = 3
prio NAND  = 3
prio OR    = 3
prio XOR   = 3
prio NOR   = 3
prio IMPL  = 4
prio EQUIV = 5
prio _     = 0
 
showOp F        = "false"
showOp T        = "true"
showOp (V n)    = n
showOp NOT      = "not"
showOp AND      = "and"
showOp OR       = "or"
showOp IMPL     = "=>"
showOp EQUIV    = "<=>"
showOp XOR      = "xor"
showOp NAND     = "nand"
showOp NOR      = "nor"
 
-- ------------------------------
 
showEx :: BoolExpr -> String
showEx = showEx' 10
 
showEx' :: Int -> BoolExpr -> String
showEx' p (RT op al)
    | p <= pop
        = "(" ++ str ++ ")"
    | otherwise
        = str
    where
    pop = prio op
 
    str = show' op al
 
    show' op al
        | op `elem` [AND,OR,IMPL,EQUIV,XOR,NAND,NOR]
            = foldl1 (\ x y -> x ++ " " ++ show op ++ " " ++ y)
              .
              map (showEx' pop) $ al
        | op == NOT
            = show op ++ " " ++ showEx' pop (head al)
        | otherwise
            = show op
 
-- ------------------------------
weiter
Als logische Operatoren sind in diesem Beispiel AND, OR, NOT, Implikation Äquivalenz, Exklusives ODER und die in der Hardware gerne benutzten NAND und NOR möglich. Neben den Operatoren gibt es die Konstanten T(rue) und F(alse) und ein Blatt für Variablen. Für diese drei Werte sollte die Liste der Nachfolger sinnvollerweise leer sein, wie es in den Definitionen für die erzeugenden Funktionen für true, false und Variablen zu sehen ist.
Für die Operatoren gelten zum Teil ebenfalls Einschränkungen an die Struktur der Kindlisten: NOT hat sinnvollerweise genau einen Nachfolger, die Implikation genau zwei. Die anderen Operatoren können als beliebigstellig aufgefaßt werden, zum Beispiel x AND y AND z durch einen AND-Knoten mit drei Nachflogern dargestellt werden. Da der Gebrauch als binären Operatoren die häufigste praktische Anwendung ist, sind hier für diese zweistelligen Ausdrücke erzeugende Funktionen definiert.
Entwickeln Sie folgende Funktionen zur einfachen Verarbeitung von logischen Ausdrücken.
module BoolExpr1
where
 
import DataTypes
 
-- ------------------------------
 
foldRT  :: ??? -> RoseTree a -> b
foldRT ??? e
    = undefined
 
-- ------------------------------
 
eval    :: Env -> BoolExpr -> Bool
eval env e
    = undefined
 
proofByEnumeration      :: BoolExpr -> Bool
proofByEnumeration e
    = undefined
 
partialEval     :: BoolExpr -> BoolExpr
partialEval e
    = undefined
 
processBottomUp :: (BoolExpr -> BoolExpr) -> BoolExpr -> BoolExpr
processBottomUp f e
    = undefined
 
-- ------------------------------
weiter
foldRT
Mit foldRT soll ein Rosetree zusammengefaltet werden können. Diese Funktion kann zum Teil in den folgenden Funktionen verwendet werden
eval
dient zur Auswertung von aussagenlogischen Formeln. Hierfür ist eine Variablenbelegung, eine Umgebung (Env), notwendig. eval kann als ein Beispiel für eine fold-Funktion gesehen werden
proofByEnumeration
Die primitivste Form des Beweises ist die vollständige Aufzählung. Mit eval ist diese sehr leicht zu realisieren: Man sammelt sich alle Variablen in einem Ausdruck auf (fold), generiert alle möglichen Belegungen (Wahrheitstabelle) und wertet für alle diese Belegungen den Ausdruck aus. Für einen Satz muss immer True das Resultat sein.
 
Testen Sie diese Beweisstrategie mit einigen aussagelogischen Sätzen, zum Beispiel modus ponens, de Morgan, oder Distributivgesetz.
partialEval
Die Konstanten true und false können in Teilausdrücken vollständig eliminiert werden. Es sind also Ausdrücke wie (x `and` true), (x `and` false), (x `equiv` true) und andere zu vereinfachen. partialEval soll genau diese Aufgabe übernehmen. Beachten Sie bitte, dass hierbei "degenerierte" Ausdrücke entstehen können, z.B (RT AND [x]) aus (x `and` true) oder (RT AND []) aus (true `and` true). Diese sollten hier auch partiell ausgewertet werden.
Tipp
Diese degenerierten Ausdrücke kann man auf einfache Weise vermeiden, wenn man sogenannte intelligente Konstruktoren baut (smart constructor functions), anstatt explizit z.B (RT AND al). Diese smarten Funktionen erzeugen dann gar nicht erst die komplizierten Funktionen, sondern gleich die einfache Form.
processBottomUp
ist eine Hilfsfuktion, die einen Ausdruck transformiert, indem sie mit den Blättern beginnend, auf jeden Teilausdruck eine Transformation anwendet. Mit dieser Funktion kann man das partielle Auswerten geeignet modularisieren, indem man eine Transformation entwickelt, die nur versucht, den Ausdruck an der Wurzel zu vereinfachen. Diese Transformation kann dann mit den Blättern beginnend auf alle Operatoren in einem Ausdruck angewendet werden.
Vereinfachung
und Transformation von Booleschen Ausdrücken.
 
Wenn alle Gesetze der Booleschen Algebra wiederholt angewendet werden, kann man einen Ausdruck vereinfachen und in eine Normalform bringen, einen Satz sogar in den Ausdruck true transformieren.
 
Ein vollständiger Formeltransformator für die Berechnung einer Normalform benötigt alle Gesetze. Hier sollen nur die Transformationen für die Elimination aller Operatoren außer AND, OR und NOT umgesetzt werden, die Verschiebung der Negation an die Variablen mit de Morgan und die Assoziativgesetze. Sind diese Transformationen für einen Knoten realisiert, kann man eine Vereinfachungsstrategie implementieren, indem man die Funktionen mit processTopDown und processBottomUp geschickt hintereinander auf ganze Bäume ausführt.
module BoolExprStep2
where
 
import DataTypes
import BoolExprStep1
 
-- ------------------------------
 
-- substitute all operators by AND, OR and NOT
 
transf2AndOrNot :: BoolExpr -> BoolExpr
transf2AndOrNot e
    = undefined
 
-- use de Morgan to move negation inside
 
moveNegationInside      :: BoolExpr -> BoolExpr
moveNegationInside e
    = undefined
 
-- use assoc for AND, OR, EQUIV and XOR
 
assocLaw        :: BoolExpr -> BoolExpr
assocLaw e
    = undefined
 
-- simplify expression by (repeated) application
-- of partial eval and the above functions to a whole
-- expression.
-- processTopDown and processBottomUp are useful in
-- context
 
simplifyExpr    :: BoolExpr -> BoolExpr
simplifyExpr e
    = undefined
 
-- ------------------------------
Parser
für Aussagen logische Ausdrücke.
 
Zur bequemen textbasierten Eingabe von Ausdrücken wird ein Parser benötigt, der die von showEx verwendete Syntax analysiert und den zugehörigen Baum aufbaut.
ist eine Parser Bibliothek für die einfache Konstruktion von top-down Parsern. Die Bibliothek steht sowohl für Hugs als auch für GHC zur Verfügung. Im Parsec Users Guide sind einfache Beispiele für die Konstruktion von Parsern anschaulich beschrieben. Insbesondere die Kapitel über Expression Parsing und Lexical Analysis sind hier brauchbar
 
Definieren Sie eine kontextfreie Grammatik für die verwendete Notation und leiten daraus einen Parser folgenden Typs ab:
module BoolExprParser
where
 
import DataTypes
 
import Text.ParserCombinators.Parsec
 
-- ------------------------------
 
readEx  :: String -> BoolExpr
readEx
    = either
      (\ e -> error $ show e)
      id
      .
      parse boolExprParser ""
 
boolExprParser  :: Parser BoolExpr
boolExprParser
    = undefined
 
-- ------------------------------
weiter
weiter

Vorgefertigte Module

die Datentypen
die Funktionen zum Auswerten und partiellen Auswerten
die Schnittstellen der Transformationsfunktionen
einige Beispiele
SeitenanfangAlte Übungen
Ein- und AusgabeInhaltsverzeichnisAbleitung von regulären Ausdrücken
Letzte Änderung: 27.03.2015
© Prof. Dr. Uwe Schmidt
Prof. Dr. Uwe Schmidt FH Wedel