Well Formedness Decidability

Into Interfaces

The careful reader may wonder about the employed proof strategy. Indeed, since we demonstrated not_in_l_pairs_bool_correctness, proving not_in_l_pairs's decidability can be achieved in a trivial manner:

In any case, for the sake of diversity and fun, we followed an approach without using the fact that we demonstrated the predicate equivalent to its computational counterpart. In the following we employ one of the two approaches as we think more convenient.

Into Bindings

Into Components

Components are an hierarchical structure. This will require employing a special trick when dealing with its decidability. Let us start by proving that a component belonging to an empty list of components can indeed be decided whether it is well-formed or not.

Now let us prove the same for the case that the component belongs to a non-empty list, and we have decidability on the well-formedness of the head element, and also on all elements of the tail.

Finally, we are in a position to prove out theorem of interest.

Naturally, as our notion of state is in fact a component with some imposed restrictions, its well_formedness can also be easily proved.

Being able to decide whether a component is indeed a well_formed_component or not was already demonstrated by our theorem well_formed_component_dec. However, we now want a function that returns true when the given component is a well_formed_component and false otherwise. Naturally, we want the ensurance that this function is correct, i.e. sound and complete w.r.t the well_formed_component predicate. Let us start by defining such function.

For our interests, we shall want to prove dec_component as being equivalent to our well_formed_component predicate as demonstrated by the eq predicate. For this, we shall follow the same approach employed for proving the decidability of well_formed_component.

Note again that lc_eq requires to be concluded by Defined rather than Qed. Moreover, we shall define the auxiliary lemma boolean_function_fact to help us proving our main theorem.

Indeed, proving dec_component_correctness follows the same approach as in well_formed_component_dec. This gives us strong confidence on the behaviour of our dec_component function. As expected, its extraction to an OCaml certified program would be achieved as follows: Recursive Extraction dec_component. It should come as no surprise that doing the same for states reuses most of the above machinery.