% -*- Coding: utf-8-*-
\documentclass[handout]{beamer}
\usetheme{Singapore}
\usepackage[utf8x]{inputenc}
\usepackage{german}
% \usepackage{graphicx}%\usepackage{epsf}
% ------------------------------------------------------------------

%% % ---- noweb/noweave zum Extrahieren von .tex und .sml-Dateien -----
%% \usepackage{noweb}
%% \nwcodetopsep = 3pt plus 1.2pt minus 1pt 
%% \def\nwendcode{\endtrivlist\endgroup\vskip-0.8ex}
%% \def\nwendquote{{}}
%% \def\Tt{\tt\fontencoding{OT1}\selectfont{}} % damit {\tt --->} funktioniert
%% % ------------------------------------------------------------------
\usepackage{url}

\parskip0.8ex

\title{Implementierung von Peirce-Algebren in SML \\ \large
  Seminar "`Relationale Grammatik"' \\ \large CIS, SS 2009}
\author{Hans Lei\ss}
\institute{Universit{\"a}t M{\"u}nchen 
\\ Centrum für Informations- und Sprachverarbeitung}

\begin{document} 
\maketitle

\def\setof#1#2{{\{#1\mid #2\}}}
\def\nat{{\mathbb N}}
\def\bool{{\mathbb B}}

\def\phi{{\varphi}}
\def\CA{{\cal A}}
\def\CB{{\cal B}}
\def\CD{{\cal D}}
\def\CP{{\cal P}}
\def\CR{{\cal R}}
\def\CO{{\cal O}}
\def\relpr{{\,;\,}}

\def\blue#1{\text{\color{blue}{#1}}}

\begin{frame}{SML - Standard ML}

\begin{itemize}
\item SML ist eine funktionale Programmiersprache
\item SML hat ein ausgefeiltes Modulsystem, mit dem man Algebren nahe an
  der mathematischen Syntax programmieren lassen

\item Wir verwenden das freie SML/NJ 

\item SML/NJ hat einen Parsergenerator ML-Yacc zur Entwicklung eigener
  (deterministischer) Programmiersprachen 
\item ML-GLR ist eine am CIS entstandene
  Variante von ML-Yacc, die lexikalische, syntaktische und semantische
  Ambiguit"aten erlaubt.

\item Semantische Annotationen der Syntaxregeln sind Funktionen.
\end{itemize}
\end{frame}

\begin{frame}{Quellen}

\begin{enumerate}
\item SML of New Jersey, ML-Lex, ML-Yacc: Bin"ar+Quelldateien 
\begin{itemize}
\item  {\tt http://www.smlnj.org}  (siehe Downloads)
\end{itemize}
\item User's Guide to ML-Lex and ML-Yacc: 
\begin{itemize}
\item \url{http://rogerprice.org} 
\end{itemize}
oder in den Quelldateien von SML:
\begin{itemize}
     \item {\tt smlnj/ml-lex/lexgen.tex} 
     \item {\tt smlnj/ml-yacc/doc/mlyacc.tex}
  \end{itemize}
\item ML-GLR: Quelldateien und Installationsanweisung 
\begin{itemize}
\item Subversion-Archiv (Rechte fehlen noch)
{\tt https:svn.cip.ifi.lmu.de/\~{}leiss/svn/hl-yacc}
\end{itemize}
\item User's Guide to ML-GLR: 
\begin{itemize}
\item Homepage des Seminars (.pdf)
\end{itemize}
\end{enumerate}
\end{frame}

\begin{frame}{Installieren von SML/NJ}

Unter {\tt www.smlnj.org}, Downloads, die neueste Version (110.71)
  holen:

\begin{itemize}
\item Unix/Linux: Unix
    The only file you need to download manually is {\color{blue}config.tgz}. Unpack,
    configure by editing config/targets, and install by running
    config/install.sh. The installer automatically downloads any additional
    files it might need. For more information, see INSTALL. 

\item Microsoft Windows: Download {\color{blue}smlnj.msi} and follow the instructions in
  WININSTALL. 
\end{itemize}
\end{frame}

\begin{frame}[fragile]{Das Wichtigste zu SML}

\begin{itemize}
\item SML Aufrufen 
\begin{verbatim}
> sml
Standard ML of New Jersey v110.67 [built: ... 2007]
-
\end{verbatim}
\item SML Beenden
\begin{verbatim}
- ^D
\end{verbatim}
\item Datei laden
\begin{verbatim}
- use "<Dateiname>";
\end{verbatim}
\item Compilation Manager (CM)
\begin{verbatim}
- CM.make "<Dateiname>.cm";   
\end{verbatim}
Das f"uhrt den "`Makefile"' {\tt <Dateiname>.cm} aus. (s.u.)
%\item Parsergenerator
%\item Parsen
\end{itemize}
\end{frame}

\begin{frame}[fragile]{Peirce-Algebra}

Eine Peirce-Algebra ist (offiziell) eine 2-sortige Struktur
\[ \CP = \langle \CB,\CR,:,{}^c\rangle, \]
wobei 
\begin{itemize}
\item $\CB = (B,+,0,\cdot,1,\bar{\ {}})$ eine Boole'sche Algebra,
\item $\CR = (R,+,0,\cdot,1,\bar{\ },\relpr,{}^{\breve{}},I)$ eine
  Relationenalgebra, 
\item "`$\cdot : \cdot$"' eine Abbildung ("`Urbild"') aus $R\times B \to B$ und 
\item "`$\cdot ^c$"' eine Abbildung ("`Rechtszylinder"') aus $B \to R$ ist, 
\end{itemize}
die gewissen Gleichungsaxiomen gen"ugen, z.B.
\begin{itemize}
\item $a\cdot (b+c) = (a\cdot c) + (b\cdot c)$ f"ur $a,b,c\in B$,
\item $(r\relpr s)^{\breve{}} = (s^{\breve{}}\relpr r^{\breve{}})$ f"ur
  $r,s\in R$,
\item $(r:1)^c = (r \relpr 1)$ f"ur alle $r\in R$.
\end{itemize}
\end{frame}


\begin{frame}[fragile]{Die Signatur einer Peirce-Algebra}

Die \emph{Signatur} einer mathematischen Struktur ist die Angabe der
Funktionen und Relationen mit ihren Stelligkeiten.

Die Signatur der Boole'schen Algebra ist 
\[ \langle +^{(2)},0^{(0)},\cdot^{(2)},1^{(0)},\bar{\ {}}^{(1)}\rangle \]

Bei einer Struktur mit mehreren Objektsorten oder -Typen mu"s man
auch die Typen angeben. 

Die Signatur einer Peirce-Algebra ist also:
\[ \langle\sigma,\rho;\ +^{\sigma\times\sigma\to\sigma},0^\sigma,\ldots,
+^{\rho\times\rho\to\rho},0^\rho,\ldots,
\relpr^{\rho\times\rho\to\rho},
:\,^{\rho\times \sigma\to\sigma}, {^{_c}\,}^{\sigma\to\rho}\rangle\]
wobei $\sigma$ der Typ der "`Mengen"' und $\rho$ der Typ der "`Relationen"' ist.
\end{frame}


\begin{frame}{Die Peirce-Algebra $\CP(U)$}

Die Standardinterpretation der Peirce-Algebra bilden die Teilmengen und
zweistelligen Relationen "uber einem Universum $U$:

\[ \CP(U) = \langle \CB(U), \CR(U), :, {}^c\rangle \] 
wobei
\begin{itemize}
\item $\CB(U) = (2^U,\cup,\emptyset,\cap,U,\overline{\cdot})$ die
  Boole'sche Algebra aller Teilmengen von $U$ ist, mit $\overline A :=
  U\setminus A$,
\item $\CR(U) = (2^{U\times U},\cup,\emptyset,\cap,U\times
  U,\overline{\cdot},\relpr,{}^{\breve{}},I)$ die Relationenalgebra aller
  2-stelligen Relationen "uber $U$ ist, $I = \setof{(u,u)}{u\in U}$,
\item $R:A := \setof{u\in U}{\exists a\in A\ R(u,a)}$ das "`Urbild der Menge
  $A$ unter der Relation $R$"', und
\item $A^c := A\times U$ der "`Rechtszylinder der Menge $A$"' ist.
\end{itemize}
\end{frame}


\begin{frame}[fragile]{Ein paar zus{\"a}tzliche Grundoperationen }

In einer "`Relationalen Grammatik"' sind als Bedeutungen von
Ausdr"ucken nur Objekte einer Peirce-Algebra $\CP(U)$ erlaubt.
%, also nur Mengen oder Relationen "uber dem Universum $U$.

Als Wahrheitswerte von Aussagen nimmt B"ottner $U$ f"ur
"`wahr"' und $\emptyset$ f"ur "`falsch"'; er braucht zus"atzlich drei
Testfunktionen: 
\begin{eqnarray*}
    U(A) &:=& \begin{cases} U & \hbox{falls $A=U$} 
              \\ \emptyset & sonst \end{cases}
 \\ E(A) &:=& \begin{cases} U & \hbox{falls $A\not=\emptyset$} 
              \\ \emptyset & sonst \end{cases}
 \\ N(A) &:=& \begin{cases} U & \hbox{falls $A=\emptyset$} 
              \\ \emptyset & sonst \end{cases}
\end{eqnarray*}

Stattdessen erweitern wir die Peirce-Algebra um die Boole'sche Algebra
$\bool$ der Wahrheitswerte und Abbildungen $U,E,N:\sigma\to \bool$:
\[ \CP(U) = \langle \CB(U), \CR(U), \bool, :, {}^c, U, E, N\rangle \] 
\end{frame}

\begin{frame}[fragile]{Signaturen in SML}

In SML kann man Module mit der in der Mathematik "ublichen Terminologie
definieren.

\begin{verbatim}
signature PEIRCE = 
  sig 
      type set   (* Mengenbereich B     *)
      type rel   (* Relationenbereich R *)
      type tv    (* Wahrheitswerte IB   *)

      val <Konstante> : <Typ>
      ...
      val <Operation> : <Argumenttyp> -> <Ergebnistyp>
      ...
      val <Operation> : <Argumenttyp> * <Argumenttyp> 
                          -> <Ergebnistyp>
  end
\end{verbatim}

\end{frame}

\begin{frame}[fragile]{Strukturen in SML}

Wenn man dazu passende Strukturen definieren will, muss man die Definition
der Typen und Werte angeben:

\begin{verbatim}
structure Peirce : PEIRCE = 
  struct
      type set = ...  (* Mengenimplementierung *)
      type rel = ...  (* Relationenimplementierung *)
      type tv  = ...  (* Wahrheitswertimplementierung *)

      val <Konstante> = <Angabe des Elements>
      ...
      val <Operation> = <Angabe der Funktion>
      ...
  end
\end{verbatim}
\end{frame}

\end{document} ---------- fuer den Rest braucht man das noweb-Programm ---------


\begin{frame}[fragile]{Die Signatur {\tt PEIRCE}}
<<PA-GLR/peirce.sig>>=
signature PEIRCE =
   sig  
       type set
  
       val ConS : string -> set  (* Konstante *)
       val UnitS : set
       val ZeroS : set
       val SumS  : set * set -> set
       val ProdS : set * set -> set
       val CompS : set -> set

@ %
\end{frame}

\begin{frame}[fragile]{}
<<PA-GLR/peirce.sig>>=
       type rel 
       
       val ConR : string -> rel (* Konstante *)
       val UnitR : rel
       val ZeroR : rel
       val SumR  : rel * rel -> rel
       val ProdR : rel * rel -> rel
       val CompR : rel -> rel

       val I     : rel
       val Conv  : rel -> rel
       val Prod  : rel * rel -> rel
       val Minor : rel -> rel   (* spaeter *)
       val Tc    : rel -> rel   (* spaeter *)
 
       val PreIm : rel * set -> set
       val Cylin : set -> rel
@ %
\end{frame}

\begin{frame}[fragile]{}
<<PA-GLR/peirce.sig>>=
        type tv 

        val And : tv * tv -> tv                                 
        val Or  : tv * tv -> tv                                 
        val Neg : tv -> tv                                 

        val E : set -> tv
        val U : set -> tv
	val N : set -> tv

        val ER : rel -> tv
        val UR : rel -> tv
        val NR : rel -> tv
   end

@ %
\end{frame}

\begin{frame}[fragile]{Alternative Signatur PEIRCE}

die Mengen- und Relationenalgebra als Komponenten vorsieht:

\begin{verbatim}
signature BOOLEAN_ALGEBRA =
   sig type t 
       val Zero : t
       val Unit : t
       val Sum  : t * t -> t
       val Prod : t * t -> t
       val Comp : t -> t
   end
signature RELATION_ALGEBRA = sig type t  ... end
signature PEIRCE = 
   sig structure Set : BOOLEAN_ALGEBRA
       structure Rel : RELATION_ALGEBRA
       val PreIm : Rel.t * Set.t -> Set.t
       val Cylin : Set.t -> Rel.t
   end
\end{verbatim}
\end{frame}

\begin{frame}[fragile]{Konstruktion der Peirce-Algebra $\CP(U)$}
\bigskip

Wir wollen keine \emph{bestimmte} Algebra {\tt P:PEIRCE}
implementieren, sondern eine \emph{Konstruktion} $\CP$, die zu gegebenem
Universum $U$ die volle Peirce'sche Algebra $\CP(U)$ liefert.

Ein Universum ist eine Grundmenge $U$ mit benannten Mengen
$A\subseteq $ und Relationen $R\subseteq U$ - den Bedeutungen von Nomina,
Verben, Adjektiven in einer Anwendung:

<<PA-GLR/peirce.sml>>=
signature UNIVERSE = 
   sig
       eqtype element  (* Typ mit Gleichheitstest = *)
       val elements : element list      (* endlich! *)
       val ConS : string -> element list
       val ConR : string -> (element * element) list
       exception NoValue (* wo ConR,ConS undefiniert *)
   end
@ %
\end{frame}

\begin{frame}[fragile]{Beispieluniversum}

<<PA-GLR/pg1.sml>>=
structure Personen : UNIVERSE = 
  struct
    datatype element = a | b | c | d | e | f | g | h | m
    val elements = [a,b,c,d,e,f,g,h,m]
    exception NoValue                    (* Synt.Kat. *)
    fun ConS "Anna"      = [a]                  (* EN *)
      | ConS "Emil"      = [e]                  (* CN *)
      | ConS "Frau"      = [a,g,m]
      | ConS "arbeiten"  = [a,e]                (* IV *)
      | ConS "gesund"    = [a]                  (* CA *)
      | ConS _           = raise NoValue
    fun ConR "lieben"    = [(b,d),(a,a),(e,a)]  (* TV *)
      | ConR "Nachbar"   = [(d,e),(e,a)]        (* RN *)
      | ConR "älter"     = [(d,a),(d,e),(a,e)]  (* IA *)
      | ConR _           = raise NoValue)
  end
@ %
\end{frame}


\begin{frame}[fragile]{Mengenimplementierung Set:SET}

<<PA-GLR/set.sml>>=
signature SET = sig  
    type 'a set (* 'a El.Typ, ''a mit Gleichheit *)
    val empty : 'a set
    val difference : ''a set -> ''a set -> ''a set
    val equal : ''a set -> ''a set -> bool
    val intersection : ''a set -> ''a set -> ''a set
    val list : 'a set -> 'a list
    val map : ('a -> ''b) -> 'a set -> ''b set
    val member : ''a -> ''a set -> bool
    val mk : ''a list -> ''a set
    val select : 'a set -> ('a -> bool) -> 'a set
    val size : 'a set -> int
    val subset : ''a set -> ''a set -> bool
    val union : ''a set -> ''a set -> ''a set
    val Union : ''a set list -> ''a set
  end
@ %
\end{frame}

\begin{frame}[fragile]{Mengenimplementierung Set : SET}

Endliche Mengen seien Listen von Objekten, die keine
Duplikate enthalten und deren Anordnung nicht benutzt werden kann:

<<PA-GLR/set.sml>>=
structure Set : SET = struct
     datatype 'a set = Set of 'a list
     val empty = Set []
     fun difference (Set S) (Set T) =
         let fun diff set [] = set  
               | diff set (e::E) = diff (drop e set) E
         in Set (diff (Set S) T) end
     and drop e (Set S) = ...
     ...
     fun list (Set S) = S
     fun map f (Set S) = mk (List.map f S)
     fun size (Set S) = List.length S
     ...
  end
@ %
\end{frame}

\begin{frame}[fragile]{Die Signatur PEIRCEfull}

In einer vollen Peirce-Algebra $\CP(U)$ sind $\CB(U)$ und $\CR(U)$ aus
demselben $U$ aufgebaut.

Wir erweitern die Signatur PEIRCE um den Typ der Individuen $U$: 
<<PA-GLR/peirce.sml>>=
signature PEIRCEfull = 
   sig 
       include PEIRCE
       type element 
   end                     
@ %
\bigskip

Wir wollten aber keine feste Peirce'sche Algebra {\tt P:PEIRCEfull}
implementieren, sondern die $\CP(U)$ f"ur beliebige Beispielmodelle $U$.
\end{frame}

\begin{frame}[fragile]{Abh"angige Strukturen: Funktoren in SML}

Die volle Peirce-Algebra $\CP(U)$ "uber $U$ \emph{h"angt} vom Universum $U$
\emph{ab}.

In SML dr"uckt man die Abh"angigkeit einer Struktur $B$ von einer anderen
Struktur $A$ durch einen {\color{blue}Funktor} $F:SIG_A \to SIG_B$ aus:

\begin{verbatim}
functor F(X:SIGA) = 
  struct ... X.f ... end : SIGB

structure B = F(A)
\end{verbatim}

Die Konstruktion $\CP$, die aus $U$ ein $\CP(U)$ bildet, soll als SML- Funktor {\tt Peirce} implementiert werden, der aus
einer Struktur $U:UNIVERSE$ eine Struktur $P(U):PEIRCEfull$ macht:

\begin{verbatim}    
functor Peirce(U : UNIVERSE) : PEIRCEfull = 
  struct ... end
\end{verbatim}

\end{frame}

\begin{frame}[fragile]{Der Funktor Peirce : UNIVERSE $\to$ PEIRCEfull}

<<PA-GLR/peirce.sml>>=
functor Peirce(U : UNIVERSE) : PEIRCEfull = 
   struct
     type element = U.element
     fun ConS s = Set.mk (U.ConS s)
     fun ConR s = Set.mk (U.ConR s)

     type set = element Set.set     (* BA(U) *)

     val UnitS = Set.mk U.elements
     val ZeroS = Set.empty
     fun SumS(A,B) = Set.union A B
     fun ProdS(A,B) = Set.intersection A B
     fun CompS(A) = Set.difference UnitS A

@ %
\end{frame}

\begin{frame}[fragile]{}
<<PA-GLR/peirce.sml>>=
     type rel = (element * element) Set.set  (* RA(U) *)

     fun Id(A) = Set.map (fn x => (x,x)) A
     val I = Id(UnitS)
     fun Cart(A,B) = 
         let fun f x = 
                 List.map (fn y => (x,y)) (Set.list B)
         in  Set.mk (List.foldr (op @) nil 
                                (List.map f (Set.list A)))
         end
     val UnitR:rel = Cart(UnitS,UnitS)
     val ZeroR = Set.empty
     fun SumR(R,S) = Set.union R S
     fun ProdR(R,S) = Set.intersection R S
     fun CompR(R) = Set.difference UnitR R
     fun Conv(R) = Set.map (fn (x,y) => (y,x)) R

@ %
\end{frame}

\begin{frame}[fragile]{}
<<PA-GLR/peirce.sml>>=
     fun Prod(R,S) =            (* Relationenprodukt *)
         let fun f(a,b) = 
             Set.map (fn (x,c) => (a,c)) 
                     (Set.select S (fn (x,c) => x = b))
         in  Set.Union (List.map f (Set.list R))
         end
     fun Tc(R) =                (* Transitive Huelle *)
         let val T = SumR(Prod(R,R),R) 
         in
             if Set.size(T) = Set.size(R) then R 
             else Tc(T)  (* terminiert bei U endlich *)
         end

     fun PreIm(R,B) =                       (* R : B *)
         Set.map #1 (Set.select R 
                          (fn (a,b) => Set.member b B))
     fun Cylin(A) = Cart(A,UnitS)             (* A^c *)
@ %
\end{frame}

\begin{frame}[fragile]{}
<<PA-GLE/peirce.sml>>=
     datatype tv = datatype bool

     fun And(A,B) = A andalso B    (* von SML's bool *)
     fun Or(A,B)  = A orelse B
     fun Neg(A)   = not A

     fun E(A) = (Set.size A > 0)
     fun N(A) = (Set.size A = 0)
     fun U(A) = ((Set.size A) = (Set.size UnitS))

     fun ER(A) = (Set.size A > 0)
     fun UR(A) = ((Set.size A) = (Set.size UnitR))
     fun NR(A) = (Set.size A = 0)
   end 
@ %
\end{frame}

\begin{frame}[fragile]{Anwendung auf das Beispieluniversum}

\begin{verbatim}
> cd PA-GLR
> sml
Standard ML of New Jersey v110.67 [built: Nov 26 2007]
- use "set.sml";
- use "peirce.sig"; use "peirce.sml";
- use "pg1.sml";
[opening pg1.sml]
structure PersonenU :
  sig
    datatype element = a | b | c | d | e | f | g | h | m
    val elements : element list
    exception NoValue
    val ConS : string -> element list
    val ConR : string -> (element * element) list
  end
- structure Personen = Peirce(PersonenU);
structure Personen : PEIRCEfull
\end{verbatim}
\end{frame}

\begin{frame}[fragile]{}

\begin{verbatim}
- PersonenU.ConR "Nachbar";
val it = [(d,e),(e,a)] : (PersonenU.element *
                          PersonenU.element) list
- Personen.ConR "Nachbar";
val it = Set [(d,e),(e,a)] : Personen.rel
- Personen.Tc it;  
val it = Set [(d,e),(e,a),(d,a)] : Personen.rel

- open Personen;
opening Personen
  type set = Personen.element Set.set
  val ConS : string -> set
  val UnitS : set
  val ZeroS : set
  val SumS : set * set -> set
  val ProdS : set * set -> set
  val CompS : set -> set

\end{verbatim}
\end{frame}

\begin{frame}[fragile]{}

\begin{verbatim}
  type rel = (Personen.element * Personen.element) Set.set
  val ConR : string -> rel
  val UnitR : rel
  val ZeroR : rel
  val SumR : rel * rel -> rel
  val ProdR : rel * rel -> rel
  val CompR : rel -> rel
  val I : rel
  val Conv : rel -> rel
  val Prod : rel * rel -> rel
  val Minor : rel -> rel
  val Tc : rel -> rel

  val PreIm : rel * set -> set
  val Cylin : set -> rel

\end{verbatim}
\end{frame}

\begin{frame}[fragile]{}
\begin{verbatim}
  datatype bool = false | true       (* = tv ! *)
  val And : tv * tv -> tv
  val Or : tv * tv -> tv
  val Neg : tv -> tv
  val E : set -> tv
  val U : set -> tv
  val N : set -> tv
  val ER : rel -> tv
  val UR : rel -> tv
  val NR : rel -> tv

  type element = PersonenU.element
\end{verbatim}

Nach dem "Offnen der Struktur entf"allt das Pr"afix {\tt Personen.}: 
\begin{verbatim}
- ConR "Nachbar";
val it = Set [(d,e),(e,a)] : rel
- true : Personen.tv;
val it = true : bool
\end{verbatim}
\end{frame}

\begin{frame}[fragile]{Fazit}

\begin{itemize}
\item In SML kann man abstrakte Strukturen gut implementieren:
\begin{verbatim}
structure A = struct 
  type t = ...               (* Objektbereich       *)
  val c : t = ...            (* Objekt              *)
  fun f (x:t, y:t) : t = ... (* Funktion f:t*t -> t *)
  structure B = ...          (* Unterstruktur       *)
end : SIGNATURE
\end{verbatim}

\item Funktoren konstruieren Strukturen aus anderen Strukturen:
%% \begin{verbatim}
%% functor F(X:SIG1) : SIG2 = struct ...X.f... end
%% \end{verbatim}

 {\tt functor Peirce(U:UNIVERSE)} konstruiert $\CP(U)$ aus $U$
\end{itemize}{\color{blue}Demn"achst:}
\begin{itemize}
\item Ziel 1: Parsergenerator, der aus einer Grammatik einen Parser
  erzeugt, der Peirce-Terme zur"uckgibt

\item Ziel 2: Funktor {\tt Semantik(A:PEIRCEfull)}, der Peirce-Terme in der
  Algebra $A$ auswertet
\end{itemize}
\end{frame}

\begin{frame}[fragile]{Compilation Manager: {\tt CM.make}}
SML hat ein eingebautes "`make"': im Unterschied zu dem von Unix sagt man im
"`Makefile"' nicht, welche Schritte ausgef"uhrt werden sollen, sondern welche Strukturen
gebaut werden sollen.

<<PA-GLR/personen.cm>>=
Group 
 signature PEIRCEfull   
 structure Personen
is 
 $/basis.cm   (* fuer structure List *)
 set.sml
 peirce.sig
 peirce.sml
 pg1.sml

@ %
\end{frame}


\begin{frame}[fragile]{Algebra der Peirce-Terme}

In der Term-Algebra werden die Funktionen der Signatur [[PEIRCE]] durch
Konstruktionsschritte beim Termaufbau "`interpretiert"':

<<PA-GLR/peirce.sml>>=
structure PeirceTerm =
   struct
       datatype set = ConS of string 
                     | SumS of set * set
                     | ZeroS
                     | ProdS of set * set
                     | UnitS 
                     | CompS of set
                     | PreIm of rel * set   (* R : B *)

@ %

Hierdurch werden Funkionen wie {\tt ConS : string -> set} oder {\tt UnitS :
  set} eingef"uhrt.

\end{frame}

\begin{frame}[fragile]{}
<<PA-GLR/peirce.sml>>=
       and      rel = ConR of string
                     | SumR of rel * rel
                     | ZeroR
                     | ProdR of rel * rel
                     | UnitR
                     | CompR of rel
                     | Id of set
                     | Minor of rel
                     | Tc of rel
                     | Prod of rel * rel
                     | Conv of rel
                     | Cylin of set
       and      tv  =  And of tv * tv
                     | Or  of tv * tv
                     | Neg of tv
                     | ...
    val I = Id UnitS
@ %
\end{frame}

\begin{frame}[fragile]{}
<<PA-GLR/peirce.sml>>=
    fun StoString ZeroS       = "0" 
      | StoString UnitS       = "1" 
      | StoString (ConS(w))   = w
      | StoString (SumS(A,B)) = 
        "(" ^ (StoString A) ^ " + " ^ (StoString B) ^ ")"
      | StoString (ProdS(A,B)) = 
        "(" ^ (StoString A) ^ " . " ^ (StoString B) ^ ")"
      | StoString (CompS(A))   = "-" ^ (StoString A) 
      | StoString (PreIm(R,A)) = 
        "(" ^ (RtoString R) ^ " : " ^ (StoString A) ^ ")"
    and RtoString (ConR(r))    = r
      | RtoString UnitR        = " 1' " 
      | RtoString ZeroR        = " 0' " 
      | RtoString (SumR(R,S))  = 
        "(" ^ (RtoString R) ^ " + " ^ (RtoString S) ^ ")"
      | RtoString (ProdR(Cylin A,Conv(Cylin B))) = 
        "(" ^ (StoString A) ^ " x " ^ (StoString B) ^ ")"                   
      | RtoString (ProdR(R,S)) = 
        "(" ^ (RtoString R) ^ " . " ^ (RtoString S) ^ ")"
      | RtoString (CompR(R))   = "-" ^ (RtoString R) 
      | RtoString (Minor(R))   = "minor" ^ (RtoString R)
      | RtoString (Tc(R))      = "tc(" ^ (RtoString R) ^ ")"
      | RtoString (Id(A))      = "Id(" ^ (StoString A) ^ ")"
      | RtoString (Prod(R,S))  = 
        "(" ^ (RtoString R) ^ " ; " ^ (RtoString S) ^ ")"
      | RtoString (Conv(R))    = "~" ^ (RtoString R) 
      | RtoString (Cylin(A))   = "("^(StoString A) ^ " x 1)" 
    and TtoString (E A) = "0 < " ^ (StoString A) 
      | TtoString (U A) = "1 = " ^ (StoString A) 
      | TtoString (N A) = "0 = " ^ (StoString A) 
      | TtoString (ER A) = "0' < " ^ (RtoString A) 
      | TtoString (UR A) = "1' = " ^ (RtoString A) 
      | TtoString (NR A) = "0' = " ^ (RtoString A) 
      | TtoString (Neg A) = "-(" ^ (TtoString A) ^ ")"
      | TtoString (And(A,B)) = "(" ^ (TtoString A) ^ " /\\ " 
                                ^ (TtoString B) ^ ")" 
      | TtoString (Or(A,B)) = "(" ^ (TtoString A) ^ " \\/ " 
                                       ^ (TtoString B) ^ ")" 
   end

@ Die Funktionen [[StoString: set -> string]], 
[[RtoString: rel -> string]] und [[TtoString: tv -> string]] sind
eingef"ugt, um die Peirce-Ausdr"ucke lesbar an\-zei\-gen zu k"onnen.
\end{frame}

\end{document}