\documentclass[landscape]{seminar}
\usepackage{alltt,graphicx,fixseminar,latexsym,color}
%
\newenvironment{Maude}[1]
{\begin{center}\begin{minipage}{#1}\begin{alltt}}
{\end{alltt}\end{minipage}\end{center}}

\newenvironment{Slide}[1]
{
\begin{slide}
\sf
\begin{center}
\textcolor{cyan}{\Large\em #1}
\end{center}
}
{
\end{slide}
}
\newcommand{\la}{\langle}
\newcommand{\ra}{\rangle}
\newcommand{\EM}[1]{\textcolor{red}{\em #1}}
%
\begin{document}

\begin{Slide}{\huge The Maude 2.0 System}
\begin{center}
\vspace{0.5in}
M. Clavel\ \ \ \ F. Dur\'{a}n\ \ \ \ S. Eker\ \ \ \ P. Lincoln\\
\vspace{.2in}
N. Mart\'{\i}-Oliet\ \ \ \ J. Meseguer\ \ \ \ C. Talcott 
\end{center}
\end{Slide}


\begin{Slide}{Sort System}
\begin{itemize}
\item \EM{Kinds} replace the \EM{Error Sorts}
of Maude 1 and can be used in operator and variable declarations.
\end{itemize}
\begin{Maude}{3.3in}
op f : [Nat] -> Nat .  *** error recovery.
\end{Maude}
\begin{itemize}
\item Operators can be declared at the kind level to indicate
partiality.
\end{itemize}
\begin{Maude}{3.3in}
op gamma : [Real] -> [Real] .
op gamma : Real ~> Real .
\end{Maude}
\begin{itemize}
\item Rewriting can occur at kind level for error recovery.
\item Canonical name for a kind is its maximal sort(s), separated by
commas and enclosed in brackets.
\item Union sorts abolished.
\end{itemize}
\end{Slide}


\begin{Slide}{Variables}
\begin{itemize}
\item Each sort or kind $t$ is considered to have a countable set of
variables $v:t$ for any Maude identifier $v$, which do not have to be declared.
\item A variable declaration {\tt var v : t .} is now considered to
declare $v$ as an \EM{alias} for the variable $v:t$.
\end{itemize}
\vspace{0.25in}
\begin{Maude}{3.3in}
parse in BOOL : X:Bool .
red in BOOL : X:Bool == X:[Bool] .  *** false
\end{Maude}
\end{Slide}


\begin{Slide}{Conditions}
\begin{itemize}
\item Rather than a single equality, conditions now allow a list of
\EM{condition fragments}, separated by \textcolor{red}{$/\backslash$}.
\item 4 types of fragments; last type is for rule conditions only:
\end{itemize}
\begin{center}
\begin{tabular}{|l|l|}
\hline
$\la$term$\ra$ = $\la$term$\ra$ & equality test \\
\hline
$\la$term$\ra$ : $\la$sort$\ra$ & sort test \\
\hline
$\la$pattern$\ra$ := $\la$term$\ra$ & assignment by matching \\
\hline
$\la$term$\ra$ $=>$ $\la$pattern$\ra$ & rewrite proof search \\
\hline
\end{tabular}
\end{center}
\begin{itemize}
\item Patterns may have unbound variables that are bound by matching;
regular terms are reduced upto strategy.
\item Failure of a fragment causes backtracking.
\end{itemize}
\end{Slide}


\begin{Slide}{Statement Attributes}
\begin{itemize}
\item Statements can now take a list of attributes.
\item Label attribute can be given to any statement, not just
rules.
\item Can be used with \EM{trace select} feature to select statements
for tracing.
\item Metadata attribute can attach arbitrary string of meta-data to a
statement for meta-processing.
\end{itemize}
\begin{Maude}{3.3in}
eq X * X - Y * Y = (X + Y) * (X - Y)
  [label diff-sqrs metadata "lemma"] .
\end{Maude}
\end{Slide}


\begin{Slide}{Ctor and Ditto Attributes}
\begin{itemize}
\item Ctor attribute allows operators to be declared as constructors
--- needed for ITP and used in term coloring.
\item Ditto copies all attributes other than ctor from a previous
subsort overloaded declaration of the operator.
% --- especially useful
%for overloaded built-in operators with there complex {\em special}
%attributes.
\end{itemize}
\begin{Maude}{3.3in}
fmod CTOR-&-DITTO-TEST is
  sorts NzNat Nat Int .
  subsorts NzNat < Nat < Int .
  op 0 : -> Nat [ctor] .
  op s_ : Nat -> NzNat [ctor prec 14] .
  op s_ : Int -> Int [ditto] .  *** non-ctor
  op -_ : NzNat -> Int [ctor prec 14] .
  op -_ : Int -> Int [ditto] .  *** non-ctor
endfm
\end{Maude}
\end{Slide}


\begin{Slide}{Iter Attribute}
\begin{itemize}
\item Allows efficient storage, i/o and sort computations for huge
towers of unary operator symbols.
\item Main application is the efficient implementation of natural
numbers using the successor notation.
\end{itemize}
\begin{Maude}{3in}
fmod ITER-TEST is
  sorts Even Odd Nat .
  subsorts Even Odd < Nat .
  op 0 : -> Even .
  op s_ : Even -> Odd [iter] .
  op s_ : Odd -> Even [iter] .
endfm

red s_^123456789(0) .
red s_^1234567890(0) .
\end{Maude}
\end{Slide}


\begin{Slide}{Format Attribute}
\begin{itemize}
\item Allows control of white-space, color and style for pretty-printing
operators.
\item Format words are given for each white-space position.
\end{itemize}
\begin{center}
\begin{tabular}{|ll|ll|}
\hline
s & space & r & red \\
\hline
t & tab & g & green \\
\hline
+ & increment indent counter & b & blue \\
\hline
- & decrement indent counter & y & yellow \\
\hline
i & indent by indent counter & m &  magenta \\
\hline
n & new line & c & cyan \\
\hline
d & default spacing & u & underline \\
\hline
o & original style & ! & bright \\
\hline
\end{tabular}
\end{center}
\end{Slide}


\begin{Slide}{Format Attribute (continued)}
\begin{Maude}{3.75in}
op while _ do _ od : Bool Statement -> Statement . 
  ^     ^ ^  ^ ^  ^

op let _ := _ : Variable Expression -> Statement .
  ^   ^ ^  ^ ^
\end{Maude}
\vspace{0.25in}
\begin{Maude}{3.75in}
op while _ do _ od : Bool Statement -> Statement
  [format (nir! o r! o++ --nir! o)] .

op let _ := _ : Variable Expression -> Statement
  [format (nir! o d d d)] .
\end{Maude}
\end{Slide}


%
%	Built-in Modules
%
\begin{Slide}{Natural Numbers}
\begin{itemize}
\item Nats are constructed using successor operator and the \EM{iter}
attribute.
\end{itemize}
\begin{Maude}{3.3in}
fmod NAT is
  sorts Zero NzNat Nat .
  subsort Zero NzNat < Nat .
  op 0 : -> Zero [ctor] .
  op s_ : Nat -> NzNat
    [ctor iter special (...)] .
  ...
endfm
\end{Maude}
\begin{itemize}
\item Decimal i/o by default.
\item Built-in operators very efficient (use GNU GMP).
\item Gcd, lcm, mod exp, bitwise ops.
\end{itemize}
\end{Slide}


\begin{Slide}{Natural Numbers (continued)}
\begin{Maude}{3.3in}
red in NAT : gcd(18, gcd(X:Nat, 12)) .

fmod COMBINATORIAL is protecting NAT .
  op _! : Nat -> NzNat .
  op C : Nat Nat -> Nat .

vars N M : Nat .
  eq 0 ! = s 0 .
  eq (s N) ! = s N * N ! .
  eq C(N, M) = N ! quo (M ! * sd(N, M) !) .
endfm

red 1000 ! .
red C(1000, 100) .
\end{Maude}
\end{Slide}


\begin{Slide}{Integers}
\begin{itemize}
\item Ints are constructed from Nats using unary minus operator.
\end{itemize}
\begin{Maude}{3.3in}
fmod INT is protecting NAT .
  sorts NzInt Int .
  subsorts NzNat < NzInt Nat < Int .
  op -_ : NzNat -> NzInt
    [ctor special (...)] .
  op -_ : NzInt -> NzInt [ditto] .
  op -_ : Int -> Int [ditto] .
  ...
endfm
\end{Maude}
\begin{itemize}
\item Adds binary minus, not and abs.
\item Most Nat ops extended.
\end{itemize}
\end{Slide}


\begin{Slide}{Rational Numbers}
\begin{itemize}
\item Rats are constructed from Nats and Ints using division
operator.
\end{itemize}
\begin{Maude}{3.3in}
fmod RAT is protecting INT .
  sorts NzRat Rat .
  subsorts NzInt < NzRat Int < Rat .
  op _/_ : NzInt NzNat -> NzRat
    [ctor prec 31 gather (E e) special (...)] .
  op _/_ : NzRat NzRat -> NzRat [ditto] .
  op _/_ : Rat NzRat -> Rat [ditto] .
  ...
endfm
\end{Maude}
\begin{itemize}
\item Supports usual arithmetic, comparison, abs, ceiling, floor, frac,
trunc.
\item Implemented by Maude equations rather than by built-ins.
\end{itemize}
\end{Slide}


\begin{Slide}{Floating Point Numbers}
\begin{itemize}
\item Floats are treated as a large set of constants - no algebraic
structure.
\item Underlying representation is hardware double precision floating
point numbers; IEEE 754 on recent hardware.
\item +/- Infinity supported.
\item All usual floating points ops supported; known inconsistencies
at corner cases patched.
\end{itemize}
\end{Slide}


\begin{Slide}{Character Strings}
\begin{itemize}
\item Strings are treated as a countable set of constants - no algebraic
structure.
\item Uses Nats for length, positions.
\item Underlying representation is the C++ STL extension \EM{ropes}.
\item Heavyweight strings that support sharing and persistence
efficiently for functional languages.
\item Supports concatenation, length, comparison, substrings, find/rfind.
\end{itemize}
\end{Slide}


\begin{Slide}{Conversion Functions}
\begin{itemize}
\item FiniteFloat to Rat is exact.
\item Rat to Float is nearest available Float; may be +/- Infinity.
\item Rat to and from String is exact; choice of representation base.
\item String to Float is nearest available Float; may be +/- Infinity.
\item Float to String has enough significant digits that converting
back finds the original Float.
\item Exact decimal expansion of a Float is available for fancier i/o
processing - may be huge.
\end{itemize}
\end{Slide}


\begin{Slide}{LTL Model Checker}
\begin{itemize}
\item Linear Temporal Logic manipulations (simplifications and
negative normal form) are done by Maude code.
\item The satisfaction of (possibly parameterized) propositions are
defined in Maude.
\item On-the-fly model checking is done by a built-in operation
\end{itemize}
\begin{Maude}{3.3in}
op _|=_ : State Formula ~> ModelCheckResult
  [special (...)] .
\end{Maude}
\begin{itemize}
\item Implementation uses state-of-the-art Buchi automaton construction
algorithm and standard double depth first search of the synchronous
product for a counterexample.
\item LTL Satisfiability solving and tautology checking also provided.
\end{itemize}
\end{Slide}


\begin{Slide}{New Meta Level}
\begin{itemize}
\item Simpler metaterm representation:
\begin{Maude}{3.3in}
1.0 + X:Float
\end{Maude}
is meta-represented as
\begin{Maude}{3.3in}
'_+_['1.0.FiniteFloat, 'X:Float]
\end{Maude}
\item Many more descent functions such as metaXapply() (with contexts)
and metaSearch().
\item Descent functions return sorts of terms.
\item Ascent functions to inspect modules in database.
\item Much more sophisticated caching at module and operator level.
\end{itemize}
\end{Slide}
%
%	Commands & Misc
%
\begin{Slide}{Search Command}
\begin{center}
\begin{itemize}
\item Breadth first search with cycle detection.
\item All nodes in search graph reduce w.r.t. equations.
\item Optional backtracking to find more solutions.
\item Path to a given solution and current search graph can be
printed.
\end{itemize}
\begin{Maude}{3.75in}
search <term> <search-type> <pattern>
  such that <condition> .
\end{Maude}
\begin{tabular}{|l|l|}
\hline
$=>$ & exactly one rewrite \\
\hline
$=>\ast$ & zero or more rewrites \\
\hline
$=>+$ & one or more rewrites \\
\hline
$=>!$ & until no more rules apply \\
\hline
\end{tabular}
\end{center}
\end{Slide}


\begin{Slide}{Profiling}
\begin{itemize}
\item Keep track of how many times each eq/mb/rl is applied.
\item For a condition, also keep track for each fragment of
\begin{itemize}
\item Initial attempts.
\item Backtrack attempts.
\item Successes.
\item Failures.
\end{itemize}
\end{itemize}
\vspace{0.25in}
\begin{Maude}{3.3in}
set profile on .
...
show profile .
\end{Maude}
\end{Slide}


\begin{Slide}{Term Coloring}
\begin{itemize}
\item Color (possibly intermediate) results based on reduced flag and
constructor status to flag problems.
\end{itemize}
\begin{Maude}{3.3in}
set print color on .
\end{Maude}
\begin{center}
\begin{tabular}{|l|l|}
\hline
reduced, ctor &	not colored \\
\hline
reduced, non-ctor, colored below & \textcolor{blue}{blue} \\
\hline
reduced, non-ctor, no colored below & \textcolor{red}{red} \\
\hline
unreduced, no reduced above & \textcolor{green}{green} \\
\hline
unreduced, reduced directly above & \textcolor{magenta}{magenta} \\
\hline
unreduced, reduced not directly above & \textcolor{cyan}{cyan} \\
\hline
\end{tabular}
\end{center}
\begin{itemize}
\item \textcolor{red}{Red} and \textcolor{magenta}{magenta} denote
likely origin of problem, \textcolor{blue}{blue} and
\textcolor{cyan}{cyan} denote secondary damage.
\end{itemize}
\end{Slide}


\begin{Slide}{Miscellaneous Features}
\begin{itemize}
\item Frozen attribute prevents selected arguments of an operator from
being rewritten by rules.
\item Position fair rewriting make bottom-up passes over the term,
applying a certain number of rule rewrites at each position.
Since rule rewriting is non-destructive, term graph is \EM{virtual}
unless forced by tracing or debugging.
\item Break to debugger when select operators rewrite or statements
with given labels execute.
\item Integrated compiler for sublanguage --- GNU g++ used as
backend. Speed up is typically a factor of 5-9.
\end{itemize}
\end{Slide}


\begin{Slide}{Optimizations}
\begin{itemize}
\item Rules can now use \EM{greedy matching} under some circumstances.
\item Left-to-right sharing allows reuse of matched subterms in rhs or
condition. Matched subterms themselves can be in earlier condition
fragments.
\item New discrimination nets allow order-sorted partial subsumption
analysis.
\item Substitution slot coloring used to minimize size of
substitutions by slot reuse - a win for large rhs.
\end{itemize}
\end{Slide}

\end{document}
