docs: Update generics.tex

docs/Generics/chapters/basic-operation.tex

@@ -215,14 +215,14 @@ \section{Protocol Components}\label{protocol component}
 We will show that the protocols that can appear in the \index{derived requirement}derivations of a given generic signature are precisely those reachable from an initial set in the \index{protocol dependency graph}protocol dependency graph. We begin by considering protocol dependencies between protocols first. Along the way, we also introduce the \emph{protocol component graph} to get around complications caused by circular dependencies.
 
 \begin{definition}
-A protocol $\protosym{P}$ \emph{depends on} a protocol $\protosym{Q}$ (or has a \emph{protocol dependency} on~$\protosym{Q}$) if we can derive a conformance to $\protosym{Q}$ from the protocol generic signature $G_\texttt{P}$; that is, if $G_\texttt{P}\vDash\ConfReq{T}{Q}$ for some type parameter \texttt{T}. We write $\protosym{P}\prec\protosym{Q}$ if this relationship holds. The \IndexDefinition{protocol dependency set}\emph{protocol dependency set} of a protocol $\protosym{P}$ is then the set of all protocols $\protosym{Q}$ such that $\protosym{P}\prec\protosym{Q}$.
+A protocol $\protosym{P}$ \emph{depends on} a protocol $\protosym{Q}$ (or has a \emph{protocol dependency} on~$\protosym{Q}$) if we can derive a conformance to $\protosym{Q}$ from the protocol generic signature $\GP$; that is, if $\GP\vdash\ConfReq{T}{Q}$ for some type parameter \texttt{T}. We write $\protosym{P}\prec\protosym{Q}$ if this relationship holds. The \IndexDefinition{protocol dependency set}\emph{protocol dependency set} of a protocol $\protosym{P}$ is then the set of all protocols $\protosym{Q}$ such that $\protosym{P}\prec\protosym{Q}$.
 \end{definition}
 
 \LemmaRef{subst lemma} implies that $\prec$ is a \index{transitive relation}transitive relation; that is, if $\protosym{P}\prec\protosym{Q}$ and $\protosym{Q}\prec\protosym{R}$, then $\protosym{P}\prec\protosym{R}$. In fact, $\prec$ is the \index{reachability relation}reachability relation in the protocol dependency graph. Before we can prove this, we need a technical result.
 
 \smallskip
 
-Let $f$ be the canonical projection from the \index{conformance path graph}conformance path graph of $G_\texttt{P}$ into the protocol dependency graph. Recall that $f$ maps an \index{abstract conformance}abstract conformance $\ConfReq{T}{P}$ to the protocol $\protosym{P}$; we previously used $f$ to study recursive conformances. Not only is $f$ a \index{graph homomorphism}graph homomorphism, but it is also a \IndexDefinition{covering map}\emph{covering map}, because if we take some abstract conformance $\ConfReq{T}{P}$, the set of \index{edge}edges with \index{source vertex}source $\ConfReq{T}{P}$ is in one-to-one correspondence with the set of edges with source $f(\ConfReq{T}{P})=\protosym{P}$. In fact, by definition both sets of edges are indexed by the \index{associated conformance requirement}associated conformance requirements defined in $\protosym{P}$.
+Let $f$ be the canonical projection from the \index{conformance path graph}conformance path graph of $\GP$ into the protocol dependency graph. Recall that $f$ maps an \index{abstract conformance}abstract conformance $\ConfReq{T}{P}$ to the protocol $\protosym{P}$; we previously used $f$ to study recursive conformances. Not only is $f$ a \index{graph homomorphism}graph homomorphism, but it is also a \IndexDefinition{covering map}\emph{covering map}, because if we take some abstract conformance $\ConfReq{T}{P}$, the set of \index{edge}edges with \index{source vertex}source $\ConfReq{T}{P}$ is in one-to-one correspondence with the set of edges with source $f(\ConfReq{T}{P})=\protosym{P}$. In fact, by definition both sets of edges are indexed by the \index{associated conformance requirement}associated conformance requirements defined in $\protosym{P}$.
 
 The theory is explained in \cite{godsil2001algebraic}, but here is a quick example to help with the intuition. We can wind the infinite ray around a cycle of length four, infinitely many times, mapping each integer $n\mapsto n \bmod 4$; every vertex has a single successor in both graphs:
 \begin{center}
@@ -271,7 +271,7 @@ \section{Protocol Components}\label{protocol component}
 If $\protosym{P}$ and $\protosym{Q}$ are any two protocols, then $\protosym{P}\prec\protosym{Q}$ if and only if there exists a path from $\protosym{P}$ to $\protosym{Q}$ in the protocol dependency graph.
 \end{proposition}
 \begin{proof}
-First, suppose $\protosym{P}\prec\protosym{Q}$. Then, there is a type parameter \texttt{T} such that $G_\texttt{P}\vDash\ConfReq{T}{Q}$. By \ThmRef{conformance paths theorem}, there exists a conformance path for $\ConfReq{T}{Q}$. This conformance path defines a path in the protocol dependency graph from \protosym{P} to $\protosym{Q}$. Now, suppose that we have a path from $\protosym{P}$ to $\protosym{Q}$ in the protocol dependency graph. Every protocol dependency path in originating at $\protosym{P}$ lifts to a path originating at $\ConfReq{Self}{P}$ in the conformance path graph of $G_\texttt{P}$. By \AlgRef{invertconformancepath}, this conformance path defines a derived conformance requirement $\ConfReq{T}{Q}$ in $G_\texttt{P}$, showing that $\protosym{P}\prec\protosym{Q}$.
+First, suppose $\protosym{P}\prec\protosym{Q}$. Then, there is a type parameter \texttt{T} such that $\GP\vdash\ConfReq{T}{Q}$. By \ThmRef{conformance paths theorem}, there exists a conformance path for $\ConfReq{T}{Q}$. This conformance path defines a path in the protocol dependency graph from \protosym{P} to $\protosym{Q}$. Now, suppose that we have a path from $\protosym{P}$ to $\protosym{Q}$ in the protocol dependency graph. Every protocol dependency path in originating at $\protosym{P}$ lifts to a path originating at $\ConfReq{Self}{P}$ in the conformance path graph of $\GP$. By \AlgRef{invertconformancepath}, this conformance path defines a derived conformance requirement $\ConfReq{T}{Q}$ in $\GP$, showing that $\protosym{P}\prec\protosym{Q}$.
 \end{proof}
 
 \begin{listing}\captionabove{Protocol component demonstration}\label{protocol component listing}
@@ -339,7 +339,7 @@ \section{Protocol Components}\label{protocol component}
 \item If $x\equiv y$ and $y\equiv z$, then in particular $x\prec y$ and $y\prec z$, so $x\prec z$, because $\prec$ is transitive. By the same argument, we also have $y\prec x$ and $z\prec y$, hence $z\prec x$. Therefore, $x\equiv z$.
 \end{itemize}
 
-The \index{equivalence class}equivalence classes of $\equiv$ are the \emph{strongly connected components} of $(V, E)$. We give this set the structure of a directed graph: an edge joins two components if and only if there is an edge joining some vertex in the first component with another vertex in the second component. The reachability relation of $(V, E)$ is well-defined on strongly connected components; if $x_1\equiv x_2$ and $y_1\equiv y_2$, then $x_1\prec y_1$ if and only if $x_2\prec y_2$. A \index{DAG|see {directed acyclic graph}}\IndexDefinition{directed acyclic graph}\emph{directed acyclic graph} (or DAG) is a graph without cycles; that is, non-trivial paths with the same source and destination vertex. In a directed acyclic graph, each vertex is in a strongly connected component by itself. Conversely, the graph of strongly connected components is itself acyclic, because a cycle is always contained entirely in its strongly connected component.
+The \index{equivalence class}equivalence classes of $\equiv$ are the \emph{strongly connected components} of $(V, E)$. We give this set the structure of a directed graph: an edge joins two components if and only if there is an edge joining some vertex in the first component with another vertex in the second component. The reachability relation of $(V, E)$ is \index{well-defined}well-defined on strongly connected components; if $x_1\equiv x_2$ and $y_1\equiv y_2$, then $x_1\prec y_1$ if and only if $x_2\prec y_2$. A \index{DAG|see {directed acyclic graph}}\IndexDefinition{directed acyclic graph}\emph{directed acyclic graph} (or DAG) is a graph without cycles; that is, non-trivial paths with the same source and destination vertex. In a directed acyclic graph, each vertex is in a strongly connected component by itself. Conversely, the graph of strongly connected components is itself acyclic, because a cycle is always contained entirely in its strongly connected component.
 
 \begin{wrapfigure}{l}{3.5cm}
 \begin{tikzpicture}[x=1cm, y=1.3cm]
@@ -513,11 +513,11 @@ \section{Protocol Components}\label{protocol component}
 The idea of a protocol having a dependency relationship on another protocol generalizes to a generic signature depending on a protocol. The protocol dependencies of a generic signature are those that may appear in a derivation.
 
 \begin{definition}
-A generic signature $G$ has a \IndexDefinition{protocol dependency}\emph{protocol dependency} on a protocol $\protosym{P}$, denoted \index{$\prec$}\index{$\prec$!z@\igobble|seealso{protocol dependency}}$G\prec\protosym{P}$, if we can derive a conformance to $\protosym{P}$ from $G$; that is, $G\vDash\ConfReq{T}{P}$. The \emph{protocol dependency set} of a generic signature $G$ is the set of all protocols $\protosym{P}$ such that $G\prec\protosym{P}$.
+A generic signature $G$ has a \IndexDefinition{protocol dependency}\emph{protocol dependency} on a protocol $\protosym{P}$, denoted \index{$\prec$}\index{$\prec$!z@\igobble|seealso{protocol dependency}}$G\prec\protosym{P}$, if we can derive a conformance to $\protosym{P}$ from $G$; that is, $G\vdash\ConfReq{T}{P}$. The \emph{protocol dependency set} of a generic signature $G$ is the set of all protocols $\protosym{P}$ such that $G\prec\protosym{P}$.
 
 \end{definition}
 
-This new form of $\prec$ is not a binary relation by our prior definition, because the two operands come from different sets. However, it is still transitive in the sense that $G\prec\protosym{P}$ and $\protosym{P}\prec\protosym{Q}$ together imply $G\prec\protosym{Q}$. Note that the two definitions of $\prec$ are related via the \index{protocol generic signature}protocol generic signature: $G_\texttt{P}\prec\protosym{Q}$ if and only if $\protosym{P}\prec\protosym{Q}$.
+This new form of $\prec$ is not a binary relation by our prior definition, because the two operands come from different sets. However, it is still transitive in the sense that $G\prec\protosym{P}$ and $\protosym{P}\prec\protosym{Q}$ together imply $G\prec\protosym{Q}$. Note that the two definitions of $\prec$ are related via the \index{protocol generic signature}protocol generic signature: $\GP\prec\protosym{Q}$ if and only if $\protosym{P}\prec\protosym{Q}$.
 
 Now, consider the protocols that appear on the right-hand sides of the \emph{minimal} (that is, explicit) conformance requirements of our generic signature $G$; call these the \emph{successors} of $G$, by analogy with the successors of a protocol in the protocol dependency graph. If we consider all protocols reachable via paths originating from the successors of~$G$, we arrive at the complete set of protocol dependencies of~$G$.