Model Extension / Gluing case study: ML Explained Models

[h0nzZik]

The Matching Logic Explained (MLE) paper by Chen, Lucanu, and Rosu contains many theories for which no model is given. On the other hand, the semantics preservation by model extension theorem implies that any two "syntactically predicate" theories whose signatures are disjoint-up-to-sort-theory can be combined without breaking their consistency (not formalized yet). I would like to use the MLE theories as a case study/benchmark for the semantics preservation theorem.

Currently, the formalized "semantics preservation by model extension" theorem says that any syntactical predicate holds in a particular valuation rho of model M iff it holds in the lifted valuation to the model Mext (and that matching of data patterns is preserved by valuation lifting and model extension).

There is no procedure for checking whether a particular pattern is a syntactical predicate (SPredicate). I would like to have a reflection-based tactic for solving such proof obligations.

I would also like to have a theory-parameterized typeclass STheory whose instances would contains proofs that the given theory contains only SPredicates.

Then I want a function for joining a list of STheories to one STheory. But what would the signature of the joined STheory be? Therefore I need a similar function for joining a list of signatures into one signature. But maybe we could again work not with lists of things, but with indexed types. Like, there would be a simple index type (usually just an enumeration) I, a function sig : I -> Signature, a function th: forall (i: I) -> @Theory (sig i). But all the signatures have to extend the Sorts signature, all the theories the Sorts theory. So we would need to be parameterized with a hypothesis

sig_sorts : forall (i : I), SignatureMorphism SortsSignature (sig I)

where SignatureMorphism S1 S2 would injectively map symbols to symbols and variables to variables. .

Alternatively, we could have the "variables" part of the signature shared globally, and work only with symbol mappings.

And we would need another hypothesis,

th_sorts : forall (i : I), @TheoryMorphism SortsSignature (sig I) SortsTheory (th I)

which would basically say that the Definedness axiom is present in th I. Maybe it could be weakened to saying that the Definedness axiom is provable from th I? But no, I do not want to invoke the proof system here. Or that the definedness axiom is a semantic consequence of th I? That could work...

In this context, we would have to define the following functions:

cSig : Signature
cSig_contains_sigI : forall (i : I), SignatureMorphism (sig I) cSig
cTheory : @Theory cSig 
cTheory_contains_theories: forall (I : I), subseteq (lift_to_cSig (th i)) cTheory

where lift_to_cSig lifts the axioms of a given theory using the cSig_contains_sigI i morphism. And now we could define the model composition. We would assume the context

models: forall (i : I), @Model (sig i).

and define

cM : @Model cSig

and prove

cM_models_cTheory : 
(forall (I : I), models i |= th i) ->
cM |= cTheory

.

[daniel-horpacsi]

Note to self: check related work on theory combination in SMT.

[h0nzZik]

@daniel-horpacsi Do you mean things like the Nelson-Oppen combination?

[daniel-horpacsi]

Amongst others, yes, but of course with less emphasis on actual solvers and more on consistency. I'm not familiar with this field but I anticipate that some problems and their solutions shall be adaptable.