static analysis for intersections

[tillmo]

Syntax will be introduced in #1571. Static analysis should compute the intersection of the signatures. The semantics of OMS1 or OMS2 should have signature \Sigma = Sig(OMS1)\cap Sig(OMS2) and model class {M \in Mod(\Sigma) | M has an expansion to an OMS1 model or to an OMS2 model}. Example: CommutativeMonoid or Group would specify all monoids that are either commutative or groups. Does this make any sense? Alternative semantics: take the intersection of sentences. Then we would get the class of all monoids.

[mcodescu]

It could be interesting to support both situations. If we decide to do so, we need two syntactical constructions.

[tillmo]

do you have a good example for the first semantics? IMHO, the monoid example only supports the second semantics.

[mcodescu]

What I can imagine is rather forced, if you discover that two specifications have something in common, I think the natural thing is to refactor them instead of just recording the similarities, or perhaps write an alignment between them. Reasoning with the first semantics also seems rather complicated, while the second semantics is not complicated at all. Let's go for the second one.

[tillmo]

note that discovering commonalities between specifications is exactly the goal of Immanuel's tool (also of HDTP). Since several solutions are possible, this is not so suited for a language construct.

Also note that the second semantics is not really logical disjunction, so the or syntax might be misleading. Do you have a better idea?

[mcodescu]

What about OMS1 intersected with OMS2?

[tillmo]

OK

[tillmo]

Note that this construct (like reject and extract) is different from existing structuring constructs. It cannot be expressed using some construction on development graph. Actually, for this construct, in the development graph, there will be (theorem?) links from the intersection to the nodes that are being intersected. The intersection node itself is constructed from scratch, using the theories of the nodes being intersected. If not all these nodes are flattenable (in the sense of the DOL standard), then the intersection is ill-formed.

[mcodescu]

I was thinking of (and started) doing the following: if one of the specifications has incoming hiding links, its not flattenable and the intersection is ill-formed. Otherwise, the signature and set of sentences of the intersection is the intersection of the signatures, respectively set of sentences of the OMS being intersected. If we add global definition links from the intersection to the nodes, this might make sentences of the intersection appear twice at the level of nodes, because the theory of a node is computed along the imports. Thus, it is indeed better to have theorem links labeled with inclusions, and they will hold trivially.

More when you see the code.

[tillmo]

note that the syntax is now OMS1 intersect OMS2.