A ‘systematic’ reformulation
A while ago I wrote 0004 about eliminating quantifier alternation, which took a fair amount of logic formula manipulation. (By the way, to our pleasant surprise, the SMT solver seems to prefer the derived formulas — inexplicably, however.) Not long after that, my colleague Yun-Sheng Chang came up with a reformulation that makes the solution much more streamlined; below is my presentation of the reformulation, along with a higher-level recap of what I did in 0004. The reformulation is a good example of the general principle of endowing definitions with enough structure to drive the construction of subsequent proofs; in this case the definitions in question are about transition systems, hence the title of this post.
In 0004 the problem was a simplified version, and here we need to restore a bit of its original form (while omitting some details given in 0004). Consider two transition systems $S$ and $T$, whose transition relations are both denoted by $(\leadsto)$. We want to establish that $S$ is simulated by $T$ within the envelope of a relation $R \subseteq S \times T$, that is,
$$ \forall s, s' \in S.\ \forall t \in T.\ s \leadsto s' \mathrel\wedge R\ (s, t) \to \exists t' \in T.\ t \leadsto t' \mathrel\wedge R\ (s', t') $$
The definition of $R$ needs to refer to some values (drawn from a set $V$) that are abstracted/extracted from states of $S$ as specified by a relation $F \subseteq S \times V$; we may assume that $F$ is total, that is, $\forall s \in S.\ \exists v \in V.\ F\ (s, v)$ (so that we can extract a value from any state). In other words, we actually want to define $R$ as a ternary relation $R_{SVT} \subseteq S \times V \times T$, and whenever we write $R_{SVT}\ (s, v, t)$ it is implied (by logical inference or just by convention) that $F\ (s, v)$ holds (so that $v$ is constrained and sometimes even determined by $s$, and is not intended to contribute an extra degree of freedom).
One natural way to achieve this is to include $F$ in the definition of $R$ — a version which we denote by $R_{FSVT}$ — so that $R_{FSVT}\ (s, v, t)$ implies $F\ (s, v)$ by definition, but $R_{FSVT}$ is rather complicated (and causes the quantifier alternation problem). My observation in 0004 was that we can separate $F$ from $R_{FSVT}$ by Skolemisation. In slightly more detail: The totality of $F$ implies the existence of a function $f \in S \to V$ satisfying $F$, that is,
\begin{equation} \exists f \in S \to V.\ \mathsf{Spec}\ f \label{eq:choice} \end{equation}
where
$$ \mathsf{Spec}\ f \defeq \forall s \in S.\ F\ (s, f\ s) $$
We can then use $f$ in the simulation statement
$$ \mathsf{Sim}\ f \defeq \forall s, s' \in S.\ \forall t \in T.\ s \leadsto s' \mathrel\wedge R_{SVT}\ (s, f\ s, t) \to \exists t' \in T.\ t \leadsto t' \mathrel\wedge R_{SVT}\ (s', f\ s', t') $$
However, $f$ appears free in $\mathsf{Sim}\ f$ and should be suitably quantified, so the complete statement should be
\begin{equation} \exists f \in S \to V.\ \mathsf{Spec}\ f \mathrel\wedge \mathsf{Sim}\ f \label{eq:complete} \end{equation}
where the two occurrences of $R_{SVT}\ (s, v, t)$ (where $s$, $f\ s$ and $s'$, $f\ s'$ are substituted for $s$, $v$) do ‘imply’ $F\ (s, v)$ due to $\mathsf{Spec}\ f$. (Note that we don’t need to use $R_{FSVT}$ but can just use $R_{SVT}$, which doesn’t need to imply $F$ logically.) To get from (\ref{eq:choice}) to (\ref{eq:complete}), it suffices to prove
\begin{equation} \forall f \in S \to V.\ \mathsf{Spec}\ f \to \mathsf{Sim}\ f \label{eq:premise} \end{equation}
and the first half of 0004 is a derivation of (\ref{eq:premise}) from the version of the simulation statement that uses $R_{FSVT}$.
Yun-Sheng’s observation is that another place to stow $F$ is the transition system $S$. Conceptually, instead of computing the values associated with the states on demand, we can pre-compute the values and store them with the states. Technically, this gives rise to a new transition system $S^\dagger$: the set of states of $S^\dagger$ is $F$, and there is a transition $(s, v) \leadsto (s', v')$ in $S^\dagger$ exactly when $s \leadsto s'$ in $S$. The statement of $S^\dagger$ being simulated by $T$ becomes
\begin{align*} & \forall (s, v), (s', v') \in S^\dagger. \\ & \quad \forall t \in T.\ (s, v) \leadsto (s', v') \mathrel\wedge R_{S^\dagger T}\ ((s, v), t) \to \exists t' \in T.\ t \leadsto t' \mathrel\wedge R_{S^\dagger T}\ ((s', v'), t') \end{align*}
where $R_{S^\dagger T} \subseteq S^\dagger \times T = F \times T$, so $R_{S^\dagger T}\ ((s, v), t)$ implies $F\ (s, v)$ by definition (‘at type level’). And, expanding the definition of $S^\dagger$, we see that the statement above is equivalent to
\begin{align*} & \forall s, s' \in S.\ \forall v, v' \in V.\ F\ (s, v) \mathrel\wedge F\ (s', v') \to \\ & \quad \forall t \in T.\ s \leadsto s' \mathrel\wedge R_{S^\dagger T}\ ((s, v), t) \to \exists t' \in T.\ t \leadsto t' \mathrel\wedge R_{S^\dagger T}\ ((s', v'), t') \end{align*}
which is the ideal form derived at the end of 0004, where it took a lot of effort to get to the end, whereas here it all follows directly and neatly from the definition of $S^\dagger$. This is not the end of the story though — we still need to establish a simulation of $S$ by $S^\dagger$, so that we can get a simulation of $S$ by $T$ by transitivity. But this is easy: just take (the converse of) the first projection $\mathsf{fst}^\circ \subseteq S \times (S \times V)$ as the simulation relation, and the simulation can be established straightforwardly, notably using the totality of $F$. Then, by transitivity, the simulation relation between $S$ and $T$ will be the composite relation $\mathsf{fst}^\circ \cdot R_{S^\dagger T}$.
Yun-Sheng intended to distill this as a general technique for deriving formulas that can be handled more efficiently by SMT solvers. Alas, the modern SMT solving algorithms seem to be so complicated that it’s rather difficult to analyse the improvement brought by the technique, which is an unfortunate situation — creating machinery that we can no longer understand and control. But hopefully there’re still a few people who know these algorithms inside out?
