playground/latex/nfa-rules.tex

82 lines
1.3 KiB
TeX

\documentclass{article}
\usepackage{mathpartir}
\begin{document}
\begin{figure}
\begin{mathpar}
\inferrule{ }{
fin \notin \delta_\emptyset^*(s, w)
}
\quad (\textsc{Null})
%
\quad \quad
\inferrule{ }{
fin \in \delta_\epsilon^*(fin, \epsilon)
}
\quad (\textsc{Eps})
%
\and
\inferrule{
fin \in \delta_a(s, [a])
}{
fin \in \delta_a^*(s, [a])
}
\quad (\textsc{Char})
%
\and
%
\inferrule{
fin_1 \in \delta_1^*(s, w_1)
\and
fin_2 \in \delta_1^*(fin_1, w_2)
}{
fin_{1 \cdot 2} \in \delta_{1 \cdot 2}^*(s, w_1 \cdot w_2)
}
\quad (\textsc{Cat})
%
\and
\\
\inferrule{
fin_1 \in \delta_1^*(s, w)
}{
fin \in \delta_{1 + 2}^*(s, w)
}
\quad (\textsc{Alt-L})
%
\and
%
\inferrule{
fin_2 \in \delta_2^*(s, w)
}{
fin \in \delta_{1 + 2}^*(s, w)
}
\quad (\textsc{Alt-R})
%
\and
\\
\inferrule{
fin_r \in \delta_r^*(s, w)
}{
fin \in \delta_{r+}^*(s, w)
}
\quad (\textsc{Plus-1})
%
\and
%
\inferrule{
fin_r \in \delta_r^*(s, w_1)
\and
fin_{r+} \in \delta_{r+}^*(fin_r, w_2)
}{
fin \in \delta_{r+}^*(s, w_1 \cdot w_2)
%fin \in \delta_{r+}^*(s, w_1 ++ w_2)
%fin \in \delta_{r+}^*(s, w_1 \mathbin{{+}{+}} w_2)
}
\quad (\textsc{Plus-*})
\end{mathpar}
\caption{Typing rules}
\label{fig:nfa_typing}
\end{figure}
\end{document}