Define HML subset expressing stability respecting branching bisimilarity

[betawave]

Define $\texttt{HML}_{\mathrm{srbb}}$ in accordance with the paper as the subset of $\texttt{HML}$ that express stability respecting branching bisimilarity.

Then show that $\texttt{HML}_{\mathrm{srbb}}$ is truly a subset of $\texttt{HML}$ so that one can reuse the notion of distinguishing power from $\texttt{HML}$.

[betawave]

While writing a first draft (see here), I encountered an issue I'd like to discuss in our larger team meeting:

When trying to map some of the clauses of $\chi$ / $\texttt{HML\_srbb\_conjunction}$ in $\texttt{HML\_srbb}$ to normal $\texttt{HML}$:

1. stable conjunction $\bigwedge\lbrace\neg\langle\tau\rangle\texttt{T}, \psi, \psi, \dots\rbrace$
2. branching conjunction $\bigwedge\lbrace(\alpha)\varphi, \psi, \psi, \dots\rbrace$

one needs to use the conjunct data constructor of $\texttt{HML}$ ($\texttt{HML\_conj}$) and add an element to the index set - either a HML_not (HML_poss 𝜏 HML_true) in the first case or something unclear to me in the other - and extend the $\psi s$ function.

Here, I see the issue that we don't know enough about the type of the index set $I$.... How can we get a new element of that type to put into that set? Are there even enough members of that type to do that?

One potential solution I see would be to extend the base $\texttt{HML}$ data type with a binary conjunction data constructor. With this one could add the fix term on the left and an index conjunction on the right.

[betawave]

I succeeded in finishing the translation function by employing the Hilbert choice operator SOME to obtain some new index new_i which has not previously been used in the index set I (via let new_i = (SOME i. i \notin I) in ...). While Isabelle excepts this definition (and is able to prove the required properties of function via fastforce & metis; I did not attempt to show termination yet), I personally am unsure if such a new index always exists... My uneasyness with this definition might stem from my general unaquaintedness with the SOME operator. The draft can be found here

[betawave]

I quickly tried proving termination of the translation function but failed. While the structure of the proof when inducting over three different formulas is not pretty, I don't think that the triple mutual recursive definition of HML_SRBB was the issue there...

I reflected further on the definition of the translation function using the SOME operator and am convinced that is not well defined, i.e. no termination proof can be found. In the current definition of HML_SRBB the following is a valid value of $\chi$/HML_srbb_conjunction: $\texttt{HML\_srbb\_conj}\ \lbrace x . \mathrm{True} \rbrace\ (\lambda\, \mathrm{dontCare} .\ \texttt{HML\_srbb\_true})$ I.e. The conjunction over an index set spanning the complete index type and mapping each element to true. Here, it is clear that SOME i. i \notin I is not 'well-defined', because there is no such new index i that is not already in the index set I, since this set already spans the complete index type. This construction is independent of the choice of index type, leading me to the conclusion that the translate function can not be defined via the SOME operator. I'm skeptical that such a function can be properly defined at all.

While researching the behavior of SOME, I found the following StackOverflow thread, which I found useful: https://stackoverflow.com/questions/65675639/how-to-use-the-the-syntax-in-isabelle-hol https://stackoverflow.com/questions/53411723/proving-intuitive-statements-about-the-in-isabelle https://stackoverflow.com/questions/50750854/isabelle-hol-what-does-the-the-construct-denote

Some relevant quotes from these threads:

SOME [...] is (a variant of) Hilbert's epsilon operator that returns an [...] element that respects a certain property. If none [...] exist, an underspecified element is returned. SOME and THE are not executable.

-- Mathias Fleury

@benkeks What's your opinion on this?

[betawave]

In our team meeting @benkeks suggested that one could try to implement the problematic clauses (stable and branching conjunction) of the translation from $\texttt{HML}_{\texttt{srbb}}$ to $\texttt{HML}$ not by extending the index set $I$ and mapping function $\psi s$ of the 'original' conjunction but instead by 'keeping' the original conjunction and wrapping it together with the new conjunct in a new conjunction containing only two elements (either the formula forbidding internal action of the $(\alpha)\varphi$ clause).

I implemented this approach on my branch in this commit. Together with some abbreviations this is quite readable in my opinion. Also, it does not employ the SOME operator, given me the confidence that this is well defined. I'm a little unsure if this translation by nesting conjunction is actually valid though, or if there are sideconditions for this to be okay which I have not properly formalized...

Additionally, I employed our finding that primrec has no issues showing the termination of our mutually recursive functions and have thereby implemented a 'working' translate function. With this, I was able to define a semantic function for $\texttt{HML}_{\texttt{srbb}}$ in terms of the semantic function of $\texttt{HML}$ which was the whole reason for this ordeal.

[benkeks]

As far as I get it, there are branches where this has been implemented, but there is no Pull Request. Could you create one? (For now, let's settle on the index-set-function approach as it seems to work.)

Technically this has not been finished during the first iteration. On the other hand, I would like to have a clear starting point for the next iteration. So if we can merge it before Monday, this would be great. Otherwise, finishing this will be a first issue for the second iteration.

[benkeks]

I move this to stage ToDo because it lacks a PR. (Once you open a PR, the issue would better fit into “in progress”.)

[betawave]

Here is the corresponding PR https://github.com/equivio/silent-step-spectroscopy/pull/29