Rules Standalone
This commit is contained in:
Andreas Stadelmeier
parent
7aa7ec3d21
commit
ac0717f4f2
267
vortragKRRUpSeminar/latexImages/rules.tex
Normal file
267
vortragKRRUpSeminar/latexImages/rules.tex
Normal file
@ -0,0 +1,267 @@
|
|||||||
|
% This is samplepaper.tex, a sample chapter demonstrating the
|
||||||
|
% LLNCS macro package for Springer Computer Science proceedings;
|
||||||
|
% Version 2.21 of 2022/01/12
|
||||||
|
%
|
||||||
|
\documentclass{standalone}
|
||||||
|
\usepackage{underscore}
|
||||||
|
\usepackage[T1]{fontenc}
|
||||||
|
% T1 fonts will be used to generate the final print and online PDFs,
|
||||||
|
% so please use T1 fonts in your manuscript whenever possible.
|
||||||
|
% Other font encondings may result in incorrect characters.
|
||||||
|
%
|
||||||
|
\usepackage{graphicx}
|
||||||
|
% Used for displaying a sample figure. If possible, figure files should
|
||||||
|
% be included in EPS format.
|
||||||
|
%
|
||||||
|
% If you use the hyperref package, please uncomment the following two lines
|
||||||
|
% to display URLs in blue roman font according to Springer's eBook style:
|
||||||
|
%\usepackage{color}
|
||||||
|
%\renewcommand\UrlFont{\color{blue}\rmfamily}
|
||||||
|
%\urlstyle{rm}
|
||||||
|
%
|
||||||
|
\include{prolog}
|
||||||
|
\usepackage{mathpartir}
|
||||||
|
\usepackage{amsmath}
|
||||||
|
\usepackage{amssymb}
|
||||||
|
\usepackage{amsthm}
|
||||||
|
\usepackage{enumitem}
|
||||||
|
\usepackage{xcolor}
|
||||||
|
%\usepackage{amsthm}
|
||||||
|
|
||||||
|
|
||||||
|
\newtheorem{theorem}{Theorem}
|
||||||
|
\newtheorem{lemma}[theorem]{Lemma}
|
||||||
|
|
||||||
|
\begin{document}
|
||||||
|
\begin{tabular}{lcll}
|
||||||
|
$c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
|
||||||
|
$\type{T} $ & $::=$ & $\tv{a} \mid \type{N}$ & Type placeholder or Type \\
|
||||||
|
$\ntype{N}$ & $::=$ & $\exptype{C}{\ol{T}}$ & Class Type containing type placeholders\\
|
||||||
|
$\gtype{G}$ & $::=$ & $\exptype{C}{\ol{G}}$ & Class Type not containing type placeholders \\
|
||||||
|
\end{tabular}
|
||||||
|
|
||||||
|
%\subsection{Subtyping}
|
||||||
|
\begin{mathpar}
|
||||||
|
\inferrule[S-Refl]{}{
|
||||||
|
\type{T} <: \type{T}
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[S-Trans]{\type{T}_1 <: \type{T}_2 \\ \type{T}_2 <: \type{T}_3}{
|
||||||
|
\type{T}_1 <: \type{T}_3
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[S-Var]{}{\type{A} <: \Delta(\type{A})}
|
||||||
|
\and
|
||||||
|
\inferrule[S-Class]{\texttt{class}\ \exptype{C}{\ol{X}} \triangleleft \type{N}}{
|
||||||
|
\exptype{C}{\ol{T}} <: [\ol{T}/\ol{X}]\type{N}
|
||||||
|
}
|
||||||
|
\end{mathpar}
|
||||||
|
\begin{mathpar}
|
||||||
|
\inferrule[N-Refl]{}{
|
||||||
|
\type{C} << \type{C}
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[N-Trans]{\type{C}_1 << \type{C}_2 \\ \type{C}_2 << \type{C}_3}{
|
||||||
|
\type{C}_1 << \type{C}_3
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[N-Class]{\texttt{class}\ \exptype{C}{\ldots} \triangleleft \exptype{D}{\ldots}}{
|
||||||
|
\type{C} << \type{D}
|
||||||
|
}
|
||||||
|
\end{mathpar}
|
||||||
|
|
||||||
|
\label{sec:implicationRules}
|
||||||
|
\begin{mathpar}
|
||||||
|
\inferrule[Subst-L]{
|
||||||
|
\tv{a} \doteq \type{T}_1 \\
|
||||||
|
\tv{a} \lessdot \type{T}_2
|
||||||
|
}{
|
||||||
|
\type{T}_1 \lessdot \type{T}_2
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[Subst-R]{
|
||||||
|
\tv{a} \doteq \type{T}_1 \\
|
||||||
|
\type{T}_2 \lessdot \tv{a}
|
||||||
|
}{
|
||||||
|
\type{T}_2 \lessdot \type{T}_1
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[Subst-Equal]{
|
||||||
|
\tv{a} \doteq \type{T}_1 \\
|
||||||
|
\tv{a} \doteq \type{T}_2
|
||||||
|
}{
|
||||||
|
\type{T}_1 \doteq \type{T}_2
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[Swap]{
|
||||||
|
\type{T}_1 \doteq \type{T}_2
|
||||||
|
}{
|
||||||
|
\type{T}_2 \doteq \type{T}_1
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[Unfold]{
|
||||||
|
\tv{b} \doteq \exptype{C}{\type{T}_1 \ldots \type{T}_n}
|
||||||
|
}{
|
||||||
|
\type{T}_i \doteq \type{T}_i
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[Unfold']{
|
||||||
|
\tv{b} \lessdot \exptype{C}{\type{T}_1 \ldots \type{T}_n}
|
||||||
|
}{
|
||||||
|
\type{T}_i \doteq \type{T}_i
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[Subst-Param]{
|
||||||
|
\type{T}' \doteq \type{S} \\
|
||||||
|
\type{T} \doteq \exptype{C}{\type{T}_1 \ldots, \type{T}', \ldots \type{T}_n} \\
|
||||||
|
}{
|
||||||
|
\type{T} \doteq \exptype{C}{\type{T}_1, \ldots \type{S}, \ldots \type{T}_n}
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[Subst-Param']{
|
||||||
|
\type{T}' \doteq \type{S} \\
|
||||||
|
\tv{b} \lessdot \exptype{C}{\type{T}_1 \ldots, \type{T}', \ldots \type{T}_n} \\
|
||||||
|
}{
|
||||||
|
\tv{b} \lessdot \exptype{C}{\type{T}_1, \ldots \type{S}, \ldots \type{T}_n}
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[S-Object]{}{\tv{a} \lessdot \type{Object}}
|
||||||
|
\and
|
||||||
|
\inferrule[Match]{
|
||||||
|
\tv{a} \lessdot \type{N}_1 \\
|
||||||
|
\tv{a} \lessdot \type{N}_2 \\
|
||||||
|
\type{N}_1 << \type{N}_2
|
||||||
|
}{
|
||||||
|
\type{N}_1 \lessdot \type{N}_2
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[Adopt]{
|
||||||
|
\tv{a} \lessdot \tv{b} \\
|
||||||
|
\tv{b} \lessdot \type{T}
|
||||||
|
}{
|
||||||
|
\tv{a} \lessdot \type{T}
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
% \inferrule[Subst-Param]{
|
||||||
|
% \tv{a} \doteq \type{N} \\
|
||||||
|
% \tv{a} = \type{T}_i \\
|
||||||
|
% \exptype{C}{\type{T}_1 \ldots \type{T}_n} \lessdot \type{T} \\
|
||||||
|
% }{
|
||||||
|
% \type{T}_i \doteq \type{N} \\
|
||||||
|
% }
|
||||||
|
\and
|
||||||
|
\inferrule[Adapt]{
|
||||||
|
\type{N}_1 \lessdot \exptype{C}{\type{T}_1 \ldots \type{T}_n} \\
|
||||||
|
\type{N}_1 <: \exptype{C}{\type{S}_1 \ldots \type{S}_n} \\
|
||||||
|
}{
|
||||||
|
\exptype{C}{\type{S}_1 \ldots \type{S}_n} \doteq \exptype{C}{\type{T}_1 \ldots \type{T}_n} \\
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[Reduce]{
|
||||||
|
\exptype{C}{\type{S}_1 \ldots \type{S}_n} \doteq \exptype{C}{\type{T}_1 \ldots \type{T}_n} \\
|
||||||
|
}{
|
||||||
|
\type{S}_i \doteq \type{T}_i \\
|
||||||
|
}
|
||||||
|
\end{mathpar}
|
||||||
|
|
||||||
|
\begin{mathpar}
|
||||||
|
\text{Apply only once per constraint:}\quad
|
||||||
|
\inferrule[Super]{
|
||||||
|
\type{N} \lessdot \tv{a}\\
|
||||||
|
\type{N} <: \type{N}'
|
||||||
|
}{
|
||||||
|
\tv{a} \doteq \type{N}'
|
||||||
|
}
|
||||||
|
\end{mathpar}
|
||||||
|
|
||||||
|
\begin{mathpar}
|
||||||
|
\inferrule[Split-L]{
|
||||||
|
\tv{a} \lessdot \tv{b}\\
|
||||||
|
\tv{a} \lessdot \type{N}\\
|
||||||
|
}{
|
||||||
|
\tv{b} \lessdot \type{N}
|
||||||
|
}
|
||||||
|
\quad \quad
|
||||||
|
\vline
|
||||||
|
\quad \quad
|
||||||
|
\inferrule[Split-R]{
|
||||||
|
\tv{a} \lessdot \tv{b}\\
|
||||||
|
\tv{a} \lessdot \type{N}\\
|
||||||
|
}{
|
||||||
|
\type{N} \lessdot \tv{b}
|
||||||
|
}
|
||||||
|
\end{mathpar}
|
||||||
|
|
||||||
|
Result:
|
||||||
|
\begin{mathpar}
|
||||||
|
\inferrule[Solution]{
|
||||||
|
\tv{a} \doteq \type{G}
|
||||||
|
}{
|
||||||
|
\sigma(\tv{a}) = \type{G}
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[Solution-Gen]{
|
||||||
|
\tv{a} \lessdot \type{C}_1, \ldots, \tv{a} \lessdot \type{C}_n \\
|
||||||
|
\forall i: \type{C}_m << \type{C}_i \\
|
||||||
|
}{
|
||||||
|
\tv{a} \doteq \type{C}_m
|
||||||
|
}
|
||||||
|
% \and
|
||||||
|
% \inferrule[Solution-Gen]{
|
||||||
|
% \tv{a} \lessdot \type{C}\\
|
||||||
|
% \sigma(\tv{a}) = \emptyset
|
||||||
|
% }{
|
||||||
|
% \tv{a} \doteq \type{A} \\ \sigma'(\tv{a}) = \type{A}
|
||||||
|
% }
|
||||||
|
% \and
|
||||||
|
% \inferrule[Solution-Gen]{
|
||||||
|
% \tv{a} \lessdot \type{G} \\
|
||||||
|
% \tv{a} \lessdot \type{G}_1, \ldots, \tv{a} \lessdot \type{G}_n \\
|
||||||
|
% \forall i: \type{G} << \type{G}_i \\
|
||||||
|
% \sigma'(\tv{a}) = \type{A}
|
||||||
|
% }{
|
||||||
|
% \Delta(\type{A}) = \type{G}
|
||||||
|
% }
|
||||||
|
\end{mathpar}
|
||||||
|
|
||||||
|
Fail:
|
||||||
|
|
||||||
|
\begin{mathpar}
|
||||||
|
% \inferrule[Fail]{
|
||||||
|
% \type{T} \lessdot \type{N}\\
|
||||||
|
% \type{T} \nless : \type{N}
|
||||||
|
% }{
|
||||||
|
% \emptyset
|
||||||
|
% }
|
||||||
|
% \and
|
||||||
|
\inferrule[Fail]{
|
||||||
|
\exptype{C}{\ldots} \doteq \exptype{D}{\ldots}\\
|
||||||
|
\type{C} \neq \type{D}
|
||||||
|
}{
|
||||||
|
\emptyset
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[Fail-Generic]{
|
||||||
|
\type{X} \doteq \type{T}\\
|
||||||
|
\type{X} \neq \type{T}
|
||||||
|
}{
|
||||||
|
\emptyset
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[Fail-Sigma]{
|
||||||
|
\tv{a} \doteq \type{N} \\
|
||||||
|
\tv{a} \in \type{N}
|
||||||
|
}{
|
||||||
|
\emptyset
|
||||||
|
}
|
||||||
|
\and
|
||||||
|
\inferrule[Fail]{
|
||||||
|
\tv{a} \lessdot \type{N}_1 \\
|
||||||
|
\tv{a} \lessdot \type{N}_2 \\
|
||||||
|
\text{not}\ \type{N}_1 << \type{N}_2 \\
|
||||||
|
\text{not}\ \type{N}_2 << \type{N}_1
|
||||||
|
}{
|
||||||
|
\emptyset
|
||||||
|
}
|
||||||
|
\end{mathpar}
|
||||||
|
\end{document}
|
||||||
Loading…
Reference in New Issue
Block a user