From 8e9c4d66a01cee8b5f3d1e5ab3a8a206e1f356de Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hugo=20F=C3=A9r=C3=A9e?= Date: Wed, 16 Oct 2024 16:08:28 +0200 Subject: [PATCH] Jfla : Rework example --- jfla-paper/fereegooliglesiasvazquez2024.tex | 31 ++++----------------- 1 file changed, 6 insertions(+), 25 deletions(-) diff --git a/jfla-paper/fereegooliglesiasvazquez2024.tex b/jfla-paper/fereegooliglesiasvazquez2024.tex index 8aa4b32..173b700 100644 --- a/jfla-paper/fereegooliglesiasvazquez2024.tex +++ b/jfla-paper/fereegooliglesiasvazquez2024.tex @@ -410,32 +410,13 @@ \subsection{Simplifications specific to Pitts' algorithm} $$ The formula $\exists p. \phi_n$ is, up to equivalence, $\bigwedge_{i=0}^n a_i$, and this is indeed what is computed by our simplified algorithm. However, the naive implementation computes a much larger formula. \sam{TODO integrate explanation below} -The first step is to shift the first conjunction ($\wedge$) into the context: -\hugo{Actually, there is immediately a conjunction of size $n$, with $n-1$ choices still to do} -$$ - \Ep {(a_0 \wedge p), (a_1 \wedge p) \wedge \cdots \wedge (a_n \wedge p)} -$$ -\hugo{Explain the general formula for the number of recursive calls} -At this point, the procedure faces two choices: shifting the first $\wedge$ either on the left or on the right. This means the interpolant becomes: - -$$ - \Ep {a_0, p, (a_1 \wedge p) \wedge \cdots \wedge (a_n \wedge p)} \wedge \Ep {(a_0 \wedge p), (a_1 \wedge p), (a_2 \wedge p) \wedge \cdots \wedge (a_n \wedge p)} -$$ - -Now, in this new expression, we have four possible choices: one in the first part and three in the second, causing the number of possibilities to grow exponentially with each recursive call. -If this process is followed until the end, it results in a large conjunction of the same element: - -$$ - \Ep {a_0, p, a_1, p, \cdots , a_n, p} -$$ - -In other words, computing the original interpolant is equivalent to computing this final form once, which is exactly what our simplification procedure accomplishes. During the first recursive call, the context will be simplified to: - -$$ - a_0, a_1, \cdots , a_n, p -$$ +It starts by building the conjunction of all the formulas obtained by applying a recursive call +to the context of the premise of an instance of rule ${\wedge \mathrm L}$ whose conclusion is of the form $\phi_n \vdash \cdot$: +$$\bigwedge_{0\le i\le n} \Ep{(a_0 \wedge p), \dots, a_i, p , (a_{i+1} \wedge p), \dots \wedge (a_n \wedge p)}$$ -eliminating all the unnecessary recursive calls in the process. +Now, each of these recursive call do in turn $n$ recursive calls themselves, and so on; leading to a total of about $(n+1)!$ calls, +where the final call in all recursive branches are identical: $\Ep{a_0, p, a_1, p, \dots, a_n, p}$. +This both leads to an unncessarily large computation time, as well as an about as large output formula. \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}.