# Complete Subhedge Projection for Stepwise Hedge Automata +
## 6 Safe-No-Change Projection
### Algorithm  
We now describe the safe-no-change projection algorithm. Let \(A=(\Sigma,Q,\Delta,I,F)\) be a SHA with schema \(\mathbf{S}\). The algorithm takes the dSHA\(A\) as input and compiles it to some dSHA\({}^{\downarrow}\)\(A^{\textit{src}}\). We will state why \(A^{\textit{src}}\) is sound for subhedge projection under the condition that \(A\) is schema-complete for schema \(\mathbf{S}\). We do _not_ even have to assume that the schema \(\mathbf{S}\) is regular. The proof is eight pages long and, therefore, delegated to the Appendix B. For any set \(P\subseteq\mathcal{Q}\), we define the set of states that safely lead to \(P\):  
\[\textit{safe}^{\Delta}(P)=\{q\in\mathcal{Q}\mid\textit{acc}^{\Delta}(\{q\}) \subseteq P\}.\]  
So, state \(q\) is safe for \(P\) if any hedge read from \(q\) on which the run with \(\Delta\) does not block must reach some state in \(P\). We note that \(\textit{safe}^{\Delta}(P)\) can be computed in linear time in the size of \(\Delta\) using inverse hedge accessibility from \(P\). We define the set of states that will no longer change:  
\[\textit{no-change}^{\Delta}=\{q\mid q\in\textit{safe}^{\Delta}(\{q\})\}.\]  
So, \(q\in\textit{no-change}^{\Delta}\) if and only if \(\textit{acc}^{\Delta}(\{q\})\subseteq\{q\}\). This means that all transition rules starting in \(q\) must loop in \(q\). In the example automaton from Figure 4, the self-looping states are those in \(\textit{no-change}^{\Delta}=\{2,3,4,5\}\). **Lemma 7**: _Let \(A=(\Sigma,\mathcal{Q},\Delta,I,F)\) be a SHA that is schema-complete for schema \(\mathbf{S}\). For any hedge \(h\in\mathbf{S}\) and state \(q\in I\cap\textit{no-change}^{\Delta}\), it then holds that \(q\xrightarrow{h}q\) wrt \(\Delta\)._  
Proof. : The schema-completeness of \(A\) for \(\mathbf{S}\) applied to \(h\in\mathbf{S}\) and \(q\in I\) yields the existence of some state \(q^{\prime}\in\mathcal{Q}\), such that \(q\xrightarrow{h}q^{\prime}\) wrt \(\Delta\). Let \(q^{\prime}\) be any such state. Note that \(q^{\prime}\in\textit{acc}^{\Delta}(q)\). Since \(q\in\textit{no-change}^{\Delta}\), we have \(q\in\textit{safe}^{\Delta}(\{q\})\), so that \(q^{\prime}\in\textit{acc}^{\Delta}(\{q\})\) implies \(q^{\prime}=q\). This proves \(q\xrightarrow{h}q\) wrt \(\Delta\). For any state \(q\in\mathcal{Q}\) and subset of states \(Q\subseteq\mathcal{Q}\), we define the following:  
\[\textit{s-down}^{\Delta}(q,\mathcal{Q}) = \textit{safe}^{\Delta}(\{p\in\mathcal{Q}\mid q\
ot\oplus^{\Delta}p \subseteq Q\})\] \[\textit{s-no-change}^{\Delta}(q) = \textit{s-down}^{\Delta}(q,\{q\})\]  
A state belongs to \(\textit{s-down}^{\Delta}(q,\mathcal{Q})\) if all states \(p\in\textit{acc}^{\Delta}(q)\) satisfy \(q\
ot\oplus^{\Delta}p\subseteq\mathcal{Q}\). So, \(p\) is a state in a down level that will safely go up to some state in \(\mathcal{Q}\). A state \(p\) belongs to \(\textit{s-no-change}^{\Delta}(q)\) if it safely does not change \(q\), i.e., if \(\{q\}\
ot\oplus^{\Delta}\textit{acc}^{\Delta}(\{p\})\subseteq\{q\}\). We next compile the SHA\(A\) to a SHA\({}^{\downarrow}\)\(A^{\textit{src}}=(\Sigma,\mathcal{Q}^{\textit{src}},\)\(\Delta^{\textit{src}},\)\(I^{\textit{src}},\)\(F^{\textit{src}})\). For this, let \(\Pi\) be a fresh symbol and consider the state set as follows:  
\[\mathcal{Q}^{\textit{src}}=\{\Pi\}\uplus(\mathcal{Q}\times 2^{\mathcal{Q}}).\]  
In practice, we restrict the state space to the those states that are accessible or clean the dSHA keeping only those states that are used in some successful run. But, in the worst case, the construction may indeed be exponential. Example 15 can be adapted to show this. A pair \((q,P)\) means the state \(q\) will safely no longer change in the current subbedge if \(q\in P\cup\textit{no-change}^{\Delta}\). In this case, the subbedge can be projected.