Event-Structures / event-struct

Mechanized Theory of Event Structures
MIT License
16 stars 1 forks source link

Labelled posets and their homomorphisms #116

Closed eupp closed 3 years ago

eupp commented 3 years ago

This PR is a retake on pomset.v. It features several changes.

  1. In pomset.v the Pomset structure is renamed into LPoset (labeled partially ordered set) to avoid confusion. A labelling function is embedded into LPoset hierarchy.

  2. An axiom of finite cause is removed from LPoset (top of the hierarchy) and is moved to a new structure Elem.eventStruct that is an elementary event structure (which is a labelled poset + axiom if finite cause). Elementary event structures are then inherited by various subclasses of prime event structures, that is prime event structures with binary and general conflict.

  3. Definition of homomorphism between labelled posets is given, together with basic combinators (id, tr) and notations.