Model-Level vs Theory-Level Semantics

The Heterogeneous Tool Set (Hets) Structured and Specifications Development Graphs Benchmark Examples Model-Level vs Theory-Level Semantics 1 2 1Till Mossakowski Florian Rabe Mihai Codescu 1DFKI GmbH Bremen and University of Bremen 2Jacobs University Bremen 12.09.2009, Udine, IFIP WG 1.3 Meeting Till Mossakowski, Florian Rabe, Mihai Codescu Model-Level vs Theory-Level SemanticsThe Heterogeneous Tool Set (Hets) Structured and Specifications Development Graphs Benchmark Examples Introduction Two di erent semantics for structured specifications: model-level semantics: the semantics of a specification SP is a signature Sig(SP) and a class of models Mod(SP) over Sig(SP) theory-level semantics: the semantics of a specification is a signature Sig(SP) and a set of sentences Th(SP) over Sig(SP) Both semantics are easily reconciled if there is no hiding (and also no freeness), because in this case: Mod(SP)=Mod(Th(SP)) However, in presence of hiding, this equation does not hold! (examples: later) Till Mossakowski, Florian Rabe, Mihai Codescu Model-Level vs Theory-Level SemanticsThe Heterogeneous Tool Set (Hets) Structured and Specifications Development Graphs Benchmark Examples Some history model-level semantics ASL (Sannella, Wirsing 1983) specification in an arbitrary institution (Sannella, Tarlecki 1988) algebraic specification languages (CASL, 1990’s ) theory-level semantics Clear (Goguen, Burstall 1980) structured theories, conservative extensions and interpolation (Maibaum, Dimitrakos, Veloso 1980’s .) hidden information modules over inclusive institutions (Goguen, Ro¸su 2004) MathML, OpenMath, OMDoc (Kohlhase et al. 2000’s) ontologies and description logics (Wolter, Lutz Till Mossakowski, Florian Rabe, Mihai Codescu Model-Level vs Theory-Level SemanticsThe Heterogeneous Tool Set (Hets) Structured and Specifications Development Graphs Benchmark Examples Motivation of the talk Report on recent developments of heterogeneous tool set (which relies on model-level semantics) Report on recent of OMDoc/MMT (which relies on theory-level semantics) Discuss the pros and cons Can both semantics be reconciled? Till Mossakowski, Florian Rabe, Mihai Codescu Model-Level vs Theory-Level Semantics The Heterogeneous Tool Set (Hets) Structured and Specifications Development Graphs Benchmark Examples Till Mossakowski, Florian Rabe, Mihai Codescu Model-Level vs Theory-Level SemanticsThe Heterogeneous Tool Set (Hets) Structured and Specifications Development Graphs Benchmark Examples Logics currently supported by Hets CASL many-sorted first-order logic, partial functions, subsorting, datatypes (induction) CoCASL coalgebraic specification of reactive systems ModalCASL first-order modal logic HasCASL higher order logic, polymorphism, type classes Haskell pure functional programming language CspCASL combination of CASL with the process algebra CSP OWL DL description logic (DL) fragment of Web Ontology Language (OWL) Maude rewriting logic with preorder algebra semantics VSE a dynamic logic with Pascal-like programs RelScheme Relational schemes Propositional classical propositional logic SoftFOL softly typed first-order logic ( TPTP) Isabelle Isabelle’s higher-order logic Till Mossakowski, Florian Rabe, Mihai Codescu Model-Level vs Theory-Level SemanticsThe Heterogeneous Tool Set (Hets) Structured and Specifications Development Graphs Benchmark Examples Sound Integration of Heterogeneity logics are formalized as institutions (Goguen, Burstall 1984) logic translations are formalized as institution (co)morphisms (Goguen, Rosu 2002) logic translations embed or encode logical structure in a way that truth is preserved Grothendieck logic = flat combination of the logics in a logic graph (Diaconescu 2002) Hets provides an object-oriented interface for plugging in institutions and (co)morphisms Till Mossakowski, Florian Rabe, Mihai Codescu Model-Level vs Theory-Level SemanticsThe Heterogeneous Tool Set (Hets) Structured and Specifications Development Graphs Benchmark Examples Institutions σ Signatures Σ → Σ’ Sen σ Sentences Sen Σ Sen Σ’ Satisfaction |= |=Σ Σ’ Mod σ Models Mod Σ Mod Σ’ Till Mossakowski, Florian Rabe, Mihai Codescu Model-Level vs Theory-Level SemanticsThe Heterogeneous Tool Set (Hets) Structured and Specifications Development Graphs Benchmark Examples The Grothendieck Institution µσ:Σ→Φ (Σ′)(σ,µ) Signatures (Σ,Ι) → (Σ’,J) µ:J→I µI αSen σ Σ′ I I µ JSen Σ SenΦ (Σ’) Sen Σ’Sentences |= |=Satisfaction Σ Σ’ µI βMod σ Σ′ I I µ JMod Σ ModΦ (Σ’) Mod Σ’Models Till Mossakowski, Florian Rabe, Mihai Codescu Model-Level vs Theory-Level SemanticsThe Heterogeneous Tool Set (Hets) Structured and Specifications Development Graphs Benchmark Examples Syntax of Structured Specifications SP ::= BASIC-SPEC basic specification | SP then SP extension | SP and SP union | SP with SYMBOL-MAP renaming | SP hide SYMBOLS hiding | SPEC-NAME [PARAM*] reference to named spec LIBRARY-ITEM ::= spec SPEC-NAME [PARAM*] = SP end name a spec | view VIEW-NAME : SP to SP = SYMBOL-MAP end refinement between specifications Till Mossakowski, Florian Rabe, Mihai Codescu Model-Level vs Theory-Level Semantics