From ac0717f4f256ee74ccfad88c74009a7231cf3ef4 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Tue, 19 Nov 2024 23:16:29 +0100 Subject: [PATCH] Rules Standalone --- vortragKRRUpSeminar/latexImages/rules.tex | 267 ++++++++++++++++++++++ 1 file changed, 267 insertions(+) create mode 100644 vortragKRRUpSeminar/latexImages/rules.tex diff --git a/vortragKRRUpSeminar/latexImages/rules.tex b/vortragKRRUpSeminar/latexImages/rules.tex new file mode 100644 index 0000000..74af7b2 --- /dev/null +++ b/vortragKRRUpSeminar/latexImages/rules.tex @@ -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}