computed weights of example

jfla-paper/fereegooliglesiasvazquez2024.tex

@@ -113,7 +113,7 @@ \section{Introduction}
 % \sam{TODO It opens up a number of new questions: Complexity, Optimality of the simplification (and is it worth it, there may be a trade-off where simpler formulas can be very difficult to obtain and the one an algorithm obtains is already readable? Although maybe this is unlikely because if a formula is already readable it should be easy to simplify it further.) }
 
 
-The {\Coq} development is available online at \url{https://github.com/hferee/UIML/}. A web demo of the calculator is available at \url{https://hferee.github.io/UIML/}, which also links to online documentation of the {\Coq} code. Throughout this paper, we provide links to relevant {\Coq} declarations with the symbol \coqdoc{toc.html}. The reference commit for the code discussed in this paper is \href{https://github.com/hferee/UIML/tree/39b38d9d8c86672bea49bef5c342a24526914de9}{\texttt{39b38d9}}.
+The {\Coq} development is available online at \url{https://github.com/hferee/UIML/}. A web demo of the calculator is available at \url{https://hferee.github.io/UIML/}, which also links to online documentation of the {\Coq} code. Throughout this paper, we provide links to relevant {\Coq} declarations under a clickable symbol \coqdoc{toc.html}. The reference commit for the code discussed in this paper is \href{https://github.com/hferee/UIML/tree/39b38d9d8c86672bea49bef5c342a24526914de9}{\texttt{39b38d9}}.
 
 \section{Sequents, proofs, and propositional quantifiers}\label{sec:prelims}
 A \emph{context} is a finite list of formulas, and is typically denoted with a capital Greek letter $\Gamma$ or $\Delta$. We denote the concatenation of contexts $\Gamma$ and $\Delta$ by $\Gamma, \Delta$, or occasionally $\Gamma \bullet \Delta$, and we abuse notation to write expressions like $\Gamma, \phi$ and $\Gamma \bullet \phi$ for the concatenation of $\Gamma$ with the one-element context containing only $\phi$. A \emph{sequent} is a pair of a context and a formula, denoted $\Gamma \Rightarrow \phi$. We now recall a notion of \emph{weight} on formulas and sequents~\cite{Pit1992}.
@@ -413,7 +413,7 @@ \subsection{Simplifications specific to Pitts' algorithm}
 \end{example}
 The main gain obtained by the definitions given in (\ref{Apsimp}) and (\ref{Epsimp}) is that the function \texttt{simp\_env} applies any possible left invertible linear rules to the context. This means that $\mathcal{E}_p$ and $\mathcal{A}_p$ are only ever applied to a simplified context $\Gamma'$ that does not contain any formulas of the form $p \to \phi$, $\phi \wedge \psi$, $(\phi \vee \psi) \to \chi$, or $(\phi \wedge \psi) \to \chi$. This means that four of the rules from the sequent calculus $\Gfourip$ can never apply to $\Gamma'$, reducing the number of different kinds of recursive calls from $8$ to $4$ for $\mathsf{E}$ and from $13$ to $9$ for $\mathsf{A}$. Since any applicable rule to $\Gamma'$ incurs a recursive call, this reduction considerably decreases the overall number of redundant recursive calls. We demonstrate this empirically in~\cref{sec:benchmarks}.
 
-While one could use these observations to give a shorter correctness proof `from scratch' with fewer cases, we were able to re-use the correctness proofs that we had already formalized previously, with only slight modifications. Whenever the old version of the proof used an induction hypothesis about $\mathcal{A}_p(\Gamma; \phi)$ or $\mathcal{E}_p(\Gamma)$, in the new proof we are able to use the same induction hypothesis for $\mathcal{A}_p(\simpenv{\Gamma}; \phi)$ or $\mathcal{E}_p(\simpenv{\Gamma}$. To prove that this is indeed possible, one needs to observe that (i) $\simpenv{\Gamma}$ has lower weight than $\Gamma$, so the induction hypothesis used for $\Gamma$ \emph{a fortiori}  applies to $\simpenv{\Gamma}$; and (ii) the context $\simpenv{\Gamma}$ is equivalent to the context $\Gamma$, and may therefore be replaced by it in any hypothesis.
+While one could use these observations to give a shorter correctness proof `from scratch' with fewer cases, we were able to re-use the correctness proofs that we had already formalized previously, with only slight modifications. Whenever the old version of the proof used an induction hypothesis about $\mathcal{A}_p(\Gamma; \phi)$ or $\mathcal{E}_p(\Gamma)$, in the new proof we are able to use the same induction hypothesis for $\mathcal{A}_p(\simpenv{\Gamma}; \phi)$ or $\mathcal{E}_p(\simpenv{\Gamma})$. To prove that this is indeed possible, one needs to observe that (i) $\simpenv{\Gamma}$ has lower weight than $\Gamma$, so the induction hypothesis used for $\Gamma$ \emph{a fortiori}  applies to $\simpenv{\Gamma}$; and (ii) the context $\simpenv{\Gamma}$ is equivalent to the context $\Gamma$, and may therefore be replaced by it in any hypothesis.
 
 A technical modification in the formalization of the proof that we had to make in order for this to go through was to change the induction principle. Our original implementation used an induction on the last rule in a hypothetical proof of a sequent of the form $\Gamma \vdash \cdot$ (when proving correctness for $\Ep{\Gamma}$) or of a sequent of the form $\Gamma \cons \cdot \vdash \phi$ (when proving correctness for $\Ap{\Gamma; \phi}$). In our new proof, we use an induction on the weight of the sequent.
 
@@ -459,8 +459,8 @@ \section{Examples, benchmarks and challenges}\label{sec:benchmarks}
 		$\exists q, \exists p, \psi_2$      & --              & 8                \\
 		$\forall p, \psi_3$                 & 429             & 1                \\
 		$\exists p, \psi_3$                 & 668             & 13               \\
-		$\forall p, \psi_4$                 & ??             & ??               \\
-		$\exists p, \psi_4$                 & ??             & ??               \\
+		$\forall p, \psi_4$                 & 33              & 4               \\
+		$\exists p, \psi_4$                 & 160             & 12               \\
 		\hline
 	\end{tabular}
 	\caption{Experimental results for computing propositional quantifiers on the set of formulas defined in Section \ref{sec:benchmarks}. The `Original' column shows the initial weights, while the `Optimized' column presents the weights after applying the optimizations described in this paper. `--' indicates computations that exceeded the 5-minute time limit, and `$^*$' that the computation time took more that 2 minutes.}