\documentclass[dvipsnames,14pt,t]{beamer}+ −
\usepackage{slides}+ −
\usepackage{langs}+ −
\usepackage{graph}+ −
\usepackage{data}+ −
\usepackage{proof}+ −
+ −
% beamer stuff + −
\renewcommand{\slidecaption}{ITP ????}+ −
\newcommand{\bl}[1]{\textcolor{blue}{#1}}+ −
+ −
+ −
\begin{document}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[t]+ −
\frametitle{%+ −
\begin{tabular}{@ {}c@ {}}+ −
\\+ −
\Large POSIX Lexing with Derivatives\\[-1.5mm] + −
\Large of Regular Expressions\\+ −
\Large (Proof Pearl)\\[-1mm] + −
\end{tabular}}\bigskip\bigskip\bigskip+ −
+ −
\normalsize+ −
\begin{center}+ −
\begin{tabular}{c}+ −
\small Fahad Ausaf\\+ −
\small King's College London\\+ −
\\+ −
\small joint work with Roy Dyckhoff and Christian Urban+ −
\end{tabular}+ −
\end{center}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{Regular Expressions}+ −
+ −
+ −
\begin{textblock}{6}(2,5)+ −
\begin{tabular}{rrl@ {\hspace{13mm}}l}+ −
\bl{$r$} & \bl{$::=$} & \bl{$\varnothing$} & null\\+ −
& \bl{$\mid$} & \bl{$\epsilon$} & empty string\\+ −
& \bl{$\mid$} & \bl{$c$} & character\\+ −
& \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\+ −
& \bl{$\mid$} & \bl{$r_1 + r_2$} & alternative / choice\\+ −
& \bl{$\mid$} & \bl{$r^*$} & star (zero or more)\\+ −
\end{tabular}+ −
\end{textblock}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{The Derivative of a Rexp}+ −
+ −
\large+ −
If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular + −
expression that matches just \bl{$s$}?\bigskip\bigskip\bigskip\bigskip+ −
+ −
\small+ −
\bl{$der\,c\,r$} gives the answer, Brzozowski (1964), Owens (2005)+ −
``\ldots have been lost in the sands of time\ldots''+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{Correctness}+ −
+ −
It is a relative easy exercise in a theorem prover:+ −
+ −
\begin{center}+ −
\bl{$matches(r, s)$} if and only if \bl{$s \in L(r)$} + −
\end{center}\bigskip+ −
+ −
\small+ −
where \bl{$matches(r, s) \dn nullable(ders(r, s))$}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{POSIX Regex Matching}+ −
+ −
Two rules:+ −
+ −
\begin{itemize}+ −
\item Longest match rule (``maximal munch rule''): The + −
longest initial substring matched by any regular expression + −
is taken as the next token.+ −
+ −
\begin{center}+ −
\bl{$\texttt{\Grid{iffoo\VS bla}}$}+ −
\end{center}\medskip+ −
+ −
\item Rule priority:+ −
For a particular longest initial substring, the first regular+ −
expression that can match determines the token.+ −
+ −
\begin{center}+ −
\bl{$\texttt{\Grid{if\VS bla}}$}+ −
\end{center}+ −
\end{itemize}\bigskip\pause+ −
+ −
\small+ −
\hfill Kuklewicz: most POSIX matchers are buggy\\+ −
\footnotesize+ −
\hfill \url{http://www.haskell.org/haskellwiki/Regex_Posix}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{POSIX Regex Matching}+ −
+ −
\begin{itemize}+ −
+ −
\item Sulzmann \& Lu came up with a beautiful+ −
idea for how to extend the simple regular expression + −
matcher to POSIX matching/lexing (FLOPS 2014)\bigskip\bigskip+ −
+ −
\begin{tabular}{@{\hspace{4cm}}c@{}}+ −
\includegraphics[scale=0.20]{pics/sulzmann.jpg}\\[-2mm]+ −
\hspace{0cm}\footnotesize Martin Sulzmann+ −
\end{tabular}\bigskip\bigskip+ −
+ −
\item the idea: define an inverse operation to the derivatives+ −
\end{itemize}+ −
+ −
+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{Regexes and Values}+ −
+ −
Regular expressions and their corresponding values+ −
(for \emph{how} a regular expression matched a string):+ −
+ −
\begin{center}+ −
\begin{columns}+ −
\begin{column}{3cm}+ −
\begin{tabular}{@{}rrl@{}}+ −
\bl{$r$} & \bl{$::=$} & \bl{$\varnothing$}\\+ −
& \bl{$\mid$} & \bl{$\epsilon$} \\+ −
& \bl{$\mid$} & \bl{$c$} \\+ −
& \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\+ −
& \bl{$\mid$} & \bl{$r_1 + r_2$} \\+ −
\\+ −
& \bl{$\mid$} & \bl{$r^*$} \\+ −
\\+ −
\end{tabular}+ −
\end{column}+ −
\begin{column}{3cm}+ −
\begin{tabular}{@{\hspace{-7mm}}rrl@{}}+ −
\bl{$v$} & \bl{$::=$} & \\+ −
& & \bl{$Empty$} \\+ −
& \bl{$\mid$} & \bl{$Char(c)$} \\+ −
& \bl{$\mid$} & \bl{$Seq(v_1,v_2)$}\\+ −
& \bl{$\mid$} & \bl{$Left(v)$} \\+ −
& \bl{$\mid$} & \bl{$Right(v)$} \\+ −
& \bl{$\mid$} & \bl{$[]$} \\+ −
& \bl{$\mid$} & \bl{$[v_1,\ldots\,v_n]$} \\+ −
\end{tabular}+ −
\end{column}+ −
\end{columns}+ −
\end{center}\pause+ −
+ −
There is also a notion of a string behind a value: \bl{$|v|$}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{Sulzmann \& Lu Matcher}+ −
+ −
We want to match the string \bl{$abc$} using \bl{$r_1$}:+ −
+ −
\begin{center}+ −
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]+ −
\node (r1) {\bl{$r_1$}};+ −
\node (r2) [right=of r1] {\bl{$r_2$}};+ −
\draw[->,line width=1mm] (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};\pause+ −
\node (r3) [right=of r2] {\bl{$r_3$}};+ −
\draw[->,line width=1mm] (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};\pause+ −
\node (r4) [right=of r3] {\bl{$r_4$}};+ −
\draw[->,line width=1mm] (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};\pause+ −
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$\;\;nullable?$}}};\pause+ −
\node (v4) [below=of r4] {\bl{$v_4$}};+ −
\draw[->,line width=1mm] (r4) -- (v4);\pause+ −
\node (v3) [left=of v4] {\bl{$v_3$}};+ −
\draw[->,line width=1mm] (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};\pause+ −
\node (v2) [left=of v3] {\bl{$v_2$}};+ −
\draw[->,line width=1mm] (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};\pause+ −
\node (v1) [left=of v2] {\bl{$v_1$}};+ −
\draw[->,line width=1mm] (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};\pause+ −
\draw[->,line width=0.5mm] (r3) -- (v3);+ −
\draw[->,line width=0.5mm] (r2) -- (v2);+ −
\draw[->,line width=0.5mm] (r1) -- (v1);+ −
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};+ −
\end{tikzpicture}+ −
\end{center}+ −
+ −
\only<10>{+ −
The original ideas of Sulzmann and Lu are the \bl{\textit{mkeps}} + −
and \bl{\textit{inj}} functions (ommitted here).}+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[t,squeeze]+ −
\frametitle{Sulzmann \& Lu Paper}+ −
+ −
\begin{itemize}+ −
\item I have no doubt the algorithm is correct --- + −
the problem is I do not believe their proof.+ −
+ −
\begin{center}+ −
\begin{bubble}[10cm]\small+ −
``How could I miss this? Well, I was rather careless when + −
stating this Lemma :)\smallskip+ −
+ −
Great example how formal machine checked proofs (and + −
proof assistants) can help to spot flawed reasoning steps.''+ −
\end{bubble}+ −
\end{center}\pause+ −
+ −
\begin{center}+ −
\begin{bubble}[10cm]\small+ −
``Well, I don't think there's any flaw. The issue is how to + −
come up with a mechanical proof. In my world mathematical + −
proof $=$ mechanical proof doesn't necessarily hold.''+ −
\end{bubble}+ −
\end{center}\pause+ −
+ −
\end{itemize}+ −
+ −
\only<3>{%+ −
\begin{textblock}{11}(1,4.4)+ −
\begin{center}+ −
\begin{bubble}[10.9cm]\small\centering+ −
\includegraphics[scale=0.37]{pics/msbug.png}+ −
\end{bubble}+ −
\end{center}+ −
\end{textblock}}+ −
+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{\begin{tabular}{c}The Proof Idea\\[-1mm] by Sulzmann \& Lu+ −
\end{tabular}}+ −
+ −
\begin{itemize}+ −
\item introduce an inductively defined ordering relation + −
\bl{$v \succ_r v'$} which captures the idea of POSIX matching+ −
+ −
\item the algorithm returns the maximum of all possible+ −
values that are possible for a regular expression.\pause+ −
\bigskip\small+ −
+ −
\item the idea is from a paper by Cardelli \& Frisch about + −
GREEDY matching (GREEDY $=$ preferring instant gratification to delayed+ −
repletion):+ −
+ −
\item e.g.~given \bl{$(a + (b + ab))^*$} and string \bl{$ab$}+ −
+ −
\begin{center}+ −
\begin{tabular}{ll}+ −
GREEDY: & \bl{$[Left(a), Right(Left(b)]$}\\+ −
POSIX: & \bl{$[Right(Right(Seq(a, b))))]$} + −
\end{tabular}+ −
\end{center} + −
\end{itemize}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{}+ −
\centering+ −
+ −
+ −
\bl{\infer{\vdash Empty : \epsilon}{}}\hspace{15mm}+ −
\bl{\infer{\vdash Char(c): c}{}}\bigskip+ −
+ −
\bl{\infer{\vdash Seq(v_1, v_2) : r_1\cdot r_2}{\vdash v_1 : r_1 \quad \vdash v_2 : r_2}}+ −
\bigskip+ −
+ −
\bl{\infer{\vdash Left(v) : r_1 + r_2}{\vdash v : r_1}}\hspace{15mm}+ −
\bl{\infer{\vdash Right(v): r_1 + r_2}{\vdash v : r_2}}\bigskip+ −
+ −
\bl{\infer{\vdash [] : r^*}{}}\hspace{15mm}+ −
\bl{\infer{\vdash [v_1,\ldots, v_n] : r^*}+ −
{\vdash v_1 : r \quad\ldots\quad \vdash v_n : r}}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}<1>[c]+ −
\frametitle{}+ −
\small+ −
+ −
%\begin{tabular}{@{}lll@{}}+ −
%\bl{$POSIX(v, r)$} & \bl{$\dn$} & \bl{$\vdash v : r$}\\ + −
% & & \bl{$\wedge \;\;(\forall v'.\;\; \vdash v' : r \,\wedge\, |v'| = |v| + −
% \Rightarrow v \succ_{\alert<2>{r}} v')$}+ −
%\end{tabular}\bigskip\bigskip\bigskip+ −
+ −
+ −
\centering+ −
+ −
%\bl{\infer{Seq(v_1, v_2) \succ_{\alert<2>{r_1\cdot r_2}} Seq(v'_1, v'_2)}+ −
% {v_1 = v'_1 \quad v_2 \succ_{\alert<2>{r_2}} v'_2}}\hspace{3mm}+ −
%\bl{\infer{Seq(v_1, v_2) \succ_{\alert<2>{r_1\cdot r_2}} Seq(v'_1, v'_2)}+ −
% {v_1 \not= v'_1 \quad v_1 \succ_{\alert<2>{r_1}} v'_1}}+ −
%\bigskip+ −
+ −
%\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')}+ −
% {v \succ_{\alert<2>{r_1}} v'}}\hspace{15mm}+ −
%\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')}+ −
% {v \succ_{\alert<2>{r_2}} v'}}\bigskip\medskip+ −
+ −
%\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')}+ −
% {length |v| \ge length |v'|}}\hspace{15mm}+ −
%\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')}+ −
% {length |v| > length |v'|}}\bigskip+ −
+ −
%\bl{$\big\ldots$}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{Problems}+ −
+ −
\begin{itemize}+ −
\item Sulzmann: \ldots Let's assume \bl{$v$} is not + −
a $POSIX$ value, then there must be another one+ −
\ldots contradiction.\bigskip\pause+ −
+ −
\item Exists?+ −
+ −
\begin{center}+ −
\bl{$L(r) \not= \varnothing \;\Rightarrow\; \exists v.\;POSIX(v, r)$}+ −
\end{center}\bigskip\bigskip\pause+ −
+ −
\item in the sequence case + −
\bl{$Seq(v_1, v_2)\succ_{r_1\cdot r_2} Seq(v_1', v_2')$}, + −
the induction hypotheses require+ −
\bl{$|v_1| = |v'_1|$} and \bl{$|v_2| = |v'_2|$}, + −
but you only know+ −
+ −
\begin{center}+ −
\bl{$|v_1| \;@\; |v_2| = |v'_1| \;@\; |v'_2|$}+ −
\end{center}\pause\small+ −
+ −
\item although one begins with the assumption that the two + −
values have the same flattening, this cannot be maintained + −
as one descends into the induction (alternative, sequence)+ −
\end{itemize}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{Our Solution}+ −
+ −
\begin{itemize}+ −
\item a direct definition of what a POSIX value is, using+ −
the relation \bl{$s \in r \to v$} (specification):\medskip+ −
+ −
\begin{center}+ −
\bl{\infer{[] \in \epsilon \to Empty}{}}\hspace{15mm}+ −
\bl{\infer{c \in c \to Char(c)}{}}\bigskip\medskip+ −
+ −
\bl{\infer{s \in r_1 + r_2 \to Left(v)}+ −
{s \in r_1 \to v}}\hspace{10mm}+ −
\bl{\infer{s \in r_1 + r_2 \to Right(v)}+ −
{s \in r_2 \to v & s \not\in L(r_1)}}\bigskip\medskip+ −
+ −
\bl{\infer{s_1 @ s_2 \in r_1 \cdot r_2 \to Seq(v_1, v_2)}+ −
{\small\begin{array}{l}+ −
s_1 \in r_1 \to v_1 \\+ −
s_2 \in r_2 \to v_2 \\+ −
\neg(\exists s_3\,s_4.\; s_3 \not= []+ −
\wedge s_3 @ s_4 = s_2 \wedge+ −
s_1 @ s_3 \in L(r_1) \wedge+ −
s_4 \in L(r_2))+ −
\end{array}}}+ −
+ −
\bl{\ldots} + −
\end{center}+ −
\end{itemize}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{Properties}+ −
+ −
It is almost trival to prove:+ −
+ −
\begin{itemize}+ −
\item Uniqueness+ −
\begin{center}+ −
If \bl{$s \in r \to v_1$} and \bl{$s \in r \to v_2$} then+ −
\bl{$v_1 = v_2$}.+ −
\end{center}\bigskip+ −
+ −
\item Correctness+ −
\begin{center}+ −
\bl{$lexer(r, s) = v$} if and only if \bl{$s \in r \to v$}+ −
\end{center}+ −
\end{itemize}\bigskip\bigskip\pause+ −
+ −
+ −
You can now start to implement optimisations and derive+ −
correctness proofs for them. But we still do not know whether+ −
+ −
\begin{center}+ −
\bl{$s \in r \to v$} + −
\end{center}+ −
+ −
is a POSIX value according to Sulzmann \& Lu's definition+ −
(biggest value for \bl{$s$} and \bl{$r$})+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{Conclusion}+ −
+ −
\begin{itemize}+ −
+ −
\item we replaced the POSIX definition of Sulzmann \& Lu by a+ −
new definition (ours is inspired by work of Vansummeren,+ −
2006)\medskip+ −
+ −
\item their proof contained small gaps (acknowledged) but had+ −
also fundamental flaws\medskip+ −
+ −
\item now, its a nice exercise for theorem proving\medskip+ −
+ −
\item some optimisations need to be applied to the algorithm+ −
in order to become fast enough\medskip+ −
+ −
\item can be used for lexing, is a small beautiful functional+ −
program+ −
+ −
\end{itemize}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[b]+ −
\frametitle{+ −
\begin{tabular}{c}+ −
\mbox{}\\[13mm]+ −
\alert{\LARGE Questions?}+ −
\end{tabular}}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
\end{document}+ −
+ −
+ −
%%% Local Variables: + −
%%% mode: latex+ −
%%% TeX-master: t+ −
%%% End: + −
+ −