signatures versus theories

[till]

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.

[maeder]

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