signatures versus theories

[sternk]

Reported by till and assigned to mcodescu Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/172

---

Implement a clean treatment of signatures versus theories. (Currently, often signatures also store some theory information. Some comorphisms are non-simple theoroidal, which is currently not backed by the general theory of heterogeneous specs.) some notions:

• a simple theoroidal comorphism maps
  • signatures to theories
  • sentences to sentences
  • the mapping of theories is induced by these maps
• an arbitrary theoroidal comorphism maps
  • theories to theories
  • sentences to sentences
  • problem here: is doable, but more complicated than the simple case. do we really need it?
• a specification frame morphism maps
  • theories to theories
  • problem here: how to translate goals? Perhaps extend the notion of theory such that some formulas are marked as goals general questions:
• can we stay with simple theoroidal comorphisms, or do we need non-simple ones?
• does it help to add the institution of presentations for each institution in the logic graph?
• can we stay with sentence-to-sentence translation, or do we need something else? problems with simple theoroidal comorphisms:
• CASL to Isabelle: free types are axioms in CASL, sig elements in Isabelle
  • solution 1
  • free types are signature elements in CASL
  • two-level construction of CASL:
  • plain CASL sigs as in RefMan
  • CASL sig = plain CASL theory = plain CASL sig + set of sort gen axioms
  • CASL theory = CASL sig + set of axioms
  • solution 2
  • free types are axioms in Isabelle
  • solution 3
  • non-simple theoroidal comorphisms
• CASL to HasCASL
  • In HasCASL, datatypes must be parts of the signature (needed for analysis of program blocks)
  • If CASL adopts the same solution, we get a simple theoroidal comorphism
  • If CASL does not so, we get a non-simple theoroidal comorphism
• HasCASL to Haskell
  • no problem, since constructors are already determined by signature and program blocks lead to complete definition of a function

• CASLtoTopSort: needs derived sig mors

  s<t  included in s<t<u is mapped to
  sort t; pred s:t  "included in"  sort u; preds s,t:u
  

  • This "included" is only a derived signature morphism. It would be nice to have an institution independent notion of derived signature morphism here
• CASLtoSPASS:
  • sort gen axioms need to become signature parts. They cannot be translated to axioms! => semi-comorphism. Better would be a kind of partial comorphism (after all, some sentences can be translated)
• CASL2SubCFOL
  • some sorts get bottom elements. These sorts are computed from the signature and the sentences (i.e. type cast) when mapping the whole theory. Therefore mapping the signature and sentences separately may not work for all sentences Are there problems with theoroidal comorphisms (i.e. sentence to sentence translation)? See also ticket #171. Discuss implications for Hets and its connection to provers.

[sternk]

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/172#comment:5

---

'CASL2SubCFOL` has been extended to allow sentence independent signature translations

[tillmo]

I think we need non-simple theoroidal comorphisms, and Hets comorphism interface supports this already, because it provides a function for mapping theories to theories. Moreover, this is backed up by the general theory, see: Mihai Codescu, Generalized Theoroidal Institution Comorphisms, http://link.springer.com/chapter/10.1007%2F978-3-642-03429-9_7 We should check whether adpoting this theory needs changes in Hets, though.

[tillmo]

@mcodescu has pointed out the following problem. Consider:

logic OWL
ontology O1 = 
  Individual: John
  Types: hasFamilyName value "Smith"^^xsd:string
  DataProperty: hasFamilyName
end
ontology O2 = 
 Individual: Tim
 DataProperty: hasFamilyName
end
interpretation V : O1 to O2 = 
  John |-> Tim
end

his is a valid OWL view, but we can disprove it easily. However, the source ontology makes use of xsd:string, while the target ontology does not. If we translate the entire development graph to CASL via a translation that adds xsd:string in the translated theory only if it appears in the sentences of the ontology, we will get a signature morphism between the translated theories that cannot map xsd:string to a sort in the target theory.

In a sense, in such a case, Hets should be able to disprove the view by the inability to translate the signature morphism. Of course, this will require some new mechanism in Hets.

[mcodescu]

If not all OWL theory morphisms can be mapped along OWL22CASL(with datatypes added by-need), then we need to identify the sublogic of OWL that is the source sublogic of this comorphism - otherwise we don't have a comorphism.

[tillmo]

Indeed, all theory morphisms can be mapped. In the example, we have a signature morphism, which also can be mapped to a signature morphism between the translations of the signatures. However, we cannot extend it to a morphism between the translations of the theories, showing that it is not a theory morphism (theory morphisms can be mapped).