Hets - the Heterogeneous Tool Set

Copyright(c) Dominik Luecke, Uni Bremen 2007
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerluecke@informatik.uni-bremen.de
Stabilityexperimental
Portabilityportable Definition of morphisms for temporal logic copied from "Propositional.Morphism" Ref. Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki. What is a Logic?. In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser. 2005.
Safe HaskellSafe-Inferred

Temporal.Morphism

Description

 

Synopsis

Documentation

data Morphism

The datatype for morphisms in temporal logic as maps of sets

Constructors

Morphism 

Fields

source :: Sign
 
target :: Sign
 
propMap :: Map Id Id
 

Instances

Eq Morphism 
Ord Morphism 
Show Morphism 
ShATermConvertible Morphism 
Pretty Morphism 
Typeable * Morphism 
Category Sign Morphism

Instance of Category for temporal logic

Sentences Temporal FORMULA Sign Morphism Symbol

Instance of Sentences for temporal logic

StaticAnalysis Temporal BASIC_SPEC FORMULA () () Sign Morphism Symbol Symbol

Static Analysis for propositional logic

Logic Temporal () BASIC_SPEC FORMULA () () Sign Morphism Symbol Symbol ()

Instance of Logic for propositional logc

pretty :: Pretty a => a -> Doc

idMor :: Sign -> Morphism

Constructs an id-morphism

isLegalMorphism :: Morphism -> Result ()

Determines whether a morphism is valid

composeMor :: Morphism -> Morphism -> Result Morphism

Composition of morphisms in temporal Logic

inclusionMap :: Sign -> Sign -> Morphism

Inclusion map of a subsig into a supersig

mapSentence :: Morphism -> FORMULA -> Result FORMULA

sentence translation along signature morphism here just the renaming of formulae

mapSentenceH :: Morphism -> FORMULA -> FORMULA

applyMap :: Map Id Id -> Id -> Id

Application function for propMaps

applyMorphism :: Morphism -> Id -> Id

Application funtion for morphisms