From 9e2b75996bf290ee72471d819c7de0c7058eb833 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 6 Dec 2021 12:56:35 -0500 Subject: [PATCH 1/3] improvements --- doc/TYPES2021/Demos/HSP.tex | 49 +++++++++++++++++++------------------ doc/TYPES2021/agda-hsp.tex | 10 ++++---- doc/TYPES2021/wjd.sty | 7 +++--- src/Demos/HSP.lagda | 46 +++++++++++++++++----------------- 4 files changed, 57 insertions(+), 55 deletions(-) diff --git a/doc/TYPES2021/Demos/HSP.tex b/doc/TYPES2021/Demos/HSP.tex index 03494267..c68811ff 100644 --- a/doc/TYPES2021/Demos/HSP.tex +++ b/doc/TYPES2021/Demos/HSP.tex @@ -30,7 +30,7 @@ \section{Introduction} repository~\cite{ualib_v1.0.0}.} suffered from a few flaws that raised two concerns. First, it was not clear whether the proof was fully constructive. Second, it was shown that if one (say, a subversive -adversary) were to take the type \ab{X}---used to represent an arbitrary collection of +adversary) were to take the type \ab{X}---which we use to represent an arbitrary collection of variable symbols---to be just the two element type, then one could combine this with our proof and derive a contradiction. To resolve these issues, as well as improve the \agdaalgebras library more generally, we have rewritten parts of the library and have @@ -9282,9 +9282,9 @@ \section{Free Algebras} The informal construction of the free algebra in \af{S} (\af{P} \ab{𝒦}), for an arbitrary class \ab{𝒦} of \ab{𝑆}-algebras, proceeds by taking the quotient of \T{X} modulo a congruence relation that we will denote by \afld{β‰ˆ}. One approach is to let -\afld{β‰ˆ} := \af{β‹‚}\{\ab{ΞΈ} \af{∈} \af{Con} (\T{X}) : \T{X} \af{/} \ab{ΞΈ} \af{∈} \af{S} +\afld{β‰ˆ} be \af{β‹‚}\{\ab{ΞΈ} \af{∈} \af{Con} (\T{X}) : \T{X} \af{/} \ab{ΞΈ} \af{∈} \af{S} \ab{𝒦}\}.\footnote{\af{Con} (\T{X}) is the set of congruences of \T{X}.} -Alternatively we could let \ab{β„°} = \af{Th} \ab{𝒦} and take \afld{β‰ˆ} to be the least equivalence relation +Equivalently, we let \ab{β„°} = \af{Th} \ab{𝒦} and take \afld{β‰ˆ} to be the least equivalence relation on the domain of \T{X} such that \begin{enumerate} \item for every equation (\ab p , \ab q) \af{∈} \af{Th} \ab{𝒦} and every @@ -9300,9 +9300,8 @@ \section{Free Algebras} \as{β†’} \af{⟦~\ab f~\ab s~⟧}~\afld{⟨\$⟩}~\ab{ρ}~\afld{β‰ˆ}~\af{⟦~\ab f~\ab t~⟧}~\afld{⟨\$⟩}~\ab{ρ}\\[-8pt] \end{enumerate} -Whichever approach we choose, the \defn{relatively free algebra over} \ab{X} (relative to +The \defn{relatively free algebra over} \ab{X} (relative to \ab{𝒦}) is defined to be the quotient \Free{X} := \T{X}~\af{/}~\afld{β‰ˆ}. - Evidently \Free{X} is a subdirect product of the algebras in \{\T{X}~\af{/}~\ab{ΞΈ}\!\}, where \ab{ΞΈ} ranges over congruences modulo which \T{X} belongs to \af{S}~\ab{𝒦}. Thus, \Free{X} \af{∈} \af{P}(\af{S}~\ab{𝒦}) βŠ† \af{S}(\af{P}~\ab{𝒦}), and it follows @@ -9314,16 +9313,16 @@ \section{Free Algebras} \paragraph*{The relatively free algebra in Agda} We now define the relatively free algebra in Agda using the language of type theory. -Our approach will be different from the informal one described above, but the end result -will be the same. +%Our approach looks a bit different from the informal one described above, because we +%represent quotients as setoids, but the end result is the same. We start with a type \ab{β„°} representing a collection of identities and, instead of forming a quotient, we take the domain of the free algebra to be a setoid whose \afld{Carrier} is the type \Term{X} of {𝑆}-terms in \ab X and whose equivalence relation includes all pairs (\ab p , \ab q) \af{∈} \Term{X} \af{Γ—} \Term{X} such that \ab p \aod{β‰ˆ} \ab q is derivable from \ab{β„°}; that is, \ab{β„°} \aod{⊒} \ab X \aod{β–Ή} \ab p \aod{β‰ˆ} \ab q. Observe that elements of this setoid are equal iff they belong to the same equivalence -class of the congruence \afld{β‰ˆ} defined above. Therefore, the setoid so defined represents -the quotient \T{X}~\af{/}~\afld{β‰ˆ}. +class of the congruence \afld{β‰ˆ} defined above. Therefore, the setoid so defined, which +we denote by \Free{X}, represents the quotient \T{X}~\af{/}~\afld{β‰ˆ}. Finally, the interpretation of an operation in the free algebra is simply the operation itself, which works since \ab{β„°} \aod{⊒} \ab X \aod{β–Ή\au{}β‰ˆ\au{}} is a congruence relation. @@ -9474,8 +9473,8 @@ \section{Free Algebras} \end{code} \paragraph*{The natural epimorphism} % from 𝑻 X to 𝔽[ X ]} -We now define the natural epimorphism from \T{X} onto the relatively free algebra \Free{X} and prove that -its kernel is the congruence of \T{X} defined by the identities modeled by (\af S \ab{𝒦}, hence by) \ab{𝒦}. +We now define the natural epimorphism from \T{X} onto \Free{X} %(= \T{X}~\af{/}~\afld{β‰ˆ}) +and prove that its kernel is contained in the collection of identities modeled by \af{V} \ab{𝒦}. % (which we represent by \af{Th} (\af{V} \ab{𝒦})). \ifshort\else \begin{code}% @@ -10151,8 +10150,8 @@ \subsection{Formal proof} (i) every equational class is a variety and (ii) every variety is an equational class. \paragraph*{Every equational class is a variety} -For (i), we need an arbitrary equational class. To obtain one, we start with an arbitrary -collection \ab{β„°} of equations and let \ab{𝒦} = \af{Mod} \ab{β„°}, the equational class +For (i), we need an arbitrary equational class, which we obtain by starting with an arbitrary +collection \ab{β„°} of equations and then defining \ab{𝒦} = \af{Mod} \ab{β„°}, the equational class determined by \ab{β„°}. We prove that \ab{𝒦} is a variety by showing that \ab{𝒦} = \af{V} \ab{𝒦}. The inclusion \ab{𝒦} \aof{βŠ†} \af V \ab{𝒦}, which holds for all classes \ab{𝒦}, is called the \defn{expansive} property of \af{V}. The converse inclusion @@ -10451,15 +10450,18 @@ \subsection{Formal proof} \paragraph*{Every variety is an equational class} -To prove statement (ii), we need an arbitrary variety; to obtain one, we start with an arbitrary class -\ab{𝒦} of \ab{𝑆}-algebras and take its \emph{varietal closure}, \af{V} \ab{𝒦}. +For (ii), we need an arbitrary variety, which we obtain by starting with an arbitrary class +\ab{𝒦} of \ab{𝑆}-algebras and taking the \emph{varietal closure}, \af{V} \ab{𝒦}. We prove that \af{V} \ab{𝒦} is an equational class by showing it is precisely the collection of algebras that model the equations in \af{Th} (\af{V} \ab{𝒦}); that is, we prove \af{V} \ab{𝒦} = \af{Mod} (\af{Th} (\af{V} \ab{𝒦})). -The inclusion \af{V} \ab{𝒦} \aof{βŠ†} \af{Mod} (\af{Th} (\af{V} \ab{𝒦})) is a simple consequence of the fact that \af{Mod} \af{Th} is a closure operator. Nonetheless, completeness demands -that we formalize this fact, however trivial is its proof. +The inclusion \af{V} \ab{𝒦} \aof{βŠ†} \af{Mod} (\af{Th} (\af{V} \ab{𝒦})) is a simple +consequence of the fact that \af{Mod} \af{Th} is a closure operator% +\ifshort +, so we omit the proof and later refer to this fact as \af{ModTh-closure}. +\else +. Nonetheless, completeness demands that we formalize this fact, however trivial its proof. -\ifshort\else \begin{code}% \>[0]\<% \\ @@ -10499,12 +10501,10 @@ \subsection{Formal proof} \AgdaSymbol{=}\AgdaSpace{}% \AgdaFunction{ov}\AgdaSpace{}% \AgdaFunction{c}\<% -\end{code} -\fi -\begin{code}% -\>[0]\<% \\ % +\\[\AgdaEmptyExtraSkip]% +% \>[1]\AgdaFunction{ModTh-closure}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaFunction{V}\AgdaSymbol{\{}\AgdaArgument{Ξ²}\AgdaSpace{}% @@ -10540,9 +10540,10 @@ \subsection{Formal proof} \\ \>[0]\<% \end{code} +\fi -It remains to prove the converse inclusion, \af{Mod} (\af{Th} (V 𝒦)) \aof{βŠ†} \af{V} \ab{𝒦}, -which is the main focus of the rest of the paper. We proceed as follows: +It remains to prove the inclusion \af{Mod} (\af{Th} (V 𝒦)) \aof{βŠ†} \af{V} \ab{𝒦}, +and this task occupies the remainder of the paper. We proceed as follows: \begin{enumerate} \item \label{item:1} Let \ab{π‘ͺ} be the product of all algebras in \af{S} \ab{𝒦}, so that \ab{π‘ͺ} \af{∈} \af{P} (\af{S} \ab{𝒦}). diff --git a/doc/TYPES2021/agda-hsp.tex b/doc/TYPES2021/agda-hsp.tex index 2deb9537..2e1f9f22 100644 --- a/doc/TYPES2021/agda-hsp.tex +++ b/doc/TYPES2021/agda-hsp.tex @@ -55,16 +55,16 @@ \crefformat{footnote}{#2\footnotemark[#1]#3} %%%%%%%%%%%%%% TITLE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\ifshort -\title{Birkhoff's Variety Theorem formalized in Agda} -\else +% \ifshort +% \title{Birkhoff's Variety Theorem formalized in Agda} +% \else \title{A Machine-checked Proof of Birkhoff's Variety Theorem in Martin-L\"of Type Theory} -\fi +% \fi %%%%%%%%%%%%%% AUTHOR %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %\author{name}{affil}{email}{orcid}{funding}. \author{William DeMeo} - {Thmpr Research} + {Thmpr Laboratory} {williamdemeo@gmail.com}{https://orcid.org/0000-0003-1832-5690}{partially supported by ERC Consolidator Grant No.~771005.} \author{Jacques Carette}{McMaster University}{carette@mcmaster.ca}{https://orcid.org/0000-0001-8993-9804}{} diff --git a/doc/TYPES2021/wjd.sty b/doc/TYPES2021/wjd.sty index 66f085be..5a89489a 100644 --- a/doc/TYPES2021/wjd.sty +++ b/doc/TYPES2021/wjd.sty @@ -189,9 +189,10 @@ \end{minipage} \begin{minipage}{0.85\textwidth} \linespread{0.7}\selectfont - {\footnotesize This work and the agda-algebras library by - \href{https://williamdemeo.gitlab.io}{William DeMeo} and the - agda-algebras team is licensed under a \href{http://creativecommons.org/licenses/by-sa/4.0/}{Creative Commons Attribution-ShareAlike 4.0 International License}.} + {\footnotesize This work and the Agda Universal Algebra Library (\agdaalgebras) + % agda-algebras library by + % \href{https://williamdemeo.gitlab.io}{William DeMeo} and the agda-algebras team + is licensed under a \href{http://creativecommons.org/licenses/by-sa/4.0/}{Creative Commons Attribution ShareAlike 4.0 International License}.} \end{minipage} % \vskip2mm % \begin{minipage}{0.1\textwidth} diff --git a/src/Demos/HSP.lagda b/src/Demos/HSP.lagda index fde9dca5..f060a35c 100644 --- a/src/Demos/HSP.lagda +++ b/src/Demos/HSP.lagda @@ -30,7 +30,7 @@ Our first formal proof of the HSP theorem, completed in January of repository~\cite{ualib_v1.0.0}.} suffered from a few flaws that raised two concerns. First, it was not clear whether the proof was fully constructive. Second, it was shown that if one (say, a subversive -adversary) were to take the type \ab{X}---used to represent an arbitrary collection of +adversary) were to take the type \ab{X}---which we use to represent an arbitrary collection of variable symbols---to be just the two element type, then one could combine this with our proof and derive a contradiction. To resolve these issues, as well as improve the \agdaalgebras library more generally, we have rewritten parts of the library and have @@ -2029,9 +2029,9 @@ and belongs to the class \af{S} (\af{P} \ab{𝒦}), and for most applications th The informal construction of the free algebra in \af{S} (\af{P} \ab{𝒦}), for an arbitrary class \ab{𝒦} of \ab{𝑆}-algebras, proceeds by taking the quotient of \T{X} modulo a congruence relation that we will denote by \afld{β‰ˆ}. One approach is to let -\afld{β‰ˆ} := \af{β‹‚}\{\ab{ΞΈ} \af{∈} \af{Con} (\T{X}) : \T{X} \af{/} \ab{ΞΈ} \af{∈} \af{S} +\afld{β‰ˆ} be \af{β‹‚}\{\ab{ΞΈ} \af{∈} \af{Con} (\T{X}) : \T{X} \af{/} \ab{ΞΈ} \af{∈} \af{S} \ab{𝒦}\}.\footnote{\af{Con} (\T{X}) is the set of congruences of \T{X}.} -Alternatively we could let \ab{β„°} = \af{Th} \ab{𝒦} and take \afld{β‰ˆ} to be the least equivalence relation +Equivalently, we let \ab{β„°} = \af{Th} \ab{𝒦} and take \afld{β‰ˆ} to be the least equivalence relation on the domain of \T{X} such that \begin{enumerate} \item for every equation (\ab p , \ab q) \af{∈} \af{Th} \ab{𝒦} and every @@ -2047,9 +2047,8 @@ i~⟧}~\afld{⟨\$⟩}~\ab{ρ}) \as{β†’} \af{⟦~\ab f~\ab s~⟧}~\afld{⟨\$⟩}~\ab{ρ}~\afld{β‰ˆ}~\af{⟦~\ab f~\ab t~⟧}~\afld{⟨\$⟩}~\ab{ρ}\\[-8pt] \end{enumerate} -Whichever approach we choose, the \defn{relatively free algebra over} \ab{X} (relative to +The \defn{relatively free algebra over} \ab{X} (relative to \ab{𝒦}) is defined to be the quotient \Free{X} := \T{X}~\af{/}~\afld{β‰ˆ}. - Evidently \Free{X} is a subdirect product of the algebras in \{\T{X}~\af{/}~\ab{ΞΈ}\!\}, where \ab{ΞΈ} ranges over congruences modulo which \T{X} belongs to \af{S}~\ab{𝒦}. Thus, \Free{X} \af{∈} \af{P}(\af{S}~\ab{𝒦}) βŠ† \af{S}(\af{P}~\ab{𝒦}), and it follows @@ -2061,16 +2060,16 @@ identified in \Free{X}. \ifshort\else (Notice that \afld{β‰ˆ} may be empty, in w \paragraph*{The relatively free algebra in Agda} We now define the relatively free algebra in Agda using the language of type theory. -Our approach will be different from the informal one described above, but the end result -will be the same. +%Our approach looks a bit different from the informal one described above, because we +%represent quotients as setoids, but the end result is the same. We start with a type \ab{β„°} representing a collection of identities and, instead of forming a quotient, we take the domain of the free algebra to be a setoid whose \afld{Carrier} is the type \Term{X} of {𝑆}-terms in \ab X and whose equivalence relation includes all pairs (\ab p , \ab q) \af{∈} \Term{X} \af{Γ—} \Term{X} such that \ab p \aod{β‰ˆ} \ab q is derivable from \ab{β„°}; that is, \ab{β„°} \aod{⊒} \ab X \aod{β–Ή} \ab p \aod{β‰ˆ} \ab q. Observe that elements of this setoid are equal iff they belong to the same equivalence -class of the congruence \afld{β‰ˆ} defined above. Therefore, the setoid so defined represents -the quotient \T{X}~\af{/}~\afld{β‰ˆ}. +class of the congruence \afld{β‰ˆ} defined above. Therefore, the setoid so defined, which +we denote by \Free{X}, represents the quotient \T{X}~\af{/}~\afld{β‰ˆ}. Finally, the interpretation of an operation in the free algebra is simply the operation itself, which works since \ab{β„°} \aod{⊒} \ab X \aod{β–Ή\au{}β‰ˆ\au{}} is a congruence relation. @@ -2093,8 +2092,8 @@ module FreeAlgebra {Ο‡ : Level}(β„° : {Y : Type Ο‡} β†’ Pred (Term Y Γ— Term Y) \end{code} \paragraph*{The natural epimorphism} % from 𝑻 X to 𝔽[ X ]} -We now define the natural epimorphism from \T{X} onto the relatively free algebra \Free{X} and prove that -its kernel is the congruence of \T{X} defined by the identities modeled by (\af S \ab{𝒦}, hence by) \ab{𝒦}. +We now define the natural epimorphism from \T{X} onto \Free{X} %(= \T{X}~\af{/}~\afld{β‰ˆ}) +and prove that its kernel is contained in the collection of identities modeled by \af{V} \ab{𝒦}. % (which we represent by \af{Th} (\af{V} \ab{𝒦})). \ifshort\else \begin{code} @@ -2237,8 +2236,8 @@ We now show how to formally express and prove the twin assertions that (i) every equational class is a variety and (ii) every variety is an equational class. \paragraph*{Every equational class is a variety} -For (i), we need an arbitrary equational class. To obtain one, we start with an arbitrary -collection \ab{β„°} of equations and let \ab{𝒦} = \af{Mod} \ab{β„°}, the equational class +For (i), we need an arbitrary equational class, which we obtain by starting with an arbitrary +collection \ab{β„°} of equations and then defining \ab{𝒦} = \af{Mod} \ab{β„°}, the equational class determined by \ab{β„°}. We prove that \ab{𝒦} is a variety by showing that \ab{𝒦} = \af{V} \ab{𝒦}. The inclusion \ab{𝒦} \aof{βŠ†} \af V \ab{𝒦}, which holds for all classes \ab{𝒦}, is called the \defn{expansive} property of \af{V}. The converse inclusion @@ -2288,30 +2287,31 @@ Together, \af{V-expa} and \af{Eqclβ‡’Var} prove that every equational class is a \paragraph*{Every variety is an equational class} -To prove statement (ii), we need an arbitrary variety; to obtain one, we start with an arbitrary class -\ab{𝒦} of \ab{𝑆}-algebras and take its \emph{varietal closure}, \af{V} \ab{𝒦}. +For (ii), we need an arbitrary variety, which we obtain by starting with an arbitrary class +\ab{𝒦} of \ab{𝑆}-algebras and taking the \emph{varietal closure}, \af{V} \ab{𝒦}. We prove that \af{V} \ab{𝒦} is an equational class by showing it is precisely the collection of algebras that model the equations in \af{Th} (\af{V} \ab{𝒦}); that is, we prove \af{V} \ab{𝒦} = \af{Mod} (\af{Th} (\af{V} \ab{𝒦})). -The inclusion \af{V} \ab{𝒦} \aof{βŠ†} \af{Mod} (\af{Th} (\af{V} \ab{𝒦})) is a simple consequence of the fact that \af{Mod} \af{Th} is a closure operator. Nonetheless, completeness demands -that we formalize this fact, however trivial is its proof. +The inclusion \af{V} \ab{𝒦} \aof{βŠ†} \af{Mod} (\af{Th} (\af{V} \ab{𝒦})) is a simple +consequence of the fact that \af{Mod} \af{Th} is a closure operator% +\ifshort +, so we omit the proof and later refer to this fact as \af{ModTh-closure}. +\else +. Nonetheless, completeness demands that we formalize this fact, however trivial its proof. -\ifshort\else \begin{code} module _ (𝒦 : Pred(Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“)){X : Type (Ξ± βŠ” ρᡃ βŠ” β„“)} where private c = Ξ± βŠ” ρᡃ βŠ” β„“ ; ΞΉ = ov c -\end{code} -\fi -\begin{code} ModTh-closure : V{Ξ² = Ξ²}{ρᡇ}{Ξ³}{ρᢜ}{Ξ΄}{ρᡈ} β„“ ΞΉ 𝒦 βŠ† Mod{X = X} (Th (V β„“ ΞΉ 𝒦)) ModTh-closure {x = 𝑨} vA {p}{q} x ρ = x 𝑨 vA ρ \end{code} +\fi -It remains to prove the converse inclusion, \af{Mod} (\af{Th} (V 𝒦)) \aof{βŠ†} \af{V} \ab{𝒦}, -which is the main focus of the rest of the paper. We proceed as follows: +It remains to prove the inclusion \af{Mod} (\af{Th} (V 𝒦)) \aof{βŠ†} \af{V} \ab{𝒦}, +and this task occupies the remainder of the paper. We proceed as follows: \begin{enumerate} \item \label{item:1} Let \ab{π‘ͺ} be the product of all algebras in \af{S} \ab{𝒦}, so that \ab{π‘ͺ} \af{∈} \af{P} (\af{S} \ab{𝒦}). From ff85a01ff2f477cb0e12787eba417e3cc395ad5b Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 6 Dec 2021 13:12:07 -0500 Subject: [PATCH 2/3] minor improvements --- doc/TYPES2021/Demos/HSP.tex | 11 ++++------- src/Demos/HSP.lagda | 11 ++++------- 2 files changed, 8 insertions(+), 14 deletions(-) diff --git a/doc/TYPES2021/Demos/HSP.tex b/doc/TYPES2021/Demos/HSP.tex index c68811ff..2ed8d7bc 100644 --- a/doc/TYPES2021/Demos/HSP.tex +++ b/doc/TYPES2021/Demos/HSP.tex @@ -20,10 +20,10 @@ \section{Introduction} To the best of our knowledge, this constitutes the first formalization in MLTT, and the first machine-verified proof, of Birkoff's celebrated 1935 result. -Our first formal proof of the HSP theorem, completed in January of -2021\footnote{See the +Our first proof of the HSP theorem, completed in January of +2021,\footnote{See the \href{https://github.com/ualib/ualib.github.io/blob/71f173858701398d56224dd79d152c380c0c2b5e/src/lagda/UALib/Birkhoff.lagda}{Birkhoff} - module from + module of the \href{https://github.com/ualib/ualib.github.io/commit/71f173858701398d56224dd79d152c380c0c2b5e}{15 Jan 2021 commit (71f1738)} of the \href{https://github.com/ualib/ualib.github.io}{ualib/ualib.gitlab.io} @@ -35,10 +35,7 @@ \section{Introduction} proof and derive a contradiction. To resolve these issues, as well as improve the \agdaalgebras library more generally, we have rewritten parts of the library and have developed a new formal proof of the HSP theorem. We are confident that the new proof, -based on version 2.0.0 of the \agdaalgebras library\footnote{See the -\href{https://github.com/ualib/agda-algebras/commit/ab859caf814566fe32205f76bd0a4ac1e6007147}{30 -Nov 2021 commit (ab859ca)} of the \agdaalgebras library~\cite{ualib_v2.0.0}.} is fully -constructive and correct, a conviction we justify in the course of this presentation. +based on version 2.0.0 of the \agdaalgebras library\footnote{\href{https://github.com/ualib/agda-algebras/commit/ab859caf814566fe32205f76bd0a4ac1e6007147}{30 Nov 2021 commit (ab859ca)} of the \agdaalgebras library~\cite{ualib_v2.0.0}.} is fully constructive and correct, a conviction we justify in due course (q.v.). What follows is a self-contained formal proof of the HSP theorem which is achieved by extracting into a single Agda module a subset of the \agdaalgebras library, including only diff --git a/src/Demos/HSP.lagda b/src/Demos/HSP.lagda index f060a35c..c3bc9d9d 100644 --- a/src/Demos/HSP.lagda +++ b/src/Demos/HSP.lagda @@ -20,10 +20,10 @@ type theory. To the best of our knowledge, this constitutes the first formalization in MLTT, and the first machine-verified proof, of Birkoff's celebrated 1935 result. -Our first formal proof of the HSP theorem, completed in January of -2021\footnote{See the +Our first proof of the HSP theorem, completed in January of +2021,\footnote{See the \href{https://github.com/ualib/ualib.github.io/blob/71f173858701398d56224dd79d152c380c0c2b5e/src/lagda/UALib/Birkhoff.lagda}{Birkhoff} - module from + module of the \href{https://github.com/ualib/ualib.github.io/commit/71f173858701398d56224dd79d152c380c0c2b5e}{15 Jan 2021 commit (71f1738)} of the \href{https://github.com/ualib/ualib.github.io}{ualib/ualib.gitlab.io} @@ -35,10 +35,7 @@ variable symbols---to be just the two element type, then one could combine this proof and derive a contradiction. To resolve these issues, as well as improve the \agdaalgebras library more generally, we have rewritten parts of the library and have developed a new formal proof of the HSP theorem. We are confident that the new proof, -based on version 2.0.0 of the \agdaalgebras library\footnote{See the -\href{https://github.com/ualib/agda-algebras/commit/ab859caf814566fe32205f76bd0a4ac1e6007147}{30 -Nov 2021 commit (ab859ca)} of the \agdaalgebras library~\cite{ualib_v2.0.0}.} is fully -constructive and correct, a conviction we justify in the course of this presentation. +based on version 2.0.0 of the \agdaalgebras library\footnote{\href{https://github.com/ualib/agda-algebras/commit/ab859caf814566fe32205f76bd0a4ac1e6007147}{30 Nov 2021 commit (ab859ca)} of the \agdaalgebras library~\cite{ualib_v2.0.0}.} is fully constructive and correct, a conviction we justify in due course (q.v.). What follows is a self-contained formal proof of the HSP theorem which is achieved by extracting into a single Agda module a subset of the \agdaalgebras library, including only From da7889e5e62be86bdc555dd7216c15d8a0cfa2c0 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 6 Dec 2021 15:00:30 -0500 Subject: [PATCH 3/3] improvements --- doc/TYPES2021/Demos/HSP.tex | 135 +++++++++++++----------------- doc/TYPES2021/acknowledgments.tex | 2 +- src/Demos/HSP.lagda | 111 +++++++++++------------- 3 files changed, 107 insertions(+), 141 deletions(-) diff --git a/doc/TYPES2021/Demos/HSP.tex b/doc/TYPES2021/Demos/HSP.tex index 2ed8d7bc..425cdc24 100644 --- a/doc/TYPES2021/Demos/HSP.tex +++ b/doc/TYPES2021/Demos/HSP.tex @@ -8740,7 +8740,9 @@ \section{Equational Logic} \AgdaPrimitive{Type}\AgdaSpace{}% \AgdaGeneralizable{Ο‡}\AgdaSymbol{\}\{}\AgdaBound{ΞΉ}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% -\AgdaPostulate{Level}\AgdaSymbol{\}\{}\AgdaBound{𝒦}\AgdaSpace{}% +\AgdaPostulate{Level}\AgdaSymbol{\}(}\AgdaBound{β„“}\AgdaSpace{}% +\AgdaSymbol{:}\AgdaSpace{}% +\AgdaPostulate{Level}\AgdaSymbol{)\{}\AgdaBound{𝒦}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaFunction{Pred}\AgdaSymbol{(}\AgdaRecord{Algebra}\AgdaSpace{}% \AgdaGeneralizable{Ξ±}\AgdaSpace{}% @@ -8749,7 +8751,7 @@ \section{Equational Logic} \AgdaGeneralizable{ρᡃ}\AgdaSpace{}% \AgdaOperator{\AgdaPrimitive{βŠ”}}\AgdaSpace{}% \AgdaFunction{ov}\AgdaSpace{}% -\AgdaGeneralizable{β„“}\AgdaSymbol{)\}\{}\AgdaBound{p}\AgdaSpace{}% +\AgdaBound{β„“}\AgdaSymbol{)\}\{}\AgdaBound{p}\AgdaSpace{}% \AgdaBound{q}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaDatatype{Term}\AgdaSpace{}% @@ -9757,9 +9759,9 @@ \section{Free Algebras} \AgdaBound{𝑨}\AgdaSpace{}% \AgdaBound{vkA}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% -\AgdaFunction{V-id1}\AgdaSymbol{\{}\AgdaArgument{β„“}\AgdaSpace{}% -\AgdaSymbol{=}\AgdaSpace{}% -\AgdaBound{β„“}\AgdaSymbol{\}\{}\AgdaArgument{p}\AgdaSpace{}% +\AgdaFunction{V-id1}\AgdaSpace{}% +\AgdaBound{β„“}\AgdaSpace{}% +\AgdaSymbol{\{}\AgdaArgument{p}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaBound{p}\AgdaSymbol{\}\{}\AgdaBound{q}\AgdaSymbol{\}}\AgdaSpace{}% \AgdaSymbol{(}\AgdaFunction{ΞΆ}\AgdaSpace{}% @@ -10111,20 +10113,19 @@ \subsection{Informal proof} The converse assertion---that \emph{every variety is an equational class}---is less obvious. Let \ab{𝒦} be an arbitrary variety. We will describe a set of equations that axiomatizes -\ab{𝒦}. A natural choice is the set -\af{Th} \ab{𝒦} of all equations that hold in \ab{𝒦}. Define \ab{𝒦⁺} = \af{Mod} (\af{Th} -\ab{𝒦}). Clearly, \ab{𝒦} \aof{βŠ†} \ab{𝒦⁺}. We prove the reverse inclusion. Let \ab{𝑨} -\af{∈} \ab{𝒦⁺}; it suffices to find an algebra \ab{𝑭} \af{∈} \af{S} (\af{P} \ab{𝒦}) such -that \ab{𝑨} is a homomorphic image of \ab{𝑭}, as this will show that \ab{𝑨} -\af{∈} \af{H} (\af{S} (\af{P} \ab{𝒦})) = \ab{𝒦}. +\ab{𝒦}. A natural choice is \af{Th} \ab{𝒦}, all equations that hold in \ab{𝒦}. +Let \ab{𝒦⁺} := \af{Mod} (\af{Th} \ab{𝒦}). Clearly, then \ab{𝒦} \aof{βŠ†} \ab{𝒦⁺}. We prove the +reverse inclusion. Let \ab{𝑨} \af{∈} \ab{𝒦⁺}; it suffices to find an algebra \ab{𝑭} \af{∈} +\af{S} (\af{P} \ab{𝒦}) such that \ab{𝑨} is a homomorphic image of \ab{𝑭}, as this will +show that \ab{𝑨} \af{∈} \af{H} (\af{S} (\af{P} \ab{𝒦})) = \ab{𝒦}. Let \ab{X} be such that there exists a \emph{surjective} environment \ab{ρ} : \ab{X} \as{β†’} \af{π•Œ[~\ab{𝑨}~]}. %\footnote{This is usually done by assuming \ab{X} has cardinality at least max(|~\af{π•Œ[~\ab{𝑨}~]}~|, Ο‰).} By the \af{lift-hom} lemma, there is an epimorphism \ab{h} from \T{X} onto \af{π•Œ[~\ab{𝑨}~]} that extends \ab{ρ}. -Now, put \aof{𝔽[~\ab{X}~]}~:=~\T{X}/\ab{Θ}, and let \ab{g} : \T{X} \as{β†’} \aof{𝔽[~\ab{X}~]} -be the natural epimorphism with kernel \ab{Θ}. We claim that \af{ker} \ab g \af{βŠ†} +Now, put \aof{𝔽[~\ab{X}~]}~:=~\T{X}/\afld{β‰ˆ}, and let \ab{g} : \T{X} \as{β†’} \aof{𝔽[~\ab{X}~]} +be the natural epimorphism with kernel \afld{β‰ˆ}. We claim that \af{ker} \ab g \af{βŠ†} \af{ker} \ab h. If the claim is true, then there is a map \ab{f} : \aof{𝔽[~\ab{X}~]} \as{β†’} \ab{𝑨} such that \ab f \af{∘} \ab g = \ab h. Since \ab h is surjective, so is \ab f. Hence \ab{𝑨} \af{∈} \af{𝖧} (\af{𝔽} \ab X) \aof{βŠ†} \ab{𝒦⁺} completing the proof. @@ -10151,9 +10152,7 @@ \subsection{Formal proof} collection \ab{β„°} of equations and then defining \ab{𝒦} = \af{Mod} \ab{β„°}, the equational class determined by \ab{β„°}. We prove that \ab{𝒦} is a variety by showing that \ab{𝒦} = \af{V} \ab{𝒦}. The inclusion \ab{𝒦} \aof{βŠ†} \af V \ab{𝒦}, which holds for all -classes \ab{𝒦}, is called the \defn{expansive} property of \af{V}. The converse inclusion -\af V \ab{𝒦} \aof{βŠ†} \ab{𝒦}, on the other hand, requires the hypothesis that \ab{𝒦} is an -equation class. We now formalize each of these inclusions. +classes \ab{𝒦}, is called the \defn{expansive} property of \af{V}. \ifshort\else \begin{code}% @@ -10368,9 +10367,12 @@ \subsection{Formal proof} \\ \>[0]\<% \end{code} -Earlier we proved the identity preservation lemma, -\af{V-id1} : \ab{𝒦} \aof{⊫} \ab p \aof{β‰ˆ} \ab q \as{β†’} \af{V} \ab{β„“} \ab{ΞΉ} \ab{𝒦} \aof{⊫} \ab p \aof{β‰ˆ} \ab q. -Thus, if \ab{𝒦} is an equational class, then \af V \ab{𝒦} \aof{βŠ†} \ab{𝒦}, as we now confirm. + +The converse inclusion, \af V \ab{𝒦} \aof{βŠ†} \ab{𝒦}, requires the +hypothesis that \ab{𝒦} is an equation class. Recall lemma +\af{V-id1}, which asserts that \ab{𝒦} \aof{⊫} \ab p \aof{β‰ˆ} \ab q implies \af{V} +\ab{β„“} \ab{ΞΉ} \ab{𝒦} \aof{⊫} \ab p \aof{β‰ˆ} \ab q. Whence, if \ab{𝒦} is an equational +class, then \af V \ab{𝒦} \aof{βŠ†} \ab{𝒦}, as we now confirm. \begin{code}% \>[0]\<% @@ -10426,11 +10428,9 @@ \subsection{Formal proof} \AgdaBound{pβ„°q}\AgdaSpace{}% \AgdaBound{ρ}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% -\AgdaFunction{V-id1}\AgdaSymbol{\{}\AgdaArgument{β„“}\AgdaSpace{}% -\AgdaSymbol{=}\AgdaSpace{}% -\AgdaBound{β„“}\AgdaSymbol{\}\{}\AgdaArgument{𝒦}\AgdaSpace{}% -\AgdaSymbol{=}\AgdaSpace{}% -\AgdaFunction{𝒦}\AgdaSymbol{\}\{}\AgdaBound{p}\AgdaSymbol{\}\{}\AgdaBound{q}\AgdaSymbol{\}(Ξ»}\AgdaSpace{}% +\AgdaFunction{V-id1}\AgdaSpace{}% +\AgdaBound{β„“}\AgdaSpace{}% +\AgdaSymbol{\{}\AgdaFunction{𝒦}\AgdaSymbol{\}\{}\AgdaBound{p}\AgdaSymbol{\}\{}\AgdaBound{q}\AgdaSymbol{\}(Ξ»}\AgdaSpace{}% \AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}% \AgdaBound{x}\AgdaSpace{}% \AgdaBound{Ο„}\AgdaSpace{}% @@ -10553,8 +10553,8 @@ \subsection{Formal proof} To define \ab{π‘ͺ} as the product of all algebras in \af{S} \ab{𝒦}, we must first contrive an index type for the class \af{S} \ab{𝒦}. We do so by letting the indices be the algebras belonging to \ab{𝒦}. Actually, each index will consist of a triple (\ab{𝑨} , \ab p , -\ab{ρ}) where \ab{𝑨} is an algebra, \ab p : \ab{𝑨} \af{∈} \af{S} \ab{𝒦}) is a proof of membership in \ab{𝒦}, -\ab{ρ} : \ab X \as{β†’} \aof{π•Œ[ \ab{𝑨} ]} is an arbitrary environment. +\ab{ρ}) where \ab{𝑨} is an algebra, \ab p : \ab{𝑨} \af{∈} \af{S} \ab{𝒦} is a proof of membership in \ab{𝒦}, +and \ab{ρ} : \ab X \as{β†’} \aof{π•Œ[ \ab{𝑨} ]} is an arbitrary environment. Using this indexing scheme, we construct \ab{π‘ͺ}, the product of all algebras in \ab{𝒦} and all environments, as follows. @@ -10595,13 +10595,13 @@ \subsection{Formal proof} \>[0]\<% \\ % -\>[1]\AgdaFunction{ℑ⁺}\AgdaSpace{}% +\>[1]\AgdaFunction{β„‘}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaPrimitive{Type}\AgdaSpace{}% \AgdaFunction{ΞΉ}\<% \\ % -\>[1]\AgdaFunction{ℑ⁺}\AgdaSpace{}% +\>[1]\AgdaFunction{β„‘}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaFunction{Ξ£[}\AgdaSpace{}% \AgdaBound{𝑨}\AgdaSpace{}% @@ -10624,16 +10624,16 @@ \subsection{Formal proof} % \\[\AgdaEmptyExtraSkip]% % -\>[1]\AgdaFunction{𝔄⁺}\AgdaSpace{}% +\>[1]\AgdaFunction{𝔄}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% -\AgdaFunction{ℑ⁺}\AgdaSpace{}% +\AgdaFunction{β„‘}\AgdaSpace{}% \AgdaSymbol{β†’}\AgdaSpace{}% \AgdaRecord{Algebra}\AgdaSpace{}% \AgdaBound{Ξ±}\AgdaSpace{}% \AgdaBound{ρᡃ}\<% \\ % -\>[1]\AgdaFunction{𝔄⁺}\AgdaSpace{}% +\>[1]\AgdaFunction{𝔄}\AgdaSpace{}% \AgdaBound{i}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{∣}}\AgdaSpace{}% @@ -10653,7 +10653,7 @@ \subsection{Formal proof} \>[1]\AgdaFunction{π‘ͺ}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaFunction{β¨…}\AgdaSpace{}% -\AgdaFunction{𝔄⁺}\<% +\AgdaFunction{𝔄}\<% \end{code} \ifshort\else @@ -10665,7 +10665,7 @@ \subsection{Formal proof} \AgdaSymbol{:}\AgdaSpace{}% \AgdaSymbol{(}\AgdaBound{i}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% -\AgdaFunction{ℑ⁺}\AgdaSymbol{)}\AgdaSpace{}% +\AgdaFunction{β„‘}\AgdaSymbol{)}\AgdaSpace{}% \AgdaSymbol{β†’}\AgdaSpace{}% \AgdaSymbol{βˆ€\{}\AgdaBound{p}\AgdaSpace{}% \AgdaBound{q}\AgdaSymbol{\}}\AgdaSpace{}% @@ -10701,7 +10701,7 @@ \subsection{Formal proof} \AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{Setoid}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% -\AgdaFunction{𝔄⁺}\AgdaSpace{}% +\AgdaFunction{𝔄}\AgdaSpace{}% \AgdaBound{i}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{]}}\AgdaSpace{}% \AgdaKeyword{using}\AgdaSpace{}% @@ -10711,7 +10711,7 @@ \subsection{Formal proof} \AgdaSymbol{;}\AgdaSpace{}% \AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{Environment}\AgdaSpace{}% -\AgdaSymbol{(}\AgdaFunction{𝔄⁺}\AgdaSpace{}% +\AgdaSymbol{(}\AgdaFunction{𝔄}\AgdaSpace{}% \AgdaBound{i}\AgdaSymbol{)}\AgdaSpace{}% \AgdaKeyword{using}\AgdaSpace{}% \AgdaSymbol{(}\AgdaSpace{}% @@ -10746,7 +10746,7 @@ \subsection{Formal proof} \>[1]\AgdaFunction{homC}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaFunction{β¨…-hom-co}\AgdaSpace{}% -\AgdaFunction{𝔄⁺}\AgdaSpace{}% +\AgdaFunction{𝔄}\AgdaSpace{}% \AgdaSymbol{(Ξ»}\AgdaSpace{}% \AgdaBound{i}\AgdaSpace{}% \AgdaSymbol{β†’}\AgdaSpace{}% @@ -10982,13 +10982,13 @@ \subsection{Formal proof} \>[0]\<% \end{code} If \AgdaPair{p}{q} belongs to the kernel of \af{homC}, then -\af{Th} \ab{𝒦} includes the identity \ab{p} \af{β‰ˆ} \ab{q}---that is, -\af{Th} \ab{𝒦} \af{⊒} \ab X \af{β–Ή} \ab{p} \af{β‰ˆ} \ab{q}. Equivalently, -if the kernel of \af{homC} is contained in that of \af{homF[ X ]}. +\af{Th} \ab{𝒦} includes the identity \ab{p} \af{β‰ˆ} \ab{q}. +%---that is, \af{Th} \ab{𝒦} \af{⊒} \ab X \af{β–Ή} \ab{p} \af{β‰ˆ} \ab{q}. +Equivalently, +the kernel of \af{homC} is contained in that of \af{homF[ X ]}. \ifshort We omit the proof of this lemma and merely display its formal statement. \else -We formalize this fact as follows. \fi \begin{code}% @@ -11130,9 +11130,9 @@ \subsection{Formal proof} % \>[3]\AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{Environment}\AgdaSpace{}% -\AgdaSymbol{(}\AgdaFunction{𝔄⁺}\AgdaSpace{}% +\AgdaSymbol{(}\AgdaFunction{𝔄}\AgdaSpace{}% \AgdaBound{i}\AgdaSymbol{)}% -\>[28]\AgdaKeyword{using}\AgdaSpace{}% +\>[27]\AgdaKeyword{using}\AgdaSpace{}% \AgdaSymbol{(}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧}}\AgdaSpace{}% \AgdaSymbol{)}\<% @@ -11141,10 +11141,10 @@ \subsection{Formal proof} \>[3]\AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{Setoid}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% -\AgdaFunction{𝔄⁺}\AgdaSpace{}% +\AgdaFunction{𝔄}\AgdaSpace{}% \AgdaBound{i}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{]}}% -\>[28]\AgdaKeyword{using}\AgdaSpace{}% +\>[27]\AgdaKeyword{using}\AgdaSpace{}% \AgdaSymbol{(}\AgdaSpace{}% \AgdaOperator{\AgdaField{\AgdaUnderscore{}β‰ˆ\AgdaUnderscore{}}}\AgdaSpace{}% \AgdaSymbol{;}\AgdaSpace{}% @@ -11510,9 +11510,9 @@ \subsection{Formal proof} % \>[2]\AgdaFunction{psC}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% -\AgdaFunction{ℑ⁺}\AgdaSpace{}% +\AgdaFunction{β„‘}\AgdaSpace{}% \AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}% -\AgdaSymbol{(}\AgdaFunction{𝔄⁺}\AgdaSpace{}% +\AgdaSymbol{(}\AgdaFunction{𝔄}\AgdaSpace{}% \AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}% \AgdaSymbol{((Ξ»}\AgdaSpace{}% \AgdaBound{i}\AgdaSpace{}% @@ -11756,9 +11756,7 @@ \subsection{Formal proof} %% ----------------------------------------------------------------------------- \section{Related work} There have been a number of efforts to formalize parts of universal algebra in -type theory besides ours% -\ifshort -. +type theory besides ours. In~\cite{Capretta:1999}, Capretta formalized the basics of universal algebra in the Calculus of Inductive Constructions using the Coq proof assistant. In~\cite{Spitters:2011}, Spitters and van der Weegen formalized the basics of universal algebra @@ -11771,33 +11769,18 @@ \section{Related work} coverage is less extensive than that of \agdaalgebras, Gunther et al do treat \emph{multi-sorted} algebras, whereas \agdaalgebras is currently limited to single sorted structures. -In~\cite{Amato:2021}, ``Amato et al formalize multi-sorted algebras with finitary - operators in UniMath. Limiting to finitary operators is due to the restrictions of the - UniMath type theory, which does not have W-types nor user-defined inductive types. - These restrictions also prompt the authors to code terms as lists of stack machine - instructions rather than trees'' (quoting~\cite{Abel:2021}). -In~\cite{Lynge:2019}, ``Lynge and Spitters formalize multi-sorted algebras in HoTT, also - restricting to finitary operators. Using HoTT they can define quotients as - types,obsoleting setoids. They prove three isomorphism theorems concerning sub- and - quotient algebras. A universal algebra or varieties are not formalized'' (quoting~\cite{Abel:2021}). -In~\cite{Abel:2021}, Abel gives a new formal proof of the soundness theorem and Birkhoff's - completeness theorem for multi-sorted algebraic structures. -\else -, most notably -\begin{enumerate} -\item -In~\cite{Capretta:1999}, Capretta formalized the basics of universal algebra in the - Calculus of Inductive Constructions using the Coq proof assistant; -\item In~\cite{Spitters:2011}, Spitters and van der Weegen formalized the basics of universal algebra - and some classical algebraic structures, also in the Calculus of Inductive Constructions using - the Coq proof assistant and promoting the use of type classes; -\item In~\cite{Gunther:2018} Gunther et al developed what seemed (prior to the \agdaalgebras library) to be - the most extensive library of formalized universal algebra to date; like \agdaalgebras, that work is based on dependent type theory, is programmed in Agda, and goes beyond the Noether isomorphism theorems to include some basic equational logic; although the coverage is less extensive than that of \agdaalgebras, Gunther et al do treat \emph{multi-sorted} algebras, whereas \agdaalgebras is currently limited to single sorted structures. - \item In~\cite{Amato:2021}, ``Amato et al formalize multi-sorted algebras with finitary operators in UniMath. Limiting to finitary operators is due to the restrictions of the UniMath type theory, which does not have W-types nor user-defined inductive types. These restrictions also prompt the authors to code terms as lists of stack machine instructions rather than trees'' (quoting~\cite{Abel:2021}). -\item In~\cite{Lynge:2019}, ``Lynge and Spitters formalize multi-sorted algebras in HoTT, also restricting to finitary operators. Using HoTT they can define quotients as types, obsoleting setoids. They prove three isomorphism theorems concerning sub- and quotient algebras. A universal algebra or varieties are not formalized'' (quoting~\cite{Abel:2021}). -\item In~\cite{Abel:2021}, Abel gives a new formal proof of the soundness theorem and Birkhoff's completeness theorem for multi-sorted algebraic structures. -\end{enumerate} -\fi + +As noted by Abel~\cite{Abel:2021}, Amato et al, in \cite{Amato:2021}, have + formalized multi-sorted algebras with finitary operators in UniMath. The restriction to + finitary operations was due to limitations of the UniMath type theory, which does + not have W-types nor user-defined inductive types. +Abel also notes that Lynge and Spitters, in~\cite{Lynge:2019}, formalize multi-sorted + algebras with finitary operators in \emph{Homotopy type theory} (\cite{HoTT}) using + Coq. HoTT's higher inductive types enable them to define quotients as types, without + the need for setoids. Lynge and Spitters prove three isomorphism theorems concerning + subalgebras and quotient algebras, but do not formalize universal algebras nor varieties. +Finally, in~\cite{Abel:2021}, Abel gives a new formal proof of the soundness theorem and + Birkhoff's completeness theorem for multi-sorted algebraic structures. %Some other projects aimed at formalizing mathematics generally, and algebra in particular, have developed into very extensive libraries that include definitions, theorems, and proofs about algebraic structures, such as groups, rings, modules, etc. However, the goals of these efforts seem to be the formalization of special classical algebraic structures, as opposed to the general theory of (universal) algebras. Moreover, the part of universal algebra and equational logic formalized in the \agdaalgebras library extends beyond the scope of prior efforts. diff --git a/doc/TYPES2021/acknowledgments.tex b/doc/TYPES2021/acknowledgments.tex index 77657f0b..b6cbe9e6 100644 --- a/doc/TYPES2021/acknowledgments.tex +++ b/doc/TYPES2021/acknowledgments.tex @@ -6,7 +6,7 @@ % VΓ­ctor LΓ³pez Juan, Ulf Norell, AndrΓ©s Sicard-RamΓ­rez,Andrea Vezzosi, and Tesla Ice Zhang) % , maintained by Matthew Daggitt and Guillaume Allais. Most of the content of this paper was generated from the literate \agda file \HSPlagda and the \LaTeXe file \agdahsp (processed with the commands -\texttt{agda --latex} and \texttt{pdflatex}), which are available in the \agdaalgebras GitHub repository~\cite{ualib_v2.0.0}. +\texttt{agda --latex} and \texttt{pdflatex}, respectively), which are available in the \agdaalgebras GitHub repository~\cite{ualib_v2.0.0}. The first author was supported by the CoCoSym Project under the ERC Consolidator Grant (ERC CoG), No. 771005. diff --git a/src/Demos/HSP.lagda b/src/Demos/HSP.lagda index c3bc9d9d..b7211281 100644 --- a/src/Demos/HSP.lagda +++ b/src/Demos/HSP.lagda @@ -1903,7 +1903,7 @@ In each case, we will only need the first implication, so we omit the others fro IH : β¨… π’œ ⊧ p β‰ˆ q IH = ⊧-P-invar π’œ {p}{q} (Ξ» i β†’ Οƒ (π’œ i) (kA i)) -module _ {X : Type Ο‡}{ΞΉ : Level}{𝒦 : Pred(Algebra Ξ± ρᡃ)(Ξ± βŠ” ρᡃ βŠ” ov β„“)}{p q : Term X} where +module _ {X : Type Ο‡}{ΞΉ : Level}(β„“ : Level){𝒦 : Pred(Algebra Ξ± ρᡃ)(Ξ± βŠ” ρᡃ βŠ” ov β„“)}{p q : Term X} where private aβ„“ΞΉ = Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ V-id1 : 𝒦 ⊫ p β‰ˆ q β†’ V β„“ ΞΉ 𝒦 ⊫ p β‰ˆ q @@ -2123,7 +2123,7 @@ module FreeHom {𝒦 : Pred(Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“)} where homF[ X ] = IsEpi.HomReduct βˆ₯ epiF[ X ] βˆ₯ kernel-in-theory : {X : Type c} β†’ ker ∣ homF[ X ] ∣ βŠ† Th (V β„“ ΞΉ 𝒦) - kernel-in-theory {X = X} {p , q} pKq 𝑨 vkA = V-id1{β„“ = β„“}{p = p}{q} (ΞΆ pKq) 𝑨 vkA + kernel-in-theory {X = X} {p , q} pKq 𝑨 vkA = V-id1 β„“ {p = p}{q} (ΞΆ pKq) 𝑨 vkA where ΞΆ : βˆ€{p q} β†’ (Th 𝒦) ⊒ X β–Ή p β‰ˆ q β†’ 𝒦 ⊫ p β‰ˆ q ΞΆ x 𝑨 kA = sound (Ξ» y ρ β†’ y 𝑨 kA ρ) x where open Soundness (Th 𝒦) 𝑨 @@ -2197,20 +2197,19 @@ class axiomatized by the set \ab{β„°} of term identities; that is, \ab{𝑨} ∈ The converse assertion---that \emph{every variety is an equational class}---is less obvious. Let \ab{𝒦} be an arbitrary variety. We will describe a set of equations that axiomatizes -\ab{𝒦}. A natural choice is the set -\af{Th} \ab{𝒦} of all equations that hold in \ab{𝒦}. Define \ab{𝒦⁺} = \af{Mod} (\af{Th} -\ab{𝒦}). Clearly, \ab{𝒦} \aof{βŠ†} \ab{𝒦⁺}. We prove the reverse inclusion. Let \ab{𝑨} -\af{∈} \ab{𝒦⁺}; it suffices to find an algebra \ab{𝑭} \af{∈} \af{S} (\af{P} \ab{𝒦}) such -that \ab{𝑨} is a homomorphic image of \ab{𝑭}, as this will show that \ab{𝑨} -\af{∈} \af{H} (\af{S} (\af{P} \ab{𝒦})) = \ab{𝒦}. +\ab{𝒦}. A natural choice is \af{Th} \ab{𝒦}, all equations that hold in \ab{𝒦}. +Let \ab{𝒦⁺} := \af{Mod} (\af{Th} \ab{𝒦}). Clearly, then \ab{𝒦} \aof{βŠ†} \ab{𝒦⁺}. We prove the +reverse inclusion. Let \ab{𝑨} \af{∈} \ab{𝒦⁺}; it suffices to find an algebra \ab{𝑭} \af{∈} +\af{S} (\af{P} \ab{𝒦}) such that \ab{𝑨} is a homomorphic image of \ab{𝑭}, as this will +show that \ab{𝑨} \af{∈} \af{H} (\af{S} (\af{P} \ab{𝒦})) = \ab{𝒦}. Let \ab{X} be such that there exists a \emph{surjective} environment \ab{ρ} : \ab{X} \as{β†’} \af{π•Œ[~\ab{𝑨}~]}. %\footnote{This is usually done by assuming \ab{X} has cardinality at least max(|~\af{π•Œ[~\ab{𝑨}~]}~|, Ο‰).} By the \af{lift-hom} lemma, there is an epimorphism \ab{h} from \T{X} onto \af{π•Œ[~\ab{𝑨}~]} that extends \ab{ρ}. -Now, put \aof{𝔽[~\ab{X}~]}~:=~\T{X}/\ab{Θ}, and let \ab{g} : \T{X} \as{β†’} \aof{𝔽[~\ab{X}~]} -be the natural epimorphism with kernel \ab{Θ}. We claim that \af{ker} \ab g \af{βŠ†} +Now, put \aof{𝔽[~\ab{X}~]}~:=~\T{X}/\afld{β‰ˆ}, and let \ab{g} : \T{X} \as{β†’} \aof{𝔽[~\ab{X}~]} +be the natural epimorphism with kernel \afld{β‰ˆ}. We claim that \af{ker} \ab g \af{βŠ†} \af{ker} \ab h. If the claim is true, then there is a map \ab{f} : \aof{𝔽[~\ab{X}~]} \as{β†’} \ab{𝑨} such that \ab f \af{∘} \ab g = \ab h. Since \ab h is surjective, so is \ab f. Hence \ab{𝑨} \af{∈} \af{𝖧} (\af{𝔽} \ab X) \aof{βŠ†} \ab{𝒦⁺} completing the proof. @@ -2237,9 +2236,7 @@ For (i), we need an arbitrary equational class, which we obtain by starting with collection \ab{β„°} of equations and then defining \ab{𝒦} = \af{Mod} \ab{β„°}, the equational class determined by \ab{β„°}. We prove that \ab{𝒦} is a variety by showing that \ab{𝒦} = \af{V} \ab{𝒦}. The inclusion \ab{𝒦} \aof{βŠ†} \af V \ab{𝒦}, which holds for all -classes \ab{𝒦}, is called the \defn{expansive} property of \af{V}. The converse inclusion -\af V \ab{𝒦} \aof{βŠ†} \ab{𝒦}, on the other hand, requires the hypothesis that \ab{𝒦} is an -equation class. We now formalize each of these inclusions. +classes \ab{𝒦}, is called the \defn{expansive} property of \af{V}. \ifshort\else \begin{code} @@ -2268,16 +2265,19 @@ module _ (𝒦 : Pred(Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“)){X : Type (Ξ± Goal = mkiso (toβ¨… , mkhom reflβ¨…) (fromβ¨… , mkhom refl) (Ξ» _ _ β†’ refl) (Ξ» _ β†’ refl) \end{code} -Earlier we proved the identity preservation lemma, -\af{V-id1} : \ab{𝒦} \aof{⊫} \ab p \aof{β‰ˆ} \ab q \as{β†’} \af{V} \ab{β„“} \ab{ΞΉ} \ab{𝒦} \aof{⊫} \ab p \aof{β‰ˆ} \ab q. -Thus, if \ab{𝒦} is an equational class, then \af V \ab{𝒦} \aof{βŠ†} \ab{𝒦}, as we now confirm. + +The converse inclusion, \af V \ab{𝒦} \aof{βŠ†} \ab{𝒦}, requires the +hypothesis that \ab{𝒦} is an equation class. Recall lemma +\af{V-id1}, which asserts that \ab{𝒦} \aof{⊫} \ab p \aof{β‰ˆ} \ab q implies \af{V} +\ab{β„“} \ab{ΞΉ} \ab{𝒦} \aof{⊫} \ab p \aof{β‰ˆ} \ab q. Whence, if \ab{𝒦} is an equational +class, then \af V \ab{𝒦} \aof{βŠ†} \ab{𝒦}, as we now confirm. \begin{code} module _ {β„“ : Level}{X : Type β„“}{β„° : {Y : Type β„“} β†’ Pred (Term Y Γ— Term Y) (ov β„“)} where private 𝒦 = Mod{Ξ± = β„“}{β„“}{X} β„° -- an arbitrary equational class EqClβ‡’Var : V β„“ (ov β„“) 𝒦 βŠ† 𝒦 - EqClβ‡’Var {𝑨}vA{p}{q} pβ„°q ρ = V-id1{β„“ = β„“}{𝒦 = 𝒦}{p}{q}(Ξ» _ x Ο„ β†’ x pβ„°q Ο„)𝑨 vA ρ + EqClβ‡’Var {𝑨}vA{p}{q} pβ„°q ρ = V-id1 β„“ {𝒦}{p}{q}(Ξ» _ x Ο„ β†’ x pβ„°q Ο„)𝑨 vA ρ \end{code} Together, \af{V-expa} and \af{Eqclβ‡’Var} prove that every equational class is a variety. @@ -2321,8 +2321,8 @@ and this task occupies the remainder of the paper. We proceed as follows: To define \ab{π‘ͺ} as the product of all algebras in \af{S} \ab{𝒦}, we must first contrive an index type for the class \af{S} \ab{𝒦}. We do so by letting the indices be the algebras belonging to \ab{𝒦}. Actually, each index will consist of a triple (\ab{𝑨} , \ab p , -\ab{ρ}) where \ab{𝑨} is an algebra, \ab p : \ab{𝑨} \af{∈} \af{S} \ab{𝒦}) is a proof of membership in \ab{𝒦}, -\ab{ρ} : \ab X \as{β†’} \aof{π•Œ[ \ab{𝑨} ]} is an arbitrary environment. +\ab{ρ}) where \ab{𝑨} is an algebra, \ab p : \ab{𝑨} \af{∈} \af{S} \ab{𝒦} is a proof of membership in \ab{𝒦}, +and \ab{ρ} : \ab X \as{β†’} \aof{π•Œ[ \ab{𝑨} ]} is an arbitrary environment. Using this indexing scheme, we construct \ab{π‘ͺ}, the product of all algebras in \ab{𝒦} and all environments, as follows. @@ -2336,22 +2336,22 @@ and all environments, as follows. \fi \begin{code} - ℑ⁺ : Type ΞΉ - ℑ⁺ = Ξ£[ 𝑨 ∈ (Algebra Ξ± ρᡃ) ] (𝑨 ∈ S β„“ 𝒦) Γ— (Carrier (Env 𝑨 X)) + β„‘ : Type ΞΉ + β„‘ = Ξ£[ 𝑨 ∈ (Algebra Ξ± ρᡃ) ] (𝑨 ∈ S β„“ 𝒦) Γ— (Carrier (Env 𝑨 X)) - 𝔄⁺ : ℑ⁺ β†’ Algebra Ξ± ρᡃ - 𝔄⁺ i = ∣ i ∣ + 𝔄 : β„‘ β†’ Algebra Ξ± ρᡃ + 𝔄 i = ∣ i ∣ π‘ͺ : Algebra ΞΉ ΞΉ - π‘ͺ = β¨… 𝔄⁺ + π‘ͺ = β¨… 𝔄 \end{code} \ifshort\else \begin{code} - skEqual : (i : ℑ⁺) β†’ βˆ€{p q} β†’ Type ρᡃ + skEqual : (i : β„‘) β†’ βˆ€{p q} β†’ Type ρᡃ skEqual i {p}{q} = ⟦ p ⟧ ⟨$⟩ snd βˆ₯ i βˆ₯ β‰ˆ ⟦ q ⟧ ⟨$⟩ snd βˆ₯ i βˆ₯ - where open Setoid 𝔻[ 𝔄⁺ i ] using ( _β‰ˆ_ ) ; open Environment (𝔄⁺ i) using ( ⟦_⟧ ) + where open Setoid 𝔻[ 𝔄 i ] using ( _β‰ˆ_ ) ; open Environment (𝔄 i) using ( ⟦_⟧ ) \end{code} The type \af{skEqual} provides a term identity \ab p \af{β‰ˆ} \ab q for each index \ab i = (\ab{𝑨} , \ab{p} , \ab{ρ}) of the product. @@ -2368,7 +2368,7 @@ so belongs to \af S (\af P \ab{𝒦}). \begin{code} homC : hom (𝑻 X) π‘ͺ - homC = β¨…-hom-co 𝔄⁺ (Ξ» i β†’ lift-hom (snd βˆ₯ i βˆ₯)) + homC = β¨…-hom-co 𝔄 (Ξ» i β†’ lift-hom (snd βˆ₯ i βˆ₯)) \end{code} \ifshort\else \begin{code} @@ -2397,13 +2397,13 @@ so belongs to \af S (\af P \ab{𝒦}). \end{code} If \AgdaPair{p}{q} belongs to the kernel of \af{homC}, then -\af{Th} \ab{𝒦} includes the identity \ab{p} \af{β‰ˆ} \ab{q}---that is, -\af{Th} \ab{𝒦} \af{⊒} \ab X \af{β–Ή} \ab{p} \af{β‰ˆ} \ab{q}. Equivalently, -if the kernel of \af{homC} is contained in that of \af{homF[ X ]}. +\af{Th} \ab{𝒦} includes the identity \ab{p} \af{β‰ˆ} \ab{q}. +%---that is, \af{Th} \ab{𝒦} \af{⊒} \ab X \af{β–Ή} \ab{p} \af{β‰ˆ} \ab{q}. +Equivalently, +the kernel of \af{homC} is contained in that of \af{homF[ X ]}. \ifshort We omit the proof of this lemma and merely display its formal statement. \else -We formalize this fact as follows. \fi \begin{code} @@ -2424,8 +2424,8 @@ We formalize this fact as follows. pqEqual : βˆ€ i β†’ skEqual i {p}{q} pqEqual i = goal where - open Environment (𝔄⁺ i) using ( ⟦_⟧ ) - open Setoid 𝔻[ 𝔄⁺ i ] using ( _β‰ˆ_ ; sym ; trans ) + open Environment (𝔄 i) using ( ⟦_⟧ ) + open Setoid 𝔻[ 𝔄 i ] using ( _β‰ˆ_ ; sym ; trans ) goal : ⟦ p ⟧ ⟨$⟩ snd βˆ₯ i βˆ₯ β‰ˆ ⟦ q ⟧ ⟨$⟩ snd βˆ₯ i βˆ₯ goal = trans (free-lift-interp{𝑨 = ∣ i ∣}(snd βˆ₯ i βˆ₯) p) ( trans (pKq i)(sym (free-lift-interp{𝑨 = ∣ i ∣} (snd βˆ₯ i βˆ₯) q))) @@ -2484,7 +2484,7 @@ With this we can prove that \Free{X} belongs to \af{S} (\af{P} \ab{𝒦}). SPF = ∣ spC ∣ , (fst βˆ₯ spC βˆ₯) , (≀-transitive F≀C (snd βˆ₯ spC βˆ₯)) where psC : π‘ͺ ∈ P (Ξ± βŠ” ρᡃ βŠ” β„“) ΞΉ (S β„“ 𝒦) - psC = ℑ⁺ , (𝔄⁺ , ((Ξ» i β†’ fst βˆ₯ i βˆ₯) , β‰…-refl)) + psC = β„‘ , (𝔄 , ((Ξ» i β†’ fst βˆ₯ i βˆ₯) , β‰…-refl)) spC : π‘ͺ ∈ S ΞΉ (P β„“ ΞΉ 𝒦) spC = PSβŠ†SP psC @@ -2521,9 +2521,7 @@ Thus, every variety is an equational class. This completes the formal proof of B %% ----------------------------------------------------------------------------- \section{Related work} There have been a number of efforts to formalize parts of universal algebra in -type theory besides ours% -\ifshort -. +type theory besides ours. In~\cite{Capretta:1999}, Capretta formalized the basics of universal algebra in the Calculus of Inductive Constructions using the Coq proof assistant. In~\cite{Spitters:2011}, Spitters and van der Weegen formalized the basics of universal algebra @@ -2536,33 +2534,18 @@ In~\cite{Gunther:2018} Gunther et al developed what seemed (prior to the \agdaal coverage is less extensive than that of \agdaalgebras, Gunther et al do treat \emph{multi-sorted} algebras, whereas \agdaalgebras is currently limited to single sorted structures. -In~\cite{Amato:2021}, ``Amato et al formalize multi-sorted algebras with finitary - operators in UniMath. Limiting to finitary operators is due to the restrictions of the - UniMath type theory, which does not have W-types nor user-defined inductive types. - These restrictions also prompt the authors to code terms as lists of stack machine - instructions rather than trees'' (quoting~\cite{Abel:2021}). -In~\cite{Lynge:2019}, ``Lynge and Spitters formalize multi-sorted algebras in HoTT, also - restricting to finitary operators. Using HoTT they can define quotients as - types,obsoleting setoids. They prove three isomorphism theorems concerning sub- and - quotient algebras. A universal algebra or varieties are not formalized'' (quoting~\cite{Abel:2021}). -In~\cite{Abel:2021}, Abel gives a new formal proof of the soundness theorem and Birkhoff's - completeness theorem for multi-sorted algebraic structures. -\else -, most notably -\begin{enumerate} -\item -In~\cite{Capretta:1999}, Capretta formalized the basics of universal algebra in the - Calculus of Inductive Constructions using the Coq proof assistant; -\item In~\cite{Spitters:2011}, Spitters and van der Weegen formalized the basics of universal algebra - and some classical algebraic structures, also in the Calculus of Inductive Constructions using - the Coq proof assistant and promoting the use of type classes; -\item In~\cite{Gunther:2018} Gunther et al developed what seemed (prior to the \agdaalgebras library) to be - the most extensive library of formalized universal algebra to date; like \agdaalgebras, that work is based on dependent type theory, is programmed in Agda, and goes beyond the Noether isomorphism theorems to include some basic equational logic; although the coverage is less extensive than that of \agdaalgebras, Gunther et al do treat \emph{multi-sorted} algebras, whereas \agdaalgebras is currently limited to single sorted structures. - \item In~\cite{Amato:2021}, ``Amato et al formalize multi-sorted algebras with finitary operators in UniMath. Limiting to finitary operators is due to the restrictions of the UniMath type theory, which does not have W-types nor user-defined inductive types. These restrictions also prompt the authors to code terms as lists of stack machine instructions rather than trees'' (quoting~\cite{Abel:2021}). -\item In~\cite{Lynge:2019}, ``Lynge and Spitters formalize multi-sorted algebras in HoTT, also restricting to finitary operators. Using HoTT they can define quotients as types, obsoleting setoids. They prove three isomorphism theorems concerning sub- and quotient algebras. A universal algebra or varieties are not formalized'' (quoting~\cite{Abel:2021}). -\item In~\cite{Abel:2021}, Abel gives a new formal proof of the soundness theorem and Birkhoff's completeness theorem for multi-sorted algebraic structures. -\end{enumerate} -\fi + +As noted by Abel~\cite{Abel:2021}, Amato et al, in \cite{Amato:2021}, have + formalized multi-sorted algebras with finitary operators in UniMath. The restriction to + finitary operations was due to limitations of the UniMath type theory, which does + not have W-types nor user-defined inductive types. +Abel also notes that Lynge and Spitters, in~\cite{Lynge:2019}, formalize multi-sorted + algebras with finitary operators in \emph{Homotopy type theory} (\cite{HoTT}) using + Coq. HoTT's higher inductive types enable them to define quotients as types, without + the need for setoids. Lynge and Spitters prove three isomorphism theorems concerning + subalgebras and quotient algebras, but do not formalize universal algebras nor varieties. +Finally, in~\cite{Abel:2021}, Abel gives a new formal proof of the soundness theorem and + Birkhoff's completeness theorem for multi-sorted algebraic structures. %Some other projects aimed at formalizing mathematics generally, and algebra in particular, have developed into very extensive libraries that include definitions, theorems, and proofs about algebraic structures, such as groups, rings, modules, etc. However, the goals of these efforts seem to be the formalization of special classical algebraic structures, as opposed to the general theory of (universal) algebras. Moreover, the part of universal algebra and equational logic formalized in the \agdaalgebras library extends beyond the scope of prior efforts.