small changes to tex

jfla-paper/fereegooliglesiasvazquez2024.tex

@@ -104,7 +104,7 @@ \section{Introduction}
 Here, by a propositional \emph{formula} we mean any term built from variables, here denoted by letters $p, q, \dots$, using binary operations $\vee, \wedge, \to$, and a nullary operation $\bot$. Alternatively, one may think of such a formula as a type in a simply typed $\lambda$-calculus with zero, sum, and product types. Throughout the paper, by \emph{equivalence} of two formulas $\phi$ and $\phi'$ we mean that the formula $(\phi \to \phi') \wedge (\phi' \to \phi)$ is provable, or, on the other side of the Curry-Howard isomorphism, inhabited. The precise definition of the adjective `simpler' in (\ref{eq:question}) that we use here depends on a function associating to each formula a natural number, its \emph{weight}. We give the function in~\cref{dfn:weight} below; for now, it suffices to say that it satisfies the intuitive property that shorter formulas have lower weight.
 
 Since intuitionistic equivalence is decidable, there evidently exists a simplest formula in any equivalence class, and such a formula is computable by a brute-force enumeration. However, we here seek a practically feasible, and provably correct, answer to the question (\ref{eq:question}).
-The immediate origin of the question, for us, lies in a verified Coq/Rocq implementation by the first and second author~\cite{FerGoo2023} of Pitts' procedure~\cite{Pit1992} for computing propositional quantifiers in intuitionistic logic \footnote{\url{https://github.com/hferee/UIML}}. Given a propositional formula $\phi$ and a propositional variable $p$, the formulas $\exists p. \phi$ and $\forall p. \phi$ are abstractly defined by the usual rules of quantification, see~\cref{dfn:prop-quantifiers}. The surprising result of~\cite{Pit1992} is that for any $\phi$, there actually exist \emph{propositional} formulas $\Ep{\phi}$ and $\Ap{\phi}$ that are equivalent to $\exists p. \phi$ and $\forall p. \phi$, respectively. This implies in particular that second-order propositional quantifiers may in fact be encoded, up to equivalence, in the zero-order fragment. Pitts' theorem has many consequences for higher-order intuitionistic logic, including a uniform interpolation theorem and the existence of a model completion for the class of Heyting algebras, further see~\cite{GhiZaw2002}. Since the implementation of~\cite{FerGoo2023}, researchers in intuitionistic logic have also become interested in computing the formulas $\Ep{\phi}$ and $\Ap{\phi}$ on specific examples; see for example~\cite{Koc2023} and also our remarks in Section~\ref{sec:benchmarks} below.
+The immediate origin of the question, for us, lies in a verified Coq/Rocq implementation by the first and second author~\cite{FerGoo2023} of Pitts' procedure~\cite{Pit1992} for computing propositional quantifiers in intuitionistic logic. Given a propositional formula $\phi$ and a propositional variable $p$, the formulas $\exists p. \phi$ and $\forall p. \phi$ are abstractly defined by the usual rules of quantification, see~\cref{dfn:prop-quantifiers}. The surprising result of~\cite{Pit1992} is that for any $\phi$, there actually exist \emph{propositional} formulas $\Ep{\phi}$ and $\Ap{\phi}$ that are equivalent to $\exists p. \phi$ and $\forall p. \phi$, respectively. This implies in particular that second-order propositional quantifiers may in fact be encoded, up to equivalence, in the zero-order fragment. Pitts' theorem has many consequences for higher-order intuitionistic logic, including a uniform interpolation theorem and the existence of a model completion for the class of Heyting algebras, further see~\cite{GhiZaw2002}. Since the implementation of~\cite{FerGoo2023}, researchers in intuitionistic logic have also become interested in computing the formulas $\Ep{\phi}$ and $\Ap{\phi}$ on specific examples; see for example~\cite{Koc2023} and also our remarks in Section~\ref{sec:benchmarks} below.
 
 A main issue that we already identified in~\cite{FerGoo2023} was that, even on relatively small inputs, the formulas that were output by our program were very large; we will quantify this in Table~\ref{tab:quant-improvements} below. In all specific cases of interest, one could show manually that the output would admit substantial simplifications, but developing an algorithm for applying such simplifications was both a conceptual and technical challenge. Our main contribution here is to give such a simplification algorithm for intuitionistic formulas, accompanied by a verified implementation in Coq/Rocq. Further, by interleaving Pitts' original recursive procedure with our simplification procedure, we obtain a program with much improved efficiency. This moreover allows us to simplify Pitts' procedure itself both on paper and in the verified implementation, building also on recent insights from work in~\cite{FGGS2024}. 
 
@@ -395,7 +395,7 @@ \subsection{Simplifications specific to Pitts' algorithm}
 However, its behaviour is very similar to the naive proof search algorithm, with additional cost incurred by the fact that non-linear rules induce many recursive calls.
 Our main improvement on the algorithm is to follow a better proof strategy,
 similar to the one discussed in Section~\ref{sec:decision}: We simplify the output during every recursive call of $\mathcal{A}_p$ or $\mathcal{E}_p$, using the function $\texttt{simp\_env}$ described above. This will still result in a correct output, essentially because, whenever $\phi$ and $\phi'$ are equivalent, the specifications of \cref{dfn:prop-quantifiers} imply that $\exists p. \phi$ and $\exists p. \phi'$ are equivalent, and that $\forall p. \phi$ and $\forall p. \phi'$ are equivalent; this invariance property lifts to $\mathsf{E}_p$ and $\mathsf{A}_p$.
-In short, we redefine the uniform interpolants as:
+In short, we redefine the functions as:
 \begin{align}
 \Ap{\Gamma; \phi} &:= \bigvee \callAp{\simpenv\Gamma; \phi} \label{Apsimp} \\ 
 \text{ and } \ \ \Ep{\Gamma} &:= \bigwedge \callEp{\simpenv\Gamma}, \label{Epsimp}