You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
\lettrine{K}{nuth-Bendix completion} is the central algorithm in the Requirement Machine. Completion attempts to construct a \index{convergent rewrite system}convergent rewrite system from a list of rewrite rules, and a convergent rewrite system allows us to decide if two terms have the same reduced form in a finite number of steps, solving the word problem. As we saw in the previous chapter, our initial rewrite rules are defined by the explicit requirements of a generic signature and its protocol dependencies. A desirable property of this mapping was given by Theorem~\ref{derivation to path}: a \emph{derived} requirement defines a rewrite path over these rewrite rules representing explicit requirements. All of this means that completion gives us a \emph{decision procedure} for the \index{derived requirement}derived requirements formalism: the question of whether any given derived requirement is satisfied---that is, if there exists a valid derivation built from explicit requirements---is easily solved by term reduction in a convergent rewrite system. This is the foundation on which we build both \index{generic signature query}generic signature queries and \index{requirement minimization}minimization.
10
10
11
-
\paragraph{The algorithm.} We'll give a self-contained description first, with much of the rest of the chapter devoted to examples. Our description can be supplemented with any text on rewrite systems, such as \cite{book2012string} or \cite{andallthat}. The algorithm is somewhat clever; to really ``get it'' might require several attempts. Donald~E.~Knuth and Peter Bendixdescribed the algorithm for term rewrite systems in a 1970 paper \cite{Knuth1983}; a correctness proof was later given by \cite{HUET198111}. In our application, the terms are elements of a free monoid, so we have a string rewrite system; this special case was studied in \cite{narendran}. A survey of related techniques appears in \cite{BUCHBERGER19873}.
11
+
\paragraph{The algorithm.} We'll give a self-contained description first, with much of the rest of the chapter devoted to examples. Our description can be supplemented with any text on rewrite systems, such as \cite{book2012string} or \cite{andallthat}. The algorithm is somewhat clever; to really ``get it'' might require several attempts. \index{Donald~Knuth}Donald~E.~Knuth and \index{Peter Bendix}Peter Bendix described the algorithm for term rewrite systems in a 1970 paper \cite{Knuth1983}; a correctness proof was later given by\index{Gerard Huet@G\'erard Huet}G\'erard Huet in\cite{HUET198111}. In our application, the terms are elements of a free monoid, so we have a string rewrite system; this special case was studied in \cite{narendran}. A survey of related techniques appears in \cite{BUCHBERGER19873}.
12
12
13
13
The entry point into the Knuth-Bendix completion procedure is Algorithm~\ref{knuthbendix}, but we break off four smaller pieces before we get there, so that only the top-level loop remains:
\item The roles of ``left'' and ``right'' are reversed because requirements use a different convention; in a reduced same-type requirement $\FormalReq{U == V}$, we have $\texttt{U} < \texttt{V}$, whereas in a rewrite rule $u\Rightarrow v$ we have $v<u$.
530
530
\item Reduced same-type requirements have the ``shortest'' distance between the left-hand and right-hand side, so if \texttt{T}, \texttt{U} and \texttt{V} are all equivalent and $\texttt{T}<\texttt{U}<\texttt{V}$, the corresponding requirements are $\FormalReq{T == U}$, $\FormalReq{U == V}$. On the other hand, if we have three terms $t$, $u$ and $v$ with $t<u<v$, then the two corresponding rewrite rules would be $u\Rightarrow t$, $v\Rightarrow t$.
531
531
\end{itemize}
532
-
These differences are explained by the original \Index{GenericSignatureBuilder@\texttt{GenericSignatureBuilder}}\texttt{GenericSignatureBuilder} minimization algorithm, described as finding a minimum spanning tree for a graph of connected components. The notion of reduced requirement output by this algorithm became part of the Swift stable \index{ABI}ABI. In Section~\ref{requirementbuilder} we show that a list of rewrite rules in a reduced rewrite system defines a list of reduced requirements via a certain transformation.
532
+
These differences are explained by the original \Index{GenericSignatureBuilder@\texttt{GenericSignatureBuilder}}\texttt{GenericSignatureBuilder} minimization algorithm, described as finding a minimum \index{spanning tree}spanning tree for a graph of connected components. The notion of reduced requirement output by this algorithm became part of the Swift stable \index{ABI}ABI. In Section~\ref{requirementbuilder} we show that a list of rewrite rules in a reduced rewrite system defines a list of reduced requirements via a certain transformation.
533
533
534
534
What we call reduced rewrite systems are sometimes ``normalized'', ``canonical'', or ``inter-reduced'' in the literature. Our rewrite system also implements a third \emph{substitution simplification} pass for rewrite system simplification. Substitution simplification reduces substitution terms appearing in superclass, concrete type and concrete conformance symbols. We will discuss it in Chapter~\ref{propertymap}.
We see that applying $\Sigma_{\ConfReq{X}{S}}$ to \texttt{\ttgp{0}{0}.[S]A} and \texttt{\ttgp{0}{0}.[S]C.[S]B} also outputs identical types: $\AssocType{[S]A}\otimes\ConfReq{X}{S}=\AssocType{[S]B}\otimes\ConfReq{Y}{S}=\texttt{Int}$. Is this the case for \emph{every} conformance to \texttt{S}? That is, is it true that $G_\texttt{S}\vDash\FormalReq{\texttt{\ttgp{0}{0}.A} == \texttt{\ttgp{0}{0}.C.B}}$?
1077
1077
1078
-
We will see the answer is ``yes,'' proving that our function \texttt{f()} type checks. For a geometric perspective, we turn to the \index{type parameter graph}type parameter graph\footnote{In our previous formulation, the type parameter graph has a distinguished root node, with every generic parameter as a child of this root. Now, our generic signature only has one generic parameter, so a root node would be superflous; we omit it in what follows.} for $G_\texttt{S}$. Figure~\ref{protocolsfig} constructs this graph in three stages:
1078
+
We will see the answer is ``yes,'' proving that our function \texttt{f()} type checks. For a visual perspective, we turn to the \index{type parameter graph}type parameter graph\footnote{In our previous formulation, the type parameter graph has a distinguished root node, with every generic parameter as a child of this root. Now, our generic signature only has one generic parameter, so a root node would be superflous; we omit it in what follows.} for $G_\texttt{S}$. Figure~\ref{protocolsfig} constructs this graph in three steps. Between each step, we have a \index{graph homomorphism}graph homomorphism---in fact, a \index{covering map}covering map, in the sense of Section~\ref{protocolcomponent}---transforming one graph into the other:
1079
1079
\begin{enumerate}
1080
-
\itemWe first draw the graph as it would be without the protocol stating any same-type requirements; we get an infinite tree where each interior node is the parent of one other interior node, and two leaf nodes.
1080
+
\itemThe first step shows the graph as it would be without the protocol stating any same-type requirements; we get an infinite tree where each interior node is the parent of one other interior node, and two leaf nodes.
1081
1081
1082
-
\item The second step introduces the same-type requirement $\FormalReq{Self == Self.C.C}$, mapping the infinite tree down to a finite graph with a cycle. Those type parameters with an even number of \texttt{C}'s are now equivalent to \texttt{\ttgp{0}{0}}, and those with an odd number, to \texttt{\ttgp{0}{0}.C}.
1082
+
\item The second step introduces the requirement $\FormalReq{Self == Self.C.C}$, collapsing the infinite tree down to a finite graph with a cycle. Those type parameters with an even number of \texttt{C}'s are now equivalent to \texttt{\ttgp{0}{0}}, and those with an odd number, to \texttt{\ttgp{0}{0}.C}.
1083
1083
1084
1084
\item The final step introduces $\FormalReq{Self.B == Self.C.A}$. This collapses \texttt{\ttgp{0}{0}.B} with \texttt{\ttgp{0}{0}.C.A}, and as one might suspect, \texttt{\ttgp{0}{0}.A} with \texttt{\ttgp{0}{0}.C.B}.
Protocol \texttt{S} is an interesting test case demonstrating the rewrite system's ability to discover non-trivial identities. It originates from a developer's bug report in 2020 \cite{sr12120}; at the time, it broke the \Index{GenericSignatureBuilder@\texttt{GenericSignatureBuilder}}\texttt{GenericSignatureBuilder}'s minimization algorithm. Amusingly, the \index{Rust}Rust compiler's generics implementation is unable to prove the derived requirement:
1304
+
Protocol \texttt{S} is an interesting test case demonstrating the rewrite system's ability to discover non-trivial identities. It originates from a developer's bug report in 2020 \cite{sr12120}; \index{history}at the time, it broke the \Index{GenericSignatureBuilder@\texttt{GenericSignatureBuilder}}\texttt{GenericSignatureBuilder}'s minimization algorithm. Amusingly, the \index{Rust}Rust compiler's generics implementation is unable to prove the derived requirement:
Both the \index{Knuth-Bendix algorithm}Knuth-Bendix completion and the \index{left simplification}rule simplification algorithms preserve the equivalence relation on terms. When completion adds a new rewrite rule, it is because the corresponding pair of terms are already joined by a \index{rewrite path}rewrite path. There is an analogous guarantee when \index{right simplification}rule simplification deletes a rewrite rule: the two terms are known to be joined by at least one other rewrite path that does not involve this rule. Intuitively, we understand that these transformations knead the \index{reduction relation}reduction relation into a better form, while the equivalence relation on terms remains completely determined by the relations of our initial \index{monoid presentation}monoid presentation.
1323
1323
1324
-
Mathematically speaking, both algorithms are defined as a transformation on monoid presentations. This transformation decomposes into a composition of sequential steps, where at each step the monoid presentation is changed in such a way that \index{monoid isomorphism}monoid isomorphism is preserved. So far, we've seen two of the four fundamental isomorphism-preserving transformations; two more make the full set:
1324
+
Mathematically speaking, both algorithms are defined as a transformation on monoid presentations. This transformation decomposes into a composition of sequential steps, where at each step the monoid presentation is changed in such a way that \index{monoid isomorphism}monoid isomorphism is preserved. So far, we've seen two of the four isomorphism-preserving transformations below, so named after \index{Heinrich Tietze}Heinrich Tietze, who introduced them in 1908:
1325
1325
\begin{definition}
1326
1326
Let $\AR$ be a finitely-presented monoid. An \IndexDefinition{Tietze transformation}\emph{elementary Tietze transformation}, or just Tietze transformation, is one of the following:
0 commit comments