Add Abstract and Termination

aspUnify.tex

@@ -2,8 +2,9 @@
 % LLNCS macro package for Springer Computer Science proceedings;
 % Version 2.21 of 2022/01/12
 %
-\documentclass[runningheads]{llncs}
+\documentclass[submission]{eptcs}
-%
+\providecommand{\event}{Symposium in honor of Peter Thiemann's 60th birthday} % Name of the event you are submitting to
+\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.
@@ -23,39 +24,48 @@
 \usepackage{mathpartir}
 \usepackage{amsmath}
 \usepackage{amssymb}
+\usepackage{amsthm}
 \usepackage{enumitem}
 %\usepackage{amsthm}
 
+
+\newtheorem{theorem}{Theorem}
+\newtheorem{lemma}[theorem]{Lemma}
+
+\title{Global Type Inference for Java using SAT Solvers}
+\author{Andreas Stadelmeier
+    \institute{DHBW\\ Stuttgart}
+    \email{a.stadelmeier@hb.dhbw-stuttgart.de}
+}
+\newcommand{\authorrunning}{Andreas Stadelmeier}
+\newcommand{\titlerunning}{Type Unification to SAT}
+\hypersetup{
+  bookmarksnumbered,
+  pdftitle    = {\titlerunning},
+  pdfauthor   = {\authorrunning},
+  pdfsubject  = {Global Type Inference for Java},               % Consider adding a more appropriate subject or description
+  pdfkeywords = {typeinference, java, sat solving, answer set programming} % Uncomment and enter keywords specific to your paper
+}
+
 \begin{document}
 %
-\title{Global Type Inference for Java using SAT Solvers}
-%
-%\titlerunning{Abbreviated paper title}
-% If the paper title is too long for the running head, you can set
-% an abbreviated paper title here
-%
-\author{First Author\inst{1}\orcidID{0000-1111-2222-3333} \and
-Second Author\inst{2,3}\orcidID{1111-2222-3333-4444} \and
-Third Author\inst{3}\orcidID{2222--3333-4444-5555}}
-%
-\authorrunning{F. Author et al.}
 % First names are abbreviated in the running head.
 % If there are more than two authors, 'et al.' is used.
 %
-\institute{Princeton University, Princeton NJ 08544, USA \and
-Springer Heidelberg, Tiergartenstr. 17, 69121 Heidelberg, Germany
-\email{lncs@springer.com}\\
-\url{http://www.springer.com/gp/computer-science/lncs} \and
-ABC Institute, Rupert-Karls-University Heidelberg, Heidelberg, Germany\\
-\email{\{abc,lncs\}@uni-heidelberg.de}}
 %
 \maketitle              % typeset the header of the contribution
 %
 \begin{abstract}
-The abstract should briefly summarize the contents of the paper in
+Global type inference for Java is able to compute correct types for an input program
-150--250 words.
+which has no type annotations at all.
+Global type inference for Featherweigt Generic Java is NP-hard.
+Former implementations of the algorithm struggled with bad runtime performance.
+In this paper we translated the type inference algorithm for Featherweight Generic Java to an
+Answer Set Program.
+Answer Set Programming (ASP) promises to solve complex computational search problems
+as long as they are finite domain.
 
-\keywords{First keyword  \and Second keyword \and Another keyword.}
+%TODO: Is this correct?
 \end{abstract}
 %
 %
@@ -117,6 +127,7 @@ The need to have an upper bound to every type placeholder.
 
 We have to formulate the unification algorithm with implication rules.
 Those can be directly translated to ASP.
+\label{sec:implicationRules}
 \begin{mathpar}
 \inferrule[Subst]{
     \tv{a} \doteq \type{N}
@@ -297,7 +308,7 @@ Fail:
 }
 \and
 \inferrule[Fail-Sigma]{
-    \tv{a} \doteq \type{N} \\
+    \tv{a} \mapsto \type{N} \\
     \tv{a} \in \type{N}
 }{
     \emptyset
@@ -326,10 +337,22 @@ Fail:
 The algorithm terminates if every type placeholder in the input constraint set has an assigned type.
 
 \section{ASP Encoding}
+The implication rules defined in chapter \ref{sec:implicationRules} can be translated to an ASP program.
+
 \begin{tabular}{l | r}
 $\exptype{C}{\ol{X}}$ & \texttt{type("C", paramX)}\\
 \end{tabular}
 
+\section{Termination}
+The amount of different constraints is limited by the maximum amount of encapsulated generics.
+The only part that is able to add an additional nesting is the Subst-Param rule.
+Here a type placeholder inside a type parameter list is replaced by another type which possibly adds
+another layer of nesting but it also removes one type placeholder.
+
+There must be one substitution that does not add another type placeholder.
+Otherwise there has to be a loop and this woul lead to an incorrect constraint set due to the Fail-Sigma rule.
+
+
 \section{Completeness}
 To proof completeness we have to show that every type can be replaced by a placeholder in a correct constraint set.
 
@@ -451,4 +474,7 @@ and every type placeholder has an upper bound $\tv{a} \lessdot \type{N}$.
   And more text.
 \end{proof}
 
+\bibliographystyle{eptcs}
+\bibliography{martin}
+
 \end{document}

eptcs.cls

@@ -0,0 +1,263 @@
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesClass{eptcs}[2022/05/20 v1.7]
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%                             options                            %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newif\ifadraft
+\newif\ifsubmission
+\newif\ifpreliminary
+\newif\ifcopyright
+\newif\ifpublicdomain
+\newif\ifcreativecommons
+\newif\ifnoderivs
+\newif\ifsharealike
+\newif\ifnoncommercial
+\adraftfalse
+\submissionfalse
+\preliminaryfalse
+\copyrightfalse
+\publicdomainfalse
+\creativecommonsfalse
+\noderivsfalse
+\sharealikefalse
+\noncommercialfalse
+\DeclareOption{adraft}{\adrafttrue}
+\DeclareOption{submission}{\submissiontrue}
+\DeclareOption{preliminary}{\preliminarytrue}
+\DeclareOption{copyright}{\copyrighttrue}
+\DeclareOption{publicdomain}{\publicdomaintrue}
+\DeclareOption{creativecommons}{\creativecommonstrue}
+\DeclareOption{noderivs}{\noderivstrue}
+\DeclareOption{noncommercial}{\noncommercialtrue}
+\DeclareOption{sharealike}{\sharealiketrue}
+\ProcessOptions\relax
+
+\LoadClass[letterpaper,11pt,twoside]{article}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%   On US letter paper the margins (left-top-right-bottom) are       %%
+%%              2.795cm - 1.23cm - 2.795cm - 3.46cm                   %%
+%%   Note: When \topmargin would be 0, the real top margin would be   %%
+%%   (72-25-12=35pt) + 1pt (unused portion of head) = .5in = 1.27cm.  %%
+%%   The bottom margin is   11in - 1in + 0.04cm - 623/72in = 3.46cm.  %%
+%%   On the first page the bottom margin contains various footers.    %%
+%%   When translating from US letter to A4 paper, without scaling, by %%
+%%   leaving the centre of the paper invariant (as is possible when   %%
+%%   printing the paper with acroread), the resulting A4 margins are  %%
+%%                2.5cm - 2.11cm - 2.5cm - 4.34cm                     %%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\textwidth              16cm             % A4 width is 21cm            %
+\textheight             623.01pt         % 46 lines exactly = 21.98cm  %
+\oddsidemargin          -0.04cm          % +1 inch = 2.5cm             %
+\evensidemargin         -0.04cm          % +1 inch = 2.5cm             %
+\topmargin              -0.04cm          % +1 inch = 2.5cm             %
+\advance\topmargin-\headheight           % 12pt                        %
+\advance\topmargin-\headsep              % 25pt                        %
+\marginparwidth          45pt            % leaves 15pt from A4 edge    %
+\advance\evensidemargin  .295cm          % centre w.r.t. letter paper  %
+\advance\oddsidemargin   .295cm          % centre w.r.t. letter paper  %
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%                  load eptcsdata when available                 %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\IfFileExists{eptcsdata.tex}{\input{eptcsdata}}{}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%			Pagestyle and titlepage      		    %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\pagestyle{myheadings}
+\renewcommand\pagestyle[1]{}             % ignore further \pagestyles
+
+\renewcommand\maketitle{\par
+  \begingroup
+    \providecommand{\event}{}
+    \ifadraft
+      \providecommand{\publicationstatus}{\Large DRAFT\quad\today}
+    \else\ifsubmission
+      \providecommand{\publicationstatus}{Submitted to:\\
+      \event}
+    \else\ifpreliminary
+      \providecommand{\publicationstatus}{Preliminary Report. Final version to appear in:\\
+      \event}
+    \else
+      \providecommand{\publicationstatus}{To appear in EPTCS.}
+    \fi\fi\fi
+    \providecommand{\titlerunning}{Please define {\ttfamily $\backslash$titlerunning}}
+    \providecommand{\authorrunning}{Please define {\ttfamily $\backslash$authorrunning}}
+    \providecommand{\copyrightholders}{\authorrunning}
+    \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
+    \def\@makefnmark{\rlap{\@textsuperscript{\normalfont\@thefnmark}}}%
+    \long\def\@makefntext##1{\parindent 1em\noindent
+            \hb@xt@1.8em{%
+                \hss\@textsuperscript{\normalfont\@thefnmark}}##1}%
+    \newpage
+    \global\@topnum\z@   % Prevents figures from going at top of page.
+    \@maketitle
+    \thispagestyle{empty}\@thanks
+  \endgroup
+  \setcounter{footnote}{0}%
+  \label{FirstPage}
+  \global\let\thanks\relax
+  \global\let\maketitle\relax
+  \global\let\@maketitle\relax
+  \global\let\@thanks\@empty
+  \global\let\@author\@empty
+  \global\let\@date\@empty
+  \global\let\@title\@empty
+  \global\let\title\relax
+  \global\let\author\relax
+  \global\let\date\relax
+  \global\let\and\relax
+}
+\def\@maketitle{%                       adapted from article.cls
+  \newpage
+\noindent
+\raisebox{-22.8cm}[0pt][0pt]{\footnotesize
+\begin{tabular}{@{}l}
+\publicationstatus
+\end{tabular}}
+\hfill\vspace{-1em}
+\raisebox{-22.8cm}[0pt][0pt]{\footnotesize
+\makebox[0pt][r]{
+\begin{tabular}{l@{}}
+\ifpublicdomain
+  This work is \href{https://creativecommons.org/publicdomain/zero/1.0/}
+  {dedicated to the public domain}.
+\else
+  \ifcopyright
+    \copyright~\copyrightholders\\
+  \fi
+  \ifcreativecommons
+    This work is licensed under the
+    \ifnoncommercial
+      \href{https://creativecommons.org}{Creative Commons}\\
+      \ifnoderivs
+	\href{https://creativecommons.org/licenses/by-nc-nd/4.0/}
+	{Attribution-Noncommercial-No Derivative Works} License.
+      \else\ifsharealike
+	\href{https://creativecommons.org/licenses/by-nc-sa/4.0/}
+	{Attribution-Noncommercial-Share Alike} License.
+      \else
+	\href{https://creativecommons.org/licenses/by-nc/4.0/}
+	{Attribution-Noncommercial} License.
+      \fi\fi
+    \else
+      \ifnoderivs
+        \href{https://creativecommons.org}{Creative Commons}\\
+	\href{https://creativecommons.org/licenses/by-nd/4.0/}
+	{Attribution-No Derivative Works} License.
+      \else\ifsharealike
+        \href{https://creativecommons.org}{Creative Commons}\\
+	\href{https://creativecommons.org/licenses/by-sa/4.0/}
+	{Attribution-Share Alike} License.
+      \else
+        \\\href{https://creativecommons.org}{Creative Commons}
+	\href{https://creativecommons.org/licenses/by/4.0/}
+	{Attribution} License.
+      \fi\fi
+    \fi
+  \fi
+\fi
+\end{tabular}}}
+  \null
+  %\vskip 2em%				a bit of space removed (< 2em)
+  \begin{center}%
+  \let \footnote \thanks
+    {\LARGE\bfseries \@title \par}%		\bf added
+    \vskip 2em%				was: 1.5em
+    {\large
+      \lineskip .5em%
+      \begin{tabular}[t]{c}%
+        \@author
+      \end{tabular}\par}%
+    \vskip 1em%			       \date and extra space removed
+  \end{center}%
+  \par
+  \markboth{\hfill\titlerunning}{\authorrunning\hfill}
+  \vskip .5em}
+
+\AtBeginDocument{
+  \providecommand{\firstpage}{1}
+  \setcounter{firstpage}{\firstpage}
+  \setcounter{page}{\firstpage}
+  \@ifpackageloaded{array}% Contributed by Wolfgang Jeltsch
+    {\newcommand{\IfArrayPackageLoaded}[2]{#1}}
+    {\newcommand{\IfArrayPackageLoaded}[2]{#2}}}
+\newcommand{\institute}[1]{\IfArrayPackageLoaded
+    {\\{\scriptsize\begin{tabular}[t]{@{}>{\footnotesize}c@{}}#1\end{tabular}}}
+    {\\{\scriptsize\begin{tabular}[t]{@{\footnotesize}c@{}}#1\end{tabular}}}}
+\newcommand{\email}[1]{\\{\footnotesize\ttfamily #1}}
+
+\renewenvironment{abstract}{\begin{list}{}%   header removed and noindent
+			{\rightmargin\leftmargin
+			\listparindent 1.5em
+			\parsep 0pt plus 1pt}
+			\small\item}{\end{list}
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\RequirePackage{hyperref} % add hyperlinks
+\RequirePackage{mathptmx} % Pick Times Roman as a base font
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%			Remember page numbers      		    %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcounter{firstpage}
+\setcounter{firstpage}{1}
+\AtEndDocument{\clearpage
+   \addtocounter{page}{-1}
+   \immediate\write\@auxout{\string
+   \newlabel{LastPage}{{}{\thepage}{}{page.\thepage}{}}}%
+   \newwrite\pages
+   \immediate\openout\pages=\jobname.pag
+   \immediate\write\pages{\arabic{firstpage}-\arabic{page}}
+   \addtocounter{page}{1}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%			Less space in lists      		    %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\def\@listi{\leftmargin\leftmargini
+            \parsep 2.5\p@ \@plus1.5\p@ \@minus\p@
+            \topsep 5\p@   \@plus2\p@ \@minus5\p@
+            \itemsep2.5\p@ \@plus1.5\p@ \@minus\p@}
+\let\@listI\@listi
+\@listi
+\def\@listii {\leftmargin\leftmarginii
+              \labelwidth\leftmarginii
+              \advance\labelwidth-\labelsep
+              \topsep    1\p@ \@plus\p@ \@minus\p@
+              \parsep    1\p@   \@plus\p@  \@minus\p@
+              \itemsep   \parsep}
+\def\@listiii{\leftmargin\leftmarginiii
+              \labelwidth\leftmarginiii
+              \advance\labelwidth-\labelsep
+              \topsep    \z@
+              \parsep    \z@
+              \itemsep   \topsep}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%       References small and with less space between items       %%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\renewenvironment{thebibliography}[1]
+     {\section*{\refname}\small%              small added
+      \list{\@biblabel{\@arabic\c@enumiv}}%
+           {\settowidth\labelwidth{\@biblabel{#1}}%
+            \leftmargin\labelwidth
+            \advance\leftmargin\labelsep
+            \@openbib@code
+            \usecounter{enumiv}%
+            \let\p@enumiv\@empty
+            \renewcommand\theenumiv{\@arabic\c@enumiv}}%
+      \sloppy
+      \clubpenalty4000
+      \@clubpenalty \clubpenalty
+      \widowpenalty4000%
+      \sfcode`\.\@m
+		\setlength{\parskip}{0pt}%
+		\setlength{\itemsep}{3pt plus 2pt}% less space between items
+     }
+     {\def\@noitemerr
+       {\@latex@warning{Empty `thebibliography' environment}}%
+      \endlist}

prolog.tex

@@ -22,8 +22,6 @@
   backgroundcolor=\color{red!20}
 }
 
-\newtheorem{recap}[note]{Recap}
-
 \newcommand{\rulenameAfter}[1]{\begin{array}[b]{l}\rulename{#1}\\[-1em] \ \end{array}}
 
 \newcommand{\tifj}{\texttt{TamedFJ}}