Taverna 2 Semantics

Language

• Channel names
• Channel types
• Parallel and sequential composition
  • control links are sequential composition
• Asynchronous execution

• Every channel has a type
• Types are either base or products or obtained by applying Computational Monads such as List Monad
• Product types interplay with Monads
  • (various) tensor products TA x TB --> T(A x B)
    • iterations
  • Users (Paul Fisher) say that having a default iteration strategy causes trouble. This is consistent with the fact that monads come with their explicit constructs.

Mathematical Structures

The structures involved are all canonical:

• Free semi-lattices (ie powersets)
• Free monoids (ie sequences)
• Monoid actions (also known as M-Sets)
• Tensor products

We start with the natural numbers N and take N* ie the set of all sequences of natural numbers. This forms a (free) monoid (over N) with the empty string as unit and concatenation as multiplication.

An action of a monoid M over a set S is an operation

 . : M x S --> S

which respects the monoidal structure:

 (m1.s).(m2.s) = (m1.m2).s
 e.s = s = s.e

(One uses the same symbol both for monoid multiplication and monoid action.)

A semilattice is a set L with a binary join operation

 + : L x L --> L

which is associative, symmetric and absorptive, the latter meaning

a+a = a

The powerset (set of sets) operation P produces free semi-lattices with union as join.

There is a tensor product of semi-lattices which classifies bilinear maps. One nice property is that the tensor product of two free semilattices is the free semilattices over the cartesian product of their bases:

P(S) * P(T) = P(S x T)

One can also take semi-lattices over M-sets (ie monoid actions) instead of simple sets and the same constructions can be carried out.

So for (one composition of) Taverna 2 jobs one ends with:

The tensor product of free semi-lattices over actions of the free monoid over the natural numbers.

Because of the pervasive use of free constructions a lot of commutative properties will hold.

These are the building blocks for the semantics of jobs in Taverna 2.

References

• A Structural approach to Operational Semantics
• Computational lambda calculus
• Computational lambda calculus - semantics
• Computational Interpretations of Linear Logic
• Semantics of Weakening and Contraction