\begin{slide}{Highscore: Reguläre Ausdrücke}

$ \left\{
w\mid
\forall p,r:
\left(\begin{array}{ll}
 &  (p<r \wedge w[p]=a \wedge  w[r]=c) \\
 \Rightarrow & \exists q: (p<q \wedge q<r\wedge w[q]=b)
\end{array}
\right)
\right\}
$

\bigskip
\begin{verbatim}
c^* (a + (b c^*))^*
\end{verbatim}


\end{slide}


\begin{slide}{Highscore: kontextfreie Grammatiken}

eindeutige Grammatik für $\{ w : 2|w|_a = |w|_b \}$

\begin{verbatim}
Grammatik
    { terminale = mkSet "ab" 
    , variablen = mkSet "S" , start = 'S'
    , regeln = mkSet 
     [ ( "S" , "" ) 
     , ( "S" , "SaSbSb" ) 
     , ( "S" , "SbSbSa" )
     , ( "S" , "SbSaSb" ) ]
    }
\end{verbatim}

\end{slide}

\begin{slide}{Highscore: Kellersprachen (JVM)}

\end{slide}

\begin{slide}{Highscore: Takeuchi-Funktionen}
\begin{verbatim}
forall x y z . t (x , y , z) == 
   if x <= y then z + 1
   else t ( t (x - 1 , y , z) 
          , t (y - 1 , z , x) 
          , t (z - 1 , x , y))

t (x , y , z) = 
   if x <= y then z + 1
   else if z < y + 2 then y + 2 else x + 3
\end{verbatim}
\end{slide}

\begin{slide}{Highscore: while/goto}
  
\begin{verbatim}
p: a;
q: b;
if (c) goto p;
if (d) goto q;

a; b;
while(d || c) {
  if (c) { a; }
  b;
}
\end{verbatim}


\end{slide}

\begin{slide}{Highscore-Gewinner}

\begin{verbatim}
106 :  5*64* :   3   2   1       1                    
 84 :  5*83* :   2   1   2       1           1        
 34 :  5*88* :   1                   1   2           1
 33 :  5*93* :   1       1                       1   1
 32 :  5*09* :       1   1   1                        
\end{verbatim}

\end{slide}
