docs: Update generics book for 2025

docs/Generics/README.md

@@ -18,7 +18,7 @@ It's written in TeX, so to typeset the PDF yourself, you need a TeX distribution
 
 ### Using `make`
 
-Running `make` in `docs/Generics/` will run `pdflatex` and `bibtex` in the right order to generate the final document with bibliography, index and cross-references:
+Running `make` in `docs/Generics/` will run `pdflatex` and `bibtex` in the right order to generate the final document with bibliography, index, and cross-references:
 
 ```
 cd docs/Generics/
@@ -61,16 +61,13 @@ This is a work in progress.
 
 The following chapters need some editing:
 
-- Part II:
-  - Substitution Maps
 - Part IV:
   - Completion
 
 The following chapters are not yet written:
 
 - Part III:
-  - Opaque Return Types
   - Existential Types
 - Part IV:
   - The Property Map
-  - Rule Minimization
+  - Minimization

docs/Generics/chapters/math-summary.tex

@@ -52,12 +52,12 @@ \section*{More}
 \item Formal systems (\SecRef{derived req}).
 \item Equivalence relations (\SecRef{valid type params}, \SecRef{rewrite graph}).
 \item Partial and linear orders (\SecRef{reduced types}, \SecRef{rewritesystemintro}, \SecRef{building terms}).
-\item Category theory (\SecRef{submapcomposition}).
+\item Category theory (\SecRef{sec:composition}).
 \item Boolean satisfiability (\SecRef{associated type inference}).
 \item Directed graphs (\SecRef{type parameter graph}, \SecRef{finding conformance paths}, \SecRef{recursive conformances}, \SecRef{protocol component}).
 \item Proof by induction (\SecRef{generic signature validity}).
-\item Computability theory (\SecRef{tag systems}, \SecRef{word problem}).
-\item Finitely-presented monoids and string rewriting (\ChapRef{monoids}, \ChapRef{completion}).
+\item Computability theory (\SecRef{halting problem}, \SecRef{word problem}).
+\item Finitely-presented monoids and string rewriting (\ChapRef{monoids}, \ChapRef{chap:completion}).
 \end{itemize}
 
 \end{document}

docs/Generics/chapters/rule-minimization.tex → docs/Generics/chapters/minimization.tex

@@ -2,7 +2,7 @@
 
 \begin{document}
 
-\chapter[]{Rule Minimization}\label{rqm minimization}
+\chapter[]{Minimization}\label{rqm minimization}
 
 \ifWIP
 TODO:
@@ -42,8 +42,6 @@
 \end{itemize}
 \fi
 
-\section[]{Loop Normalization}
-
 \ifWIP
 \cite{homotopyreduction}
 \IndexFlag{disable-requirement-machine-loop-normalization}
@@ -127,6 +125,25 @@
 
 \fi
 
+\section[]{Concrete Contraction}\label{concrete contraction}
+
+\IndexFlag{disable-requirement-machine-concrete-contraction}
+\IndexTwoFlag{debug-requirement-machine}{concrete-contraction}
+
+\IndexDefinition{concrete contraction}
+
+\ifWIP
+TODO:
+\begin{itemize}
+\item Doesn't actually appear in signature so should not impact minimization
+\item The problem: it might give you a smaller anchor
+\item Invariant violation without concrete contraction
+\item Concrete contraction substitutes superclass and concrete types
+\item Also GSB compatibility: T.A, T == C, C.A is a concrete typealias that's not an associated type. this doesn't add a rule
+\item Open question: can we do this in a more principled way
+\end{itemize}
+\fi
+
 \section[]{Source Code Reference}\label{rqm minimization source ref}
 
 \end{document}