METRIC POMSET SEMANTICS FOR A CONCURRENT LANGUAGE WITH RECURSION

We study the semantics of a simple language with concurrency and recursion. Our semantic domain consists of (sets of) finite and infinite partially ordered multisets (pomsets) in order to model true concurrency (i.e. non-interleaved parallel execution). It will be shown that the set of pomsets can be turned into a complete ultra-metric space. With the induced notion of convergence, it is possible to provide meaning to infinite computations. Operational and denotational semantics for the considered language are provided and their equivalence is established by showing that both are fixed points of a contracting higher order operator. In a final section we give a tentative denotational semantics for an extension of the language with synchronization.