swift-mirror/docs/Generics/chapters/rewrite-system-minimization.tex

\documentclass[../generics]{subfiles}

\begin{document}

\chapter{Rewrite System Minimization}\label{rqm minimization}

\ifWIP
TODO:
\begin{itemize}
\item Theory: parallel paths
\item Rule appears once in empty context
\item I want to delete a rule without changing the rewrite system
\item Two parallel paths; one is the rule itself, the other does not involve the rule
\item I can replace one parallel path with another in a rewrite loop
\item Specifically, I can replace my rule with its defining path
\item Now no loops mention the rule
\item What happens to the original loop?
\item Geometric space: we have a hole, and a loop that winds around it. we cannot shrink the loop down to a single point.
\item We fill in the hole, now the loop shrinks to a single point.
\item Homotopy relation
\end{itemize}
\fi

\section{Homotopy Reduction}\label{homotopy reduction}

\IndexTwoFlag{debug-requirement-machine}{homotopy-reduction}
\IndexTwoFlag{debug-requirement-machine}{homotopy-reduction-detail}

\ifWIP
TODO:
\begin{itemize}
\item Finding rules appearing once in empty context, caching this per-rewrite loop
\item Deleting uninteresting loops
\item Rewrite path evaluator
\item Finding best candidate
\item Replacing a rule with a path
\item Marking rules as redundant
\item Recording replacement paths
\item flag to dump redundant paths
\item propagating explicit flag
\item propagating explicit ID
\end{itemize}
\fi

\section{Loop Normalization}

\cite{homotopyreduction}
\IndexFlag{disable-requirement-machine-loop-normalization}

\ifWIP
TODO:
\begin{itemize}
\item collapse inverses together
\item orthogonal rewrite steps and interchange
\item freely reduced loop
\item example after rule replacement or something
\item cyclically reduced loop
\item cyclic reduction example from adding a rewrite rule where critical pair resolves trivially
\item ``homotopy relation generated by empty set''
\end{itemize}
\fi

\section{The Elimination Order}\label{elimination order}

\ifWIP
TODO:
\begin{itemize}
\item three passes
\item each pass considers (rule, loop) pairs by certain order
\item describe each heuristic
\end{itemize}
\fi

\section{Conformance Minimization}\label{minimal conformances}

\IndexTwoFlag{debug-requirement-machine}{minimal-conformances}
\IndexTwoFlag{debug-requirement-machine}{minimal-conformances-detail}

\ifWIP
TODO:
\begin{itemize}
\item example where homotopy reduction minimizes too much
\item invariant: relate to conformance paths, and reducing the unbound term to bound term
\item protocol inheritance
\item concrete conformances
\item fake completion algorithm
\item critical pairs: conformance vs conformance, conformance vs same-type
\item the LHS simplified hack to keep requirements in their ``home protocol''
\item example where we need to minimize entire connected component at once because two requirements in two different protocols are mutually redundant
\end{itemize}
\fi

\section{Correctness}\label{minimization correctness}

\section{Building Requirements}\label{requirement builder}

\IndexFlag{requirement-machine-max-split-concrete-equiv-class-attempts}
\IndexTwoFlag{debug-requirement-machine}{minimization}
\IndexTwoFlag{debug-requirement-machine}{redundant-rules}
\IndexTwoFlag{debug-requirement-machine}{redundant-rules-detail}
\IndexTwoFlag{debug-requirement-machine}{split-concrete-equiv-class}

\ifWIP
TODO:
\begin{itemize}
\item same-type requirements: connected component thing
\item type alias requirements: the concrete equiv class splitting equivalent
\item splitting concrete equivalence classes: describe the problem, give example, say which generic signature invariant is violated. alternative formulation would work but breaks \index{ABI}ABI, so for GSB compatibility we split equivalence classes.
\end{itemize}
\fi

\section{Source Code Reference}\label{rqm minimization source ref}

\end{document}