search

spechub / Hets

The Heterogeneous Tool Set
http://hets.eu
GNU General Public License v2.0
57 stars 19 forks source link

extend DG structure such that all of DOL is covered #1693

Open tillmo opened 7 years ago

tillmo commented 7 years ago

e.g. minimize, maximize needs to be added to the free/cofree case.

mcodescu commented 7 years ago

Comments on the DG data structures:

  1. make sure that current language, logic and serialization are fully covered (currently, only logic is covered).

  2. the global environment should be generalized to allow all kinds of signatures.

We currently have:

We need:

We need types for their signatures, see section on DOL semantics.

  1. I was thinking to have one entry for all mapping types:

OMSMappingEntry OMSMappingSig

but we have some complications with the fact that some refinements are OMS mappings, but not all of them (branching refinement including arch specs, component refinements).

  1. for minimize/maximize we could probably do ClosableDefLink ClosureType MaybeNode with all 4 types of closure instead of FreeOrCofreeDefLink FreeOrCofree MaybeNode in DGLinkType.

  2. for approximation, it seems to me that we need a DGLinkType that does not import axioms: you don't want new sentences appearing in the theory of the original ontology.

  3. I'm not sure we cover all cases for conservativity strength in Common/Consistency, data Conservativity: mcons, ccons, mono, def, wdef At least wdef seems not to be covered.

  4. we need a datatype for mappings between networks. This should be a a map with elements of the type (node in source graph, node in target graph, GMorphism between their signatures)

  5. signatures of refinements must be generalised such that refinements between networks are covered but in a way that does not mess up the static analysis of the refinement language. This requires quite some refactoring (because for example the refinement tree pointers needed for combining refinement trees are in the refinement signatures, and we would need to change that type too)

  6. AlignSig seems to be generic enough to cover heterogeneous alignments

tillmo commented 7 years ago

1+2: I agree (have slightly edited 1). 3: OK, then refinements ened different treatmens? isn't the full language of the refinement paper covered already? 4: agreed 5: we also could have an inclusion link in the opposite direction. However, this would require computation of the approximation at static analysis time. With a "forgetting" link, we could postpone this. 6: yes, (only) wdef is missing 7 agreed 8 agreed 9 good!

Could you go ahead and start implementing this?

mcodescu commented 7 years ago

(3) the refinement language is covered in Hets, but not included in DOL. In particular, DOL refinements are a type of OMS mapping. CASL architectural specifications are a particular case of CASL refinement. If CASL refinements = DOL refinements, then we would need consider arch specs and unit spec to be OMS mappings as well. I don't think that's wrong, we just need to be aware of this.

(5) I don't understand: do you want to have an inclusion link from the original theory to the approximation? This doesn't really make sense to me, as the signature of the approximation is smaller or in a less expressive logic. And in the other direction, you have the problem that I mentioned: when computing the theory of the original ontology, you include the sentences in the approximation. We seem to need something similar to a hiding link. Yes, I'll start doing this.

tillmo commented 7 years ago
  1. indeed, the CASL (or, more precisely: refinement paper) and DOL refinement languages need to be united. In the refinement paper, we have arch specs and branching refinements which are not there in DOL. In DOL, we have refinement of networks which are not there in the refinement paper.
  2. agreed.
tillmo commented 7 years ago

@mcodescu, if you have implemented something here, could you please push it onto a branch? I might want to discuss it tomorrow on a train trip with @eugenk

mcodescu commented 7 years ago

I have started something here: https://github.com/spechub/Hets/tree/1693-datatypes-for-DOL It's possible I'll make more changes by tomorrow.

mcodescu commented 7 years ago

For 1 we would need to change LogicGraph in Logic/Grothendieck. It already has a current logic and current syntax, I guess adding a currentLanguage :: IRI would be enough. Did not implement it because I wasn't sure.

For 4 I still need to rename the types FreeOrCofree and FreeOrCofreeDefLink, but I modified them to cover all cases we need already.

For 3 and 8 I need more time to think.