From 28e3f553ea39aba6629ed5570bd405b2b920486e Mon Sep 17 00:00:00 2001 From: Cynthia Kop Date: Mon, 5 Jan 2026 22:59:19 +0100 Subject: [PATCH] Wrote up an explanation for the higher-order formalism --- lmcs.cls | 506 +++++++++++++++++++++++++++++++++++++ stcrs.bib | 75 ++++++ stcrs.tex | 734 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 1315 insertions(+) create mode 100644 lmcs.cls create mode 100644 stcrs.bib create mode 100644 stcrs.tex diff --git a/lmcs.cls b/lmcs.cls new file mode 100644 index 0000000..fb3c121 --- /dev/null +++ b/lmcs.cls @@ -0,0 +1,506 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Modification log +%% +%% 2004/03/25 v0.1 based on amsart.cls, inspired by jair.sty +%% 2004/09/01 v0.2 based on amsart.cls +%% 2004/10/12 v0.3 based on amsart.cls +%% 2004/12/16 v0.4 based on amsart.cls +%% 2005/01/24 v0.5 based on amsart.cls +%% 2005/03/10 v0.6 based on amsart.cls +%% 2006/07/24 v0.7 based on amsart.cls +%% 2007/11/13 v0.8 based on amsart.cls +%% +%% Juergen Koslowski, Stefan Milius +%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\NeedsTeXFormat{LaTeX2e} +\ProvidesClass{lmcs} + [2009/05/25 v0.8 LMCS Layout Editor Class] +\DeclareOption*{\PassOptionsToClass{\CurrentOption}{amsart}} +\ProcessOptions\relax + +\LoadClass[11pt,reqno]{amsart} +\usepackage{helvet,cclicenses} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Use of this class, cf. also lmcs-smp.tex +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% This class builds upon the amsart class of AMS-LaTeX and requires use +% of LaTeX 2e. +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Start of the paper +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% \documentclass{lmcs} +% +% without any options followed optionally by +% +% \usepackage{package1,package2,...} +% +% loading additional macro packages you may wish to use, (eg, xypic, etc.) +% (This also is the place to define further theorem-environments, in case +% those provided by default do not suffice, cf. below.) +% +% \begin{document} +% \title[short_title]{real title} +% +% and a list of author information of the form +% +% \author[short_author1]{Author 1} +% \address{address 1} +% \email{author1@email1} +% \thanks{thanks 1} +% +% \author[short_author2]{Author 2} +% \address{address 2} +% \email{author2@email2} +% \thanks{thanks 2} +% +% \author[short_author3]{Author 3} +% \address{address 3} +% \email{author3@email3} +% \thanks{thanks 3} +% +% The \email and \thanks fields are optional. The \thanks fields appear +% in footnotes on the title page, the addresses and email information +% is relegated to the end of the article. The optional arguments to +% the \title and \author macros determine a running head on the odd +% and even pages, respectively. +% +% Lists of keywords and phrases as well as an ACM Subject +% classification are mandatory; these appear in footnotes on the +% title page, preceeding any \thanks fields. +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Body of the paper +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% We encourage the use of LaTeX's crossreferencing capabilities with the +% \label and \ref commands, for sections, subsections, theorems etc., and +% displayed equations and figures. +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Theorems, Definitions etc. +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% The following theorem-like environments are available. The +% numbering is consecutive within sections. +% +% thm Theorem +% cor Corollary +% lem Lemma +% prop Proposition +% asm Asumption +% +% defi Definition +% rem Remark +% rems Remarks (intended for use with itemized remarks) +% exa Example +% exas Examples (intended for use with itemized examples) +% conj Conjecture +% prob Problem +% oprob Open Problem +% algo Algorithm +% obs Observation +% +% If you require additional environments, you can add them before +% \begin{document} by means of +% +% \theoremstyle{plain}\newtheorem{env}[thm]{Environment} +% +% or +% +% \theoremstyle{definition}\newtheorem{env}[thm]{Environment} +% +% In the first case the font within the new environment will be italicised. +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Proofs +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Proofs start with the command \proof and should be ended by \qed, +% which provides an end-of-proof box at the right margin: +% +% \proof ... \qed +% +% In itemized or enumerated proofs the \qed command has to occur BEFORE +% \end{itemize} or \end{enumerate} to ensure proper placement of the box: +% +% \proof +% \begin{itemize} +% \item[(1)] ... +% \item[(2)] ... +% ... +% \item[(n)] ... \qed +% \end{itemize} +% +% Similarly, the box may be used within theorem environments, when no +% explicit proof is given: +% +% \begin{thm} ... \qed \end{thm} +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Itemized or enumerated environments and proofs +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% By default, the first item of an itemized (or enumerated) environment +% or proof appears inlined on the same line as the environment title. +% This can be prevented by placing \hfill before the itemization, e.g.: +% +% \begin{thm}\label{T:abc}\hfill +% \begin{itemize} ... +% +% \proof\hfill +% \begin{itemize} ... + + +% +% End of the paper +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Acknowledgements should be placed in a non-numbered section: +% +% \section*{Acknowledgement} +% +% The bibliography uses alpha.bst where references are built from the +% authors' initials and the year of publication. The use of bibtex +% for creating the bibliography is strongly encouraged. Then the +% end of the paper takes the form +% +% \begin{thebibliography}{key} +% \end{thebibliography} +% \end{document} +% +% where ``key'' is the longest alphanumerical key expected to occur. +% +% Optionally, appendices can be inserted after the bibliography by +% means of +% +% \end{thebibliography} +% \appendix +% \section{} % Appendix A +% \section{} % Appendix B +% % etc. +% \end{document} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%% actual macros +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\count255=\the\catcode`\@ \catcode`\@=11 \edef\catc@de{\the\count255} + +\newif\ifsuPer \suPertrue +\def\rsuper#1{\ifsuPer${\,}^{\MakeLowercase #1}$\fi}% +\def\lsuper#1{\ \hskip-2 pt\ifsuPer\llap{${}^{\MakeLowercase #1}\ $\fi}}% + +\def\titlecomment#1{\def\@titlecomment{#1}} +\let\@titlecomment=\@empty +\renewcommand{\sfdefault}{phv} +\renewcommand*\subjclass[2][1991]{% + \def\@subjclass{#2}% + \@ifundefined{subjclassname@#1}{% + \ClassWarning{\@classname}{Unknown edition (#1) of ACM + Subject Classification; using '1991'.}% + }{% + \@xp\let\@xp\subjclassname\csname subjclassname@1998\endcsname + }% +} +\@namedef{subjclassname@1998}{1998 ACM Subject Classification} +\newcommand{\revisionname}{Revision Note} +\newbox\revisionbox +\newenvironment{revision}{% + \ifx\maketitle\relax + \ClassWarning{\@classname}{Revision should precede + \protect\maketitle\space in LMCS documentclasses; reported}% + \fi + \global\setbox\revisionbox=\vtop \bgroup + \normalfont\Small + \list{}{\labelwidth\z@ + \leftmargin3pc \rightmargin\leftmargin + \listparindent\normalparindent \itemindent\z@ + \parsep\z@ \@plus\p@ + \let\fullwidthdisplay\relax + }% + \item[\hskip\labelsep\scshape\revisionname.]% +}{% + \endlist\egroup + \ifx\@setrevision\relax \@setrevisiona \fi +} +\def\@setrevision{\@setrevisiona \global\let\@setrevision\relax} +\def\@setrevisiona{% + \ifvoid\revisionbox + \else + \skip@20\p@ \advance\skip@-\lastskip + \advance\skip@-\baselineskip \vskip\skip@ + \box\revisionbox + \prevdepth\z@ % because \revisionbox is a vtop + \bigskip\hrule\medskip + \fi +} +\def\@setsubjclass{% + {\itshape\subjclassname:}\enspace\@subjclass\@addpunct.} +\def\@setkeywords{% + {\itshape \keywordsname:}\enspace \@keywords\@addpunct.} +\def\@settitlecomment{\@titlecomment\@addpunct.} +\def\@maketitle{% + \normalfont\normalsize + \let\@makefnmark\relax \let\@thefnmark\relax + \ifx\@empty\@date\else \@footnotetext{\@setdate}\fi + \ifx\@empty\@subjclass\else \@footnotetext{\@setsubjclass}\fi + \ifx\@empty\@keywords\else \@footnotetext{\@setkeywords}\fi + \ifx\@empty\@titlecomment\else \@footnotetext{\@settitlecomment}\fi + \ifx\@empty\thankses\else \@footnotetext{% + \def\par{\let\par\@par}\@setthanks\par}\fi + \@mkboth{\@nx\shortauthors}{\@nx\shorttitle}% + \global\topskip12\p@\relax % 5.5pc " " " " " + \topskip42 pt\@settitle + \ifx\@empty\authors \else \@setauthors \fi + \@setaddresses + \ifx\@empty\@dedicatory + \else + \baselineskip18\p@ + \vtop{\centering{\footnotesize\itshape\@dedicatory\@@par}% + \global\dimen@i\prevdepth}\prevdepth\dimen@i + \fi + \endfront@text + \bigskip\hrule\medskip + \@setrevision + \@setabstract + \vskip-\bigskipamount + \normalsize + \if@titlepage + \newpage + \else + \dimen@34\p@ \advance\dimen@-\baselineskip + \vskip\dimen@\relax + \fi +} +\def\@setaddresses{\par + \nobreak \begingroup +\footnotesize + \def\author##1{\nobreak\addvspace\bigskipamount}% + \def\\{\unskip, \ignorespaces}% + \interlinepenalty\@M + \def\address##1##2{\begingroup + \par\addvspace\bigskipamount\noindent\narrower + \@ifnotempty{##1}{(\ignorespaces##1\unskip) }% + {\ignorespaces##2}\par\endgroup}% + \def\curraddr##1##2{\begingroup + \@ifnotempty{##2}{\nobreak\indent{\itshape Current address}% + \@ifnotempty{##1}{, \ignorespaces##1\unskip}\/:\space + ##2\par}\endgroup}% + \def\email##1##2{\begingroup + \@ifnotempty{##2}{\nobreak\indent{\itshape e-mail address}% + \@ifnotempty{##1}{, \ignorespaces##1\unskip}\/:\space + {##2}\par}\endgroup}% + \def\urladdr##1##2{\begingroup + \@ifnotempty{##2}{\nobreak\indent{\itshape URL}% + \@ifnotempty{##1}{, \ignorespaces##1\unskip}\/:\space + \ttfamily##2\par}\endgroup}% + \addresses + \endgroup +} +\copyrightinfo{}{} + +\newinsert\copyins +\skip\copyins=3pc +\count\copyins=1000 % magnification factor, 1000 = 100% +\dimen\copyins=.5\textheight % maximum allowed per page + +\renewcommand{\topfraction}{0.95} % let figure take up nearly whole page +\renewcommand{\textfraction}{0.05} % let figure take up nearly whole page + +%% Specify the dimensions of each page + +\setlength{\oddsidemargin}{.25 in} % Note \oddsidemargin = \evensidemargin +\setlength{\evensidemargin}{.25 in} +\setlength{\marginparwidth}{0.07 true in} +\setlength{\topmargin}{-0.7 in} +\addtolength{\headheight}{1.84 pt} +\addtolength{\headsep}{0.25in} +\addtolength{\voffset}{0.7 in} +\setlength{\textheight}{8.5 true in} % Height of text (including footnotes & figures) +\setlength{\textwidth}{6.0 true in} % Width of text line. +\setlength{\parindent}{20 pt} % Width of text line. +\widowpenalty=10000 +\clubpenalty=10000 +\@twosidetrue \@mparswitchtrue \def\ds@draft{\overfullrule 5pt} +\raggedbottom + +%% Pagestyle + +%% Defines the pagestyle for the title page. +%% Usage: \lmcsheading{vol}{issue}{year}{pages}{subm}{publ}{rev}{spec_iss}{title} + +\def\lmcsheading#1#2#3#4#5#6#7{\def\ps@firstpage{\let\@mkboth\@gobbletwo% +\def\@oddhead{% +\hbox{% + \vbox to 30 pt{\scriptsize\vfill + \hbox{\textsf{Logical Methods in Computer Science}\hfil} + \hbox{\textsf{Vol.~? (?:?) 2???, ? pages}} + \hbox{\textsf{www.lmcs-online.org}} + \rlap{\vrule width\hsize depth .4 pt}}}\hfill +\raise 4pt +\hbox{% + \vbox to 30 pt{\scriptsize\vfill + \hbox{\textsf{}} + \hbox{\textsf{}}}}\hfill +\raise 4pt +\hbox{% + \vbox to 30 pt{\scriptsize\vfill + \hbox to 94 pt{\textsf{Submitted\hfill date}} + \hbox to 94 pt{\textsf{Published\hfill date}} + }}} +\def\@evenhead{}\def\@evenfoot{}}% +\thispagestyle{firstpage}} + +\def\endfront@text{% + \insert\copyins{\hsize\textwidth + \fontsize{6}{7\p@}\normalfont\upshape + \noindent +%\hfill\textsf{DOI:10.2168/LMCS-???} +%\hfill\textsf{\copyright\shortauthors} +\hfill +\hbox{ + \vbox{\fontsize{6}{8 pt}\baselineskip=6 pt\vss + \hbox{\textsf{\,\,\copyright\quad \shortauthors}\hfil} + \hbox{\textsf{Creative Commons}\hfil}}} +\par\kern\z@}% +} +%\def\endfront@text{} + +\def\enddoc@text{} + +%% Defines the pagestyle for the rest of the pages +%% Usage: \ShortHeadings{Minimizing Conflicts}{Minton et al} +%% \ShortHeadings{short title}{short authors} + +%\def\firstpageno#1{\setcounter{page}{#1}} +%\def\ShortHeadings#1#2{\def\ps@lmcsps{\let\@mkboth\@gobbletwo% +%\def\@oddhead{\hfill {\small\sc #1} \hfill}% +%\def\@oddfoot{\hfill \small\rm \thepage \hfill}% +%\def\@evenhead{\hfill {\small\sc #2} \hfill}% +%\def\@evenfoot{\hfill \small\rm \thepage \hfill}}% +%\pagestyle{lmcsps}} + +%% MISCELLANY + +\def\@startsection#1#2#3#4#5#6{\bigskip% + \if@noskipsec \leavevmode \fi + \par \@tempskipa #4\relax + \@afterindentfalse + \ifdim \@tempskipa <\z@ \@tempskipa -\@tempskipa \@afterindentfalse\fi + \if@nobreak \everypar{}\else + \addpenalty\@secpenalty\addvspace\@tempskipa\fi + \@ifstar{\@dblarg{\@sect{#1}{\@m}{#3}{#4}{#5}{#6}}}% + {\@dblarg{\@sect{#1}{#2}{#3}{#4}{#5}{#6}}}% +} + +\def\figurecaption#1#2{\noindent\hangindent 40pt + \hbox to 36pt {\small\sl #1 \hfil} + \ignorespaces {\small #2}} +% Figurecenter prints the caption title centered. +\def\figurecenter#1#2{\centerline{{\sl #1} #2}} +\def\figurecenter#1#2{\centerline{{\small\sl #1} {\small #2}}} + +% +% Allow ``hanging indents'' in long captions +% +\long\def\@makecaption#1#2{ + \vskip 10pt + \setbox\@tempboxa\hbox{#1: #2} + \ifdim \wd\@tempboxa >\hsize % IF longer than one line: + \begin{list}{#1:}{ + \settowidth{\labelwidth}{#1:} + \setlength{\leftmargin}{\labelwidth} + \addtolength{\leftmargin}{\labelsep} + }\item #2 \end{list}\par % Output in quote mode + \else % ELSE center. + \hbox to\hsize{\hfil\box\@tempboxa\hfil} + \fi} + + +% Define strut macros for skipping spaces above and below text in a +% tabular environment. +\def\abovestrut#1{\rule[0in]{0in}{#1}\ignorespaces} +\def\belowstrut#1{\rule[-#1]{0in}{#1}\ignorespaces} + +%%% Theorem environments + +% the following environments switch to a slanted font: +\theoremstyle{plain} + +\newtheorem{thm}{Theorem}[section] +\newtheorem{cor}[thm]{Corollary} +\newtheorem{lem}[thm]{Lemma} +\newtheorem{prop}[thm]{Proposition} +\newtheorem{asm}[thm]{Assumption} + +% the following environments keep the roman font: +\theoremstyle{definition} + +\newtheorem{rem}[thm]{Remark} +\newtheorem{rems}[thm]{Remarks} +\newtheorem{exa}[thm]{Example} +\newtheorem{exas}[thm]{Examples} +\newtheorem{defi}[thm]{Definition} +\newtheorem{conv}[thm]{Convention} +\newtheorem{conj}[thm]{Conjecture} +\newtheorem{prob}[thm]{Problem} +\newtheorem{oprob}[thm]{Open Problem} +\newtheorem{algo}[thm]{Algorithm} +\newtheorem{obs}[thm]{Observation} +\newtheorem{qu}[thm]{Question} +\newtheorem{fact}[thm]{Fact} +\newtheorem{pty}[thm]{Property} + +\numberwithin{equation}{section} + +% end-of-proof sign, to appear at right margin +% Paul Taylor and Chris Thompson, Cambridge, 1986 +% +\def\pushright#1{{% set up + \parfillskip=0pt % so \par doesn't push #1 to left + \widowpenalty=10000 % so we dont break the page before #1 + \displaywidowpenalty=10000 % ditto + \finalhyphendemerits=0 % TeXbook exercise 14.32 + % + % horizontal + \leavevmode % \nobreak means lines not pages + \unskip % remove previous space or glue + \nobreak % don't break lines + \hfil % ragged right if we spill over + \penalty50 % discouragement to do so + \hskip.2em % ensure some space + \null % anchor following \hfill + \hfill % push #1 to right + {#1} % the end-of-proof mark (or whatever) + % + % vertical + \par}} % build paragraph + +\def\qEd{{\lower1 pt\hbox{\vbox{\hrule\hbox{\vrule\kern4 pt + \vbox{\kern4 pt\hbox{\hss}\kern4 pt}\kern4 pt\vrule}\hrule}}}} +\def\qed{\pushright{\qEd} + \penalty-700 \par\addvspace{\medskipamount}} + +\newenvironment{Proof}[1][\proofname]{\par + \pushQED{\qed}% + \normalfont \topsep6\p@\@plus6\p@\relax + \trivlist + \item[\hskip\labelsep + \itshape + #1]\ignorespaces +}{% + \popQED\endtrivlist\@endpefalse +} +\newenvironment{iteMize}[1]{\begin{enumerate}[#1]}{\end{enumerate}} +\newenvironment{desCription}{\begin{enumerate}[\hbox to8 pt{\hfill}]}{\end{enumerate}} +% Bibliographystyle + +\bibliographystyle{alpha} + +\endinput diff --git a/stcrs.bib b/stcrs.bib new file mode 100644 index 0000000..9b3e3f0 --- /dev/null +++ b/stcrs.bib @@ -0,0 +1,75 @@ +@inproceedings{bla:00, + author = {Blanqui, F.}, + title = {Termination and Confluence of Higher-Order Rewrite Systems}, + booktitle = {Proceedings of the 11th International Conference on Rewriting + Techniques and Applications (RTA '00)}, + year = {2000}, + series = {LNCS}, + pages = {47--61}, +} + +@inproceedings{jou:rub:99, + author = {Jouannaud, J. and Rubio, A.}, + title = {The higher-order recursive path ordering}, + booktitle = {Proceedings of the 14th Annual Symposium on Logic in + Computer Science (LICS '99)}, + year = {1999}, + series = {IEEE}, + pages = {402--411}, + OPTmonth = jul, + OPTaddress = {Trento, Italy} +} + +@phdthesis{klo:80, + author = {Klop, J.W.}, + title = {{C}ombinatory {R}eduction {S}ystems}, + school = {CWI Netherlands}, + year = {1980}, +} + +@phdthesis{kop:12, + author = {Kop, C.}, + title = {Higher Order Termination}, + school = {Radboud University Nijmegen}, + year = {2012}, +} + +@article{kus:01, + author = {Kusakari, K.}, + title = {On proving termination of term rewriting systems + with higher-order variables}, + journal = {IPSJ Transactions on Programming}, + year = {2001}, + volume = {42}, + number = {SIG 7 PRO11}, + pages = {35--45}, +} + +@inproceedings{nip:91, + author = {Nipkow, T.}, + title = {Higher-order critical pairs}, + booktitle = {Proceedings of the 6th Annual IEEE Symposium on Logic in + Computer Science (LICS '91)}, + year = {1991}, + editor = {Kahn, G.}, + pages = {342--349}, + publisher = {IEEE}, + OPTmonth = {jul}, + OPTaddress = {Amsterdam, The Netherlands} +} + +@inproceedings{yam:01, + author = {Yamada, T.}, + title = {Confluence and termination + of simply typed term rewriting systems}, + booktitle = {Proceedings of the 12th International Conference + on Rewriting Techniques and Applications (RTA '01)}, + year = {2001}, + editor = {Middeldorp, A.}, + volume = {2051}, + series = {LNCS}, + pages = {338--352}, + publisher = {Springer}, + OPTaddress = {Tsukuba, Japan}, +} + diff --git a/stcrs.tex b/stcrs.tex new file mode 100644 index 0000000..cfe05a8 --- /dev/null +++ b/stcrs.tex @@ -0,0 +1,734 @@ +\documentclass{lmcs} +\pdfoutput=1 + +\usepackage{enumerate} +\usepackage[colorlinks=true]{hyperref} +\usepackage{amssymb} +\usepackage{xcolor,latexsym,amsmath,extarrows,alltt} +\usepackage{xspace} +\usepackage{booktabs} +\usepackage{mathtools} +\usepackage{enumitem} +\usepackage{stmaryrd} +\usepackage{microtype} + +\theoremstyle{theorem}\newtheorem{theorem}{Theorem} +\theoremstyle{theorem}\newtheorem{lemma}[theorem]{Lemma} +\theoremstyle{theorem}\newtheorem{corollary}[theorem]{Corollary} +\theoremstyle{definition}\newtheorem{definition}[theorem]{Definition} +\theoremstyle{definition}\newtheorem{example}[theorem]{Example} + +\newcommand{\N}{\mathbb{N}} +\newcommand{\F}{\mathcal{F}} +\newcommand{\V}{\mathcal{V}} +\newcommand{\Vmeta}{\mathcal{M}} +\newcommand{\Vfree}{\mathcal{V}_{\mathit{nonb}}} +\newcommand{\Vbound}{\mathcal{V}} +\newcommand{\Sorts}{\mathcal{S}} +\newcommand{\Types}{\mathcal{T}\!ypes} +\newcommand{\Terms}{\mathcal{T}} +\newcommand{\ATerms}{\mathcal{T}_{\mathcal{A}}} +\newcommand{\FOTerms}{\mathcal{T}_{\mathcal{FO}}} +\newcommand{\Rules}{\mathcal{R}} +\newcommand{\FV}{\mathit{FV}} +\newcommand{\FMV}{\mathit{MVar}} +\newcommand{\Positions}{\mathit{Positions}} +\newcommand{\SubPositions}{\mathit{SubPositions}} +\newcommand{\HeadPositions}{\mathit{HeadPositions}} +\newcommand{\Pairs}{\mathit{Pairs}} + +\newcommand{\domain}{\mathtt{domain}} +\newcommand{\order}{\mathit{order}} + +\newcommand{\asort}{\iota} +\newcommand{\bsort}{\kappa} +\newcommand{\atype}{\sigma} +\newcommand{\btype}{\tau} +\newcommand{\ctype}{\pi} +\newcommand{\dtype}{\alpha} +\newcommand{\identifier}[1]{\mathtt{#1}} +\newcommand{\afun}{\identifier{f}} +\newcommand{\bfun}{\identifier{g}} +\newcommand{\cfun}{\identifier{h}} +\newcommand{\avar}{x} +\newcommand{\bvar}{y} +\newcommand{\cvar}{z} +\newcommand{\Avar}{X} +\newcommand{\Bvar}{Y} +\newcommand{\Cvar}{Z} +\newcommand{\AFvar}{F} +\newcommand{\BFvar}{G} +\newcommand{\CFvar}{H} +\newcommand{\typeof}{\mathsf{typeof}} + +\newcommand{\clause}[1]{\textbf{#1}} +\newcommand{\hastype}{\ \mathtt{::}\ } + +\newcommand{\abs}[3]{\lambda #1\!:\!#2.#3} +\newcommand{\app}[2]{#1 \cdot #2} +\newcommand{\apps}[3]{#1 \cdot #2 \cdots #3} +\newcommand{\metaabs}[2]{\langle #1\rangle#2} +\newcommand{\metaabsn}[4]{\metaabs{#1_1\!:\!#2_1,\dots,#1_n\!:\!#2_{#3}}{#4}} +\newcommand{\metaabslist}[3]{\langle #1_1\!:\!#2_1,\dots,#1_n\!:\!#2_{#3} \rangle} + +\newcommand{\arity}{\mathit{ar}} +\newcommand{\head}{\mathsf{head}} +\newcommand{\arrtype}{\rightarrow} +\newcommand{\arrz}{\Rightarrow} +\newcommand{\arr}[1]{\arrz_{#1}} +\newcommand{\arrr}[1]{\arr{#1}^*} +\newcommand{\subtermeq}{\unlhd} +\newcommand{\headsubtermeq}{\unlhd_{\bullet}} +\newcommand{\supterm}{\rhd} +\newcommand{\suptermeq}{\unrhd} +\newcommand{\replace}[3]{#1_{#2:=#3}} + +\newcommand{\symb}[1]{\mathtt{#1}} + +\newcommand{\nul}{\symb{0}} +\newcommand{\one}{\symb{1}} +\newcommand{\nil}{\symb{nil}} +\newcommand{\cons}{\symb{cons}} +\newcommand{\strue}{\symb{true}} +\newcommand{\sfalse}{\symb{false}} +\newcommand{\append}{\symb{append}} +\newcommand{\suc}{\symb{s}} +\newcommand{\map}{\symb{map}} +\newcommand{\bool}{\symb{bool}} +\newcommand{\nat}{\symb{nat}} +\newcommand{\real}{\symb{real}} +\newcommand{\lijst}{\symb{list}} +\newcommand{\unitsort}{\mathtt{o}} + +\newcommand{\cora}{\textsf{CORA}\xspace} + +\newcommand{\secshort}{\S} +\newcommand{\myparagraph}[1]{\paragraph{\textbf{#1}}} + +\setlength{\parindent}{0pt} +\setlength{\parskip}{\bigskipamount} +\setlist[itemize]{topsep=-\bigskipamount} + +\newcommand{\mysubsection}[1]{\vspace{-12pt}\subsubsection{#1}} + +\begin{document} + +\title{Higher-order rewriting (union beta)} + +\maketitle + +\begin{abstract} +The following pages describe the syntax and semantics of the higher-order ARI formalism. +This format is simply-typed (without formalism) and in principle curried. Matching is +\emph{mostly} plain, though a limited form of higher-order matching modulo beta is +included for pattrens. +\end{abstract} + +\section{Syntax} + +\subsection{Grammar} +\ + +\begin{tabular}{lll} +trs & ::= & \texttt{(format higher-order)} sort+ fun+ hrule+ \\ +sort & ::= & \texttt{(sort} IDENTIFIER\texttt{)} \\ +fun & ::= & \texttt{(fun} IDENTIFIER type\texttt{)} \\ +type & ::= & IDENTIFIER $|$ \texttt{(-}$\mathtt{>}$ type+ IDENTIFIER\texttt{)} \\ +term & ::= & IDENTIFIER $|$ \texttt{(}IDENTIFIER term+\texttt{)} $|$ \texttt{(}\texttt{lambda} \texttt{(}var+\texttt{)} term\texttt{)} \\ +var & ::= & \texttt{(}IDENTIFIER type\texttt{)} \\ +rule & ::= & \texttt{(rule} term term\texttt{)} \\ +\end{tabular} + +\subsection{Restrictions} + +\begin{itemize} +\item The left- and right-hand sides of rules must have the same type. +\item All unbound variables in the right-hand side must occur in the left-hand side. +\item The left-hand side has the form \texttt{f} or (\texttt{f} l1 ... ln) with f a function symbol. +\item The left-hand side must be a \textbf{pattern}, i.e., the arguments of every applied free variable are distinct bound variables. +\item If any variable occurs applied on the left, then each occurrence in the left-hand side must have exactly the same number of + arguments, and each occurrence on the right must have \emph{at least} that number of arguments. +\end{itemize} + +\section{Semantics} + +\subsection{Types} + +We use simple types, i.e., fixing a set $\Sorts$ of sorts, the types $\Types$ of \emph{types} is generated inductively by: + +\[ \Types ::= \Sorts\, |\, \Types \arrtype \Types \] + +The arrow operator $\arrtype$ is right-associative, so all types can be denoted in a form +$\atype_1 \arrtype \dots \arrtype \atype_m \arrtype \asort$ with $\asort \in \Sorts$. +In ARI format, such a type is denoted $\mathtt{(-\!\!>\ \sigma_1\ \dots\ \sigma_n\ \asort)}$. + +\subsection{Terms} + +We fix a set $\F$ of \emph{function symbols}, also called the \emph{alphabet}; each function +symbol is equipped with a type. Notation: $(\afun \hastype \atype) \in \F$, where $\afun$ is +the name and $\atype$ the type. We also fix an infinite set $\V$ of \emph{variables}, disjoint +from the names used in $\F$. + +A \emph{type environment} is a function $\Gamma$ from a subset of $\V$ to $\Types$. +(That is, it is a set of pairs $(\avar \hastype \atype)$ such that no $\avar$ occurs more than +once.) + +\emph{Terms} are those expressions $s$ such that $\Gamma \vdash s \hastype \atype$ can be derived +for some type environment $\Gamma$ using the following clauses: + +\begin{description} +\item[constant] if $(\afun \hastype \atype) \in \F$ then $\Gamma \vdash \afun \hastype \atype$ +\item[variable] if $(\avar \hastype \atype) \in \Gamma$ then $\Gamma \vdash \avar \hastype \atype$ +\item[application] if $\Gamma \vdash s \hastype \atype \arrtype \btype$ and + $\Gamma \vdash t \hastype \atype$ then $\Gamma \vdash \app{s}{t} :: \btype$ +\item[abstraction] if $\avar \in \V$ and $\replace{\Gamma}{\avar}{\atype} \vdash t :: \btype$, then + $\Gamma \vdash \abs{\avar}{\atype}{t} :: \atype \arrtype \btype$ \\ + (Here, $\replace{\Gamma}{\avar}{\atype}$ is the function that maps $\avar$ to $\atype$ and all other + variables $\bvar$ to $\Gamma(\bvar)$.) +\end{description} + +The application operator $\cdot$ is left-associative, so every term can be written $h \cdot s_1 +\cdots s_n$ with $n \geq 0$, where $h$ is a function symbol, variable or abstraction. +In ARI format, such a term is denoted $(h\ s_1 \cdots s_n)$. +%The abstraction operator extends as far to the right as possible, so a term +%$\abs{x}{\atype}{s \cdot t \cdot q}$ should be read as $\abs{x}{\atype}{((s \cdot t) \cdot q)}$. +We also use $\lambda x_1\!:\!\sigma_1,\dots,x_n\!:\!\sigma_n.s$ to denote +$\abs{x_1}{\sigma_1}{(\lambda \dots (\abs{x_n}{\sigma_n}{s})\dots)}$. In ARI format, this is denoted +$\mathtt{(lambda\ ((}x_1\ \sigma_1\mathtt{)} \dots \mathtt{(}x_n\ \sigma_n\mathtt{))}\ s\mathtt{)}$. + +Term equality is considered modulo $\alpha$-equivalence as usual (where variable renaming does not +affect types, so for instance $\abs{\avar}{\atype}{\symb{0}} \neq \abs{\bvar}{\btype}{\symb{0}}$ if +$\atype \neq \btype$). Equality is \emph{not} considered modulo $\beta$ or $\eta$-equivalence, so +for instance $\app{(\abs{\avar}{\nat}{(\app{\symb{s}}{\avar})})}{\symb{0}}$ is distinct from +$\app{\symb{s}}{\symb{0}}$ (but \emph{is} equal to +$\app{(\abs{\bvar}{\nat}{(\app{\symb{s}}{\bvar})})}{\symb{0}}$). + +We define the set $\FV(s)$ of free variables in $s$ as usual: the set of all variables occurring in +$s$ which are not bound by a $\lambda$. + +When reasoning about terms, it is often useful to consider the ``maximally applied subterm'' +relation $\suptermeq$, defined as follows: +\begin{itemize} +\item $s \suptermeq t$ if $s = t$ or $s \supterm t$ +\item $\app{s}{u} \supterm t$ if $u \suptermeq t$ or $s \supterm t$ +\item $\abs{\avar}{\atype}{s} \supterm t$ if $u \suptermeq t$ +\end{itemize} +Note that for instance $\app{\app{\afun}{s_1}}{s_2} \supterm s_i$ but \emph{not} $\app{\app{\afun}{ +s_1}}{s_2} \supterm \app{\afun}{s_1}$: subterms at the head of an application are deliberately not +included. + +\subsection{Substitution and variable capture} + +For type environments $\Gamma,\Delta$, a \emph{substitution} is a type-preserving function from +$\Gamma$ to the set of terms typable under $\Delta$. Formally, we denote $\Gamma, \Delta \vdash +\gamma$ if $\domain(\gamma) = \domain(\Gamma)$ and $\Delta \vdash \gamma(\avar) \hastype \atype$ +for every $(\avar \hastype \atype) \in \Gamma$. + +A substitution $\gamma$ is applied to a term $s$, notation $s\gamma$, by the following procedure: +\begin{enumerate} +\item rename all bound variables in $s$ to fresh variables, i.e., distinct variables that do not + occur in $\Gamma$ or $\Delta$ +\item replace each free variable $x$ by $\gamma(x)$ +\end{enumerate} + +Formally, if $\Gamma,\Delta \vdash \gamma$ and $\Gamma \vdash s \hastype \atype$ and all bound +variables in $s$ have been renamed to be disjoint from each other and from the variables in +$\Gamma$ and $\Delta$, then $s\gamma$ is obtained by the following clauses, yielding a term such +that $\Delta \vdash s\gamma \hastype \atype$: + +\begin{itemize} +\item $\afun\gamma = \afun$ +\item $\avar\gamma = \gamma(\avar)$ if $\avar \in \domain(\gamma)$ +\item $\avar\gamma = \avar$ if $\avar \notin \domain(\gamma)$ +\item $(\app{s}{t})\gamma = \app{(s\gamma)}{(t\gamma)}$ +%\item $(\abs{\avar}{\atype}{s})\gamma = \abs{\bvar}{\atype}{(s\replace{\gamma}{\avar}{\bvar})}$ +% for $\bvar$ a \emph{fresh} variable, i.e., $\bvar$ does not occur in $\Gamma$ or $\Delta$. +\item $(\abs{\avar}{\atype}{s})\gamma = \abs{\avar}{\atype}{(s\gamma)}$; + here, due to the $\alpha$-renaming beforehand, $\avar$ does not occur in $\domain(\gamma)$ or in + $\FV(\bvar\gamma)$ for any $\bvar \in \FV(s) \setminus \{\avar\}$ +\end{itemize} + +Note that substitution is preserved under $\alpha$-renaming, i.e., if $s =_\alpha t$, and $\delta$ +is a substitution on the same domain as $\gamma$ such that each $\gamma(\avar) =_\alpha +\delta(\avar)$, then $s\gamma =_\alpha t\delta$. + +We denote $[\avar_1:=s_1,\dots,\avar_n:=s_n]$ for the substitution on domain $\{\avar_1,\dots, +\avar_n\}$ that maps each $\avar_i$ to $s_i$. + +\begin{example} +Regarding variable capture, consider the following two illustrative cases. + +\begin{itemize} +\item $(\abs{\avar}{\atype}{(\app{\afun}{\avar})})[\avar:=\symb{a}] = + \abs{\cvar}{\atype}{(\app{\afun}{\cvar})} =_\alpha + \abs{\avar}{\atype}{(\app{\afun}{\avar})}$: \\ + the bound variable $\avar$ is not replaced by $\symb{a}$, since it is bound + (and hence renamed before substituting) +\item $(\abs{\avar}{\atype}{(\app{\afun}{\bvar})})[\bvar:=\avar] = + \abs{\cvar}{\atype}{(\app{\afun}{\avar})}$: \\ + the binder is renamed, so the $\avar$ in the range of the substitution is not captured. +\end{itemize} +\end{example} + +\subsection{Rules} + +A \emph{rule} $\rho$ consists of two terms $\ell \arrz r$, such that a type environment +$\Gamma$ exists with: + +\begin{itemize} +\item both sides have the same type: both $\Gamma \vdash \ell \hastype \atype$ and $\Gamma \vdash + r \hastype \atype$ for some $\atype$ (but it is not required that $\atype$ is a sort) +\item all variables on the right also occur on the left: $\FV(r) \subseteq \FV(\ell)$ +\item the left-hand side is a functional term: $\ell$ has a form $\apps{\afun}{\ell_1}{\ell_k}$ + with $\afun \in \F$ +\item $\ell$ is a \emph{pattern}: if $\ell \suptermeq \apps{\avar}{s_1}{s_n}$ for some + $\avar \in \FV(\ell)$ then $s_1,\dots,s_n$ are distinct bound variables; that is, + $\{s_1,\dots,s_n\} \subseteq \V \setminus \FV(\ell)$ and $s_i \neq s_j$ for + $1 \leq i < j \leq n$ +\item free variables are used \emph{consistently}: there is a function $\arity$ from $\FV(\ell)$ + to $\N$ such that: + \begin{itemize} + \item if $\ell \suptermeq \apps{\avar}{\bvar_1}{\bvar_n}$ with $\avar \in \FV(\ell)$ then + $\arity(\avar) = n$ + \item if $r \suptermeq \apps{\avar}{s_1}{s_n}$ with $\avar \in \FV(\ell)$ then + $\arity(\avar) \leq n$ + \end{itemize} +\item both left- and right-hand sides are $\beta$-normal: neither has a subterm of the form + $\app{(\abs{\avar}{\atype}{s})}{t_0} \cdots t_n$ +\end{itemize} + +Note that $\Gamma$ is always uniquely defined by the restrictions on $\ell$. + +\begin{example} +A valid rule where all variables have arity $0$ is: +\[ +\app{\app{\symb{map}}{F}}{(\app{\app{\cons}{x}}{y})} \arrz +\app{\app{\cons}{(\app{F}{x})}}{(\app{\app{\symb{map}}{F}}{y})} +\] +A valid rule where $F$ has arity $1$ is: +\[ +\app{\app{\symb{map}}{(\abs{\cvar}{\nat}{(\app{F}{\cvar})})}}{(\app{\app{\cons}{x}}{y})} \arrz +\app{\app{\cons}{(\app{F}{x})}}{(\app{\app{\symb{map}}{(\abs{\cvar}{\nat}{(\app{F}{\cvar})})}}{y})} +\] +Note that these rules model \emph{essentially} the same relation. To keep the database clean, we +advise submitting only examples using the shorter form where this is possible (that is, keeping +variable arity as low as possible by eta-shortening variables), unless the choice of presentation +is actively relevant for questions of termination or confluence. + +An example of an invalid rule is the following: +\[ +\app{\symb{der}}{(\abs{\avar}{\real}{(\app{\app{\symb{plus}}{(\app{F}{\avar})}}{(\app{G}{\avar})})})} +\arrz +\abs{\avar}{\real}{\app{\app{\symb{plus}}{(\app{(\app{\symb{der}}{F})}{\avar})}}{(\app{(\app{\symb{der}}{G})}{\avar})}} +\] +This is not valid because in the right-hand side, both $F$ and $G$ occur with fewer arguments than +they have in the left-hand side. A corrected version of this rule has the same left-hand side, but +the following right-hand side: +\[ +\abs{\avar}{\real}{\app{\app{\symb{plus}}{ + (\app{(\app{\symb{der}}{(\abs{\bvar}{\nat}{(\app{F}{\bvar})})})}{\avar}) + }}{ + (\app{(\app{\symb{der}}{(\abs{\bvar}{\nat}{(\app{F}{\bvar})})})}{\avar}) + }} +\] +Note that in this rule, the left-hand side cannot be eta-shortened, so we could not avoid $F$ having +arity $1$. +\end{example} + +Due to the pattern restriction, the type of the free variables in a rule can always be deduced from +context. Hence, it suffices to give a rule without explicitly supplying $\Gamma$. + +\subsection{Rewriting} + +For a rule $\ell \arrz r$ with type environment $\Gamma$ and arity function $\arity$ from $\Gamma$ +to $\N$, a \emph{meta-substitution} to a target type environment $\Delta$ is defined as a function +$\delta$ that maps each $\avar$ with $(\avar \hastype \atype) \in \Gamma$ and $\arity(\avar) = n$ to +a construction $\metaabsn{\bvar}{\btype}{n}{t}$, where +$\{\bvar_1,\dots,\bvar_n\} \in \V \setminus (\domain(\Gamma) \cup \domain(\Delta))$, +all $\bvar_i$ are distinct, and $\Delta \cup \{\bvar_1 \hastype \btype_1,\dots,\bvar_n +\hastype\btype_n\} \vdash t \hastype \atype$. + +A meta-substitution $\delta$ is applied to $s \in \{\ell,r\}$, notation $s\delta$, by the following +procedure: +\begin{enumerate} +\item rename all bound variables that occur in $s$ to fresh variables, i.e., distinct variables + that do not occur in $\Gamma$, $\Delta$, or any of the argument lists $\metaabslist{\bvar}{ + \btype}{n}$ in the range of $\delta$ +\item replace each occurrence of $\apps{\avar}{s_1}{s_n}$ in $s$ with $\avar \in \FV(s)$ and + $n = \arity(\avar)$ by $t[\bvar_1:=s_1\delta,\dots,\bvar_n:=s_n\delta]$ if + $\delta(\avar) = \metaabsn{\bvar}{\btype}{n}{t}$; formally, this is achieved by: + \begin{itemize} + \item $(\apps{\afun}{s_1}{s_m})\delta = \apps{\afun}{(s_1\delta)}{(s_m\delta)}$ + \item $(\apps{\avar}{s_1}{s_m})\delta = \apps{\avar}{(s_1\delta)}{(s_m\delta)}$ + if $\avar \notin \domain(\delta)$ + \item $(\apps{\avar}{s_1}{s_n} \cdots s_m)\delta = + \apps{(t[\bvar_1:=s_1\delta,\dots,\bvar_n:=s_n\delta])}{(s_{n+1}\delta)}{(s_m\delta)}$ + if $\delta(\avar) = \metaabsn{\bvar}{\btype}{n}{t}$ (by the arity restriction, we always + have $0 \leq n \leq m$) + \item $(\apps{(\abs{\avar}{\atype}{t})}{s_1}{s_n})\delta = + \apps{(\abs{\avar}{\atype}{(t\delta)})}{(s_1\delta)}{(s_n\delta)}$; \\ + here, due to the $\alpha$-renaming beforehand, $x$ does not occur in $\domain(\delta)$ nor + anywhere in any $\delta(\bvar)$ + \end{itemize} +\end{enumerate} + +For a set of rules $\Rules$, the reduction relation on terms is defined by the following inductive +clauses: +\begin{itemize} +\item $\ell\delta \arr{\Rules} r\delta$ if $\ell \arrz r \in \Rules$ is a rule with type + environment $\Gamma$ and arity function $\arity$, and $\delta$ is a meta-substitution on domain + $\Gamma$ that respects $\arity$ +\item $\app{(\abs{\avar}{\atype}{s})}{t} \arr{\Rules} s[\avar:=t]$ (the $\beta$-rule) +\item $\app{s}{t} \arr{\Rules} \app{s'}{t}$ if $s \arr{\Rules} s'$ +\item $\app{s}{t'} \arr{\Rules} \app{s}{t'}$ if $t \arr{\Rules} t'$ +\item $\abs{\avar}{\atype}{s} \arr{\Rules} \abs{\avar}{\atype}{s'}$ if $s \arr{\Rules} s'$ +\end{itemize} + +Note in particular that $\beta$ is a separate rule; we do not work \emph{modulo} $\beta$ (despite +the use of meta-substitutions for matching, which creates a somewhat similar effect). + +\begin{example}\label{ex:map} +Suppose $\Rules$ contains a rule +\[ +\app{\app{\symb{map}}{F}}{(\app{\app{\cons}{x}}{y})} \arrz +\app{\app{\cons}{(\app{F}{x})}}{(\app{\app{\symb{map}}{F}}{y})} +\] +We have that $\app{\app{\symb{map}}{\textcolor{red}{(\app{\symb{plus}}{(\app{\suc}{\nul})})}}}{(\app{\app{\cons}{\textcolor{blue}{\nul}}}{\textcolor{green}{\nil}})}$ +reduces at the root to +\[\app{\app{\cons}{(\app{\textcolor{red}{\app{\symb{plus}}{(\app{\suc}{\nul})}}}{\textcolor{blue}{\nul}})}}{(\app{\app{\symb{map}}{\textcolor{red}{(\app{\symb{plus}}{(\app{\suc}{\nul})})}}}{\textcolor{green}{\nil}})}\] +using the meta-substitution $[F:=\metaabs{}{\textcolor{red}{\app{\symb{plus}}{(\app{\suc}{\nul})}}},x:=\metaabs{}{\textcolor{blue}{\nul}},t:=\metaabs{}{\textcolor{green}{\nil}]}$. + +Also, $\app{ + \app{ + \symb{map} + }{ + \textcolor{red}{(\abs{\avar}{\nat}{ + \app{\app{ + \symb{plus} + }{ + (\app{\suc}{\nul}) + }}{ + \avar + } + })} + } + }{ + (\app{\app{\cons}{\textcolor{blue}{\nul}}}{\textcolor{green}{\nil}}) + }$ +reduces at the root to +\[ + \app{ + \app{ + \cons + }{( + \app{ + \textcolor{red}{ + (\abs{\avar}{\nat}{ + \app{\app{ + \symb{plus} + }{ + (\app{\suc}{\nul}) + }}{ + \avar + } + }) + } + }{ + \textcolor{blue}{\nul} + } + )} + }{ + (\app{ + \app{ + \symb{map} + }{ + \textcolor{red}{ + (\abs{\avar}{\nat}{ + \app{\app{ + \symb{plus} + }{ + (\app{\suc}{\nul}) + }}{ + \avar + } + }) + } + } + }{ + \textcolor{green}{\nil} + }) + } +\] +using the meta-substitution $[F:=\metaabs{}{\textcolor{red}{\abs{\avar}{\nat}{\app{\app{\symb{plus}}{(\app{\suc}{\nul})}}{\avar}}}}, + x:=\metaabs{}{\textcolor{blue}{\nul}},t:=\metaabs{}{\textcolor{green}{\nil}]}$. +This in turn reduces by a $\arr{\beta}$ step to: +\[ + \app{ + \app{ + \cons + }{( + \app{ + \textcolor{red}{ + \app{ + \symb{plus} + }{ + (\app{\suc}{\nul}) + } + } + }{ + \textcolor{blue}{\nul} + } + )} + }{ + (\app{ + \app{ + \symb{map} + }{ + \textcolor{red}{ + (\abs{\avar}{\nat}{ + \app{\app{ + \symb{plus} + }{ + (\app{\suc}{\nul}) + }}{ + \avar + } + }) + } + } + }{ + \textcolor{green}{\nil} + }) + } +\] +\end{example} + +\begin{example} +In the above example, all variables have arity $0$. Now suppose $\Rules$ instead contains a rule +where $F$ has arity $1$: +\[ +\app{\app{\symb{map}}{(\abs{\cvar}{\nat}{(\app{F}{\cvar})})}}{(\app{\app{\cons}{x}}{y})} \arrz +\app{\app{\cons}{(\app{F}{x})}}{(\app{\app{\symb{map}}{(\abs{\cvar}{\nat}{(\app{F}{\cvar})})}}{y})} +\] +In this case, $\app{\app{\symb{map}}{\textcolor{red}{(\app{\symb{plus}}{(\app{\suc}{\nul})})}}}{(\app{\app{\cons}{\textcolor{blue}{\nul}}}{\textcolor{green}{\nil}})}$ +\emph{does not reduce}, since every instance of the left-hand side has a $\lambda$-abstraction as the first argument of $\map$. + +On the other hand, +$\app{ + \app{ + \symb{map} + }{ + (\abs{\avar}{\nat}{ + \app{\textcolor{red}{\app{ + \symb{plus} + }{ + (\app{\suc}{\nul}) + }}}{ + \avar + } + }) + } +}{ + (\app{\app{\cons}{\textcolor{blue}{\nul}}}{\textcolor{green}{\nil}}) +}$ +does reduce, to +\[ + \app{ + \app{ + \cons + }{( + \app{ + \textcolor{red}{ + \app{ + \symb{plus} + }{ + (\app{\suc}{\nul}) + } + } + }{ + \textcolor{blue}{\nul} + } + )} + }{ + (\app{ + \app{ + \symb{map} + }{ + \textcolor{red}{ + (\abs{\avar}{\nat}{ + \app{\app{ + \symb{plus} + }{ + (\app{\suc}{\nul}) + }}{ + \avar + } + }) + } + } + }{ + \textcolor{green}{\nil} + }) + } +\] +(in one go), by using the meta-substitution +$[F:=\metaabs{y\!:\!\nat}{\app{\textcolor{red}{\app{\symb{plus}}{(\app{\suc}{\nul})}}}{y}}, + x:=\metaabs{}{\textcolor{blue}{\nul}},t:=\metaabs{}{\textcolor{green}{\nil}}]$. +Similarly, +$\app{ + \app{ + \symb{map} + }{ + (\abs{\avar}{\nat}{ + \textcolor{red}{\app{ + \app{\symb{plus}}{\textcolor{black}{\avar}}}{ + (\app{\suc}{\nul}) + }} + }) + } +}{ + (\app{\app{\cons}{\textcolor{blue}{\nul}}}{\textcolor{green}{\nil}}) +}$ +reduces at the root to +\[ + \app{ + \app{ + \cons + }{( + \textcolor{red}{ + \app{ + \app{\symb{plus}}{\textcolor{blue}{\nul}} + }{(\app{\suc}{\nul})} + } + )} + }{ + (\app{ + \app{ + \symb{map} + }{ + (\abs{\avar}{\nat}{ + \textcolor{red}{ + \app{\app{ + \symb{plus} + }{ + \textcolor{black}{\avar} + }}{ + (\app{\suc}{\nul}) + } + } + }) + } + }{ + \textcolor{green}{\nil} + }) + } +\] +\end{example} + +\section{Potential subcategories} + +The formalism described in this paper does not have a clear name in the literature, although it is +a slight variation (to be precise: a restricted version) of systems that appear in various sources +(e.g., \cite{bla:00,kop:12}). +Essentially, it is a simply-typed version of \emph{combinatory reduction systems}~\cite{klo:80}, +with a $\beta$-rule implicitly included for all types. +We have imposed sanity limitations that often occur in the literature like limiting left-hand sides +to patterns and requiring right-hand sides to be in $\beta$-normal form; in the rare cases where +benchmarks are desired that violate these restrictions this can easily be encoded by including an +explicit ``application'' symbol $\symb{@}$ of the required type, and adding a rule +$\app{\app{\symb{@}}{(\abs{\avar}{\atype}{\app{F}{\avar}})}}{\bvar} \arrz \app{F}{\bvar}$. + +There are other formalisms of higher-order term rewriting in the literature, several of which can be +viewed as limitations of, or strategies for, the formalism described here. Hence, the same +benchmarks (or: a subset thereof) can be used in different categories should the need arise. We +list the most pertinent of them below. + +\subsection{Simply-typed Term Rewriting Systems~\cite{kus:01}} + +In this case, the set of terms is restricted to \emph{$\lambda$-free terms}; that is, abstraction +is not permitted in term formation. This limits both rule formation (no lambdas may occur on +either side of a rule), but also the terms that should be considered for termination or confluence. +Since terms contain no abstractions, the $\arr{\beta}$ step is not part of reduction. + +\begin{example} +Let $\symb{A} \hastype \mathsf{o} \arrtype \mathsf{o} \arrtype{o}$ and +$\symb{L} \hastype (\mathsf{o} \arrtype \mathsf{o}) \arrtype{o}$, and +$\Rules = \{ \app{\symb{A}}{(\app{\symb{L}}{\avar})} \arrz x \}$. +(Note that this rule has type $\mathsf{o} \arrtype \mathsf{o}$.) +This system is: +\begin{itemize} +\item \emph{terminating} when viewed as an STRS, because every step decreases the size o fthe term +\item \emph{non-terminating} when viewed in the default way, because, writing + $\omega = \app{\symb{L}}{(\abs{\avar}{\mathtt{o}}{\app{\app{\symb{A}}{\avar}}{\avar}})}$, + we have $ + \app{\app{\symb{A}}{\omega}}{\omega} = + \app{\app{\symb{A}}{(\app{\symb{L}}{\underline{(\abs{\avar}{\mathtt{o}}{\app{\app{\symb{A}}{\avar}}{\avar}})}})}}{\omega} \arr{\Rules} + \app{(\abs{\avar}{\mathtt{o}}{\app{\app{\symb{A}}{\avar}}{\avar}})}{\omega} \arr{\beta} + \app{\app{\symb{A}}{\omega}}{\omega}$. +\end{itemize} +\end{example} + +\subsection{Plain higher-order rewriting~\cite{jou:rub:99}} + +In this case, the set of terms is not restricted, but the set of \emph{rules} is: we require that +$\arity(\avar) = 0$ for all variables. That is, variables should always occur unapplied in the +left-hand side, and meta-substitution is just substitution. This means matching is \emph{plain}. +This is the formalism that was used in the higher-order category of the termination competition up +to 2024. + +\begin{example} +In plain systems, there is no way to specify a rule +\[ +\begin{array}{c} +\app{\symb{der}}{(\abs{\avar}{\real}{(\app{\app{\symb{plus}}{(\app{F}{\avar})}}{(\app{G}{\avar})})})}\ \arrz \\ +\abs{\avar}{\real}{\app{\app{\symb{plus}}{ + (\app{(\app{\symb{der}}{(\abs{\bvar}{\nat}{(\app{F}{\bvar})})})}{\avar}) + }}{ + (\app{(\app{\symb{der}}{(\abs{\bvar}{\nat}{(\app{F}{\bvar})})})}{\avar}) + }} +\end{array} +\] +However, for systems that can be specified with arity $0$ for all variables (such as +Example~\ref{ex:map} and all STRSs), termination and confluence are equivalent whether we consider +the systems as plain or default (since the set of terms and the reduction relation are unchanged). +\end{example} + +\subsection{Pattern higher-order rewriting systems~\cite{nip:91}} + +This formalism as defined considers rewriting modulo $\alpha\beta\eta$. However, it can be +modeled in our default formalism by (1) limiting the set of terms to terms in $\eta$-long form, and +(2) imposing a \emph{priority}: $\arr{\beta}$ must always be applied before any step using a rule. + +\begin{example} +Let $\symb{h} \hastype (\mathsf{o} \arrtype \mathsf{o}) \arrtype \mathsf{o}$ and $\symb{a} \hastype \mathsf{o}$, +and $\Rules = \{ \app{\symb{h}}{F} \arrz \app{F}{(\app{\symb{h}}{(\abs{\avar}{\mathsf{o}}{\symb{a}})})} \}$. +This system is: +\begin{itemize} +\item \emph{terminating} when viewed as a PRS, since the priority ensures that, when + $\app{\symb{h}}{(\abs{\avar}{\mathsf{o}}{\symb{a}})}$ is reduced, the result is immediately + $\beta$-normalised to $\symb{a}$; termination of the whole system then follows by a computability + argument; +\item \emph{non-terminating} when viewed in the default way, since + $\app{\symb{h}}{(\abs{\avar}{\mathsf{o}}{\symb{a}})} \arr{\Rules} + \app{(\abs{\avar}{\mathsf{o}}{\symb{a}})}{\underline{(\app{\symb{h}}{(\abs{\avar}{\mathsf{o}}{\symb{a}})})}}$, + which contains the original term as a subterm. +\end{itemize} +\end{example} + +Note that, for rules to be usable on terms in $\eta$-long form, they should match on $\eta$-long +terms, and result in them as well; hence, benchmarks can only be used as PRS benchmarks if, for all +rules $\ell \arrz r \in \Rules$, both $\ell$ and $r$ are well-behaved for the set $\FV(\ell)$: +\begin{itemize} +\item all variables in $\FV(\ell)$ are well-behaved; +\item $\abs{\avar}{\atype}{s}$ is well-behaved if $s$ is; +\item a term whose type is a sort is well-behaved if it has one of the forms + $\app{\avar}{s_1} \cdots s_n$ or $\app{\afun}{s_1} \cdots s_n$, and all $s_i$ are well-behaved. +\end{itemize} +(That is, $\ell$ and $r$ are $\beta$-normal terms which are \emph{mostly} in $\eta$-long form, +except the free variables do not need to be expanded.) + +\bibliographystyle{plain} +\bibliography{stcrs} + +\end{document} +