7 Definitions of combinators

General simple composition

Section 3.1 introduces the simple composition combinator. Given n classes X₁, …, X_n, of types T₁, …, T_n respectively, and given a function F of type Loc → T₁ → ⋅⋅⋅ → T_n → Bag(T), one can define the class F o (X₁,,X_n). This combinator is defined in terms of one of the Logic of Events’ primitive combinators. Given n classes X₁, …, X_n, of types T₁, …, T_n respectively, and given a function F of type Loc → Bag(T₁) →→ Bag(T_n) → Bag(T), the class F O (X₁; ⋅⋅⋅ ;X_n) is one of the Logic of Events’ primitive combinator. The class F o (X₁,,X_n) is defined as:

⋃ ⋃ (λloc.λb1....λbn. ⋅⋅⋅ F loc x1 ⋅⋅⋅ xn) O (X1 ;⋅⋅⋅;Xn ) x1∈b1 xn∈bn

Until

The binary infix operator until can then be defined in terms of this more general simple composition combinator as follows:

import bag-null;;

class until X Y =
let F loc b1 b2 = if bag-null b2 then b1 else {}
in F o (X,Prior(Y)) ;;

infix until;;

The bag-null function is a function that returns true iff its argument is the empty bag. Note that using an infix declaration, one can declare infix operators in EventML.

Once

The Once operator can be defined in terms of the until operator as follows:

class Once X = (X until X) ;;

Output

The Output operator can be defined in terms of the Once operator as follows:

class Output b = Once(b o ());;

The “at” combinator

The binary infix operator @ can be defined in terms of the simple combinator as follows:

import bag-deq-member ;;
class @ X locs =
let F loc x = if bag-deq-member (op =) loc locs then {x} else {}
in F o X ;;
infix @ ;;

(Note that this code is not valid EventML code because @ is not a valid identifier.)

Parallel combination

The parallel combinator can be defined in terms of the more general simple combinator as follows:

class || X Y = (\loc.\b1.\b2.b1++b2) o (X,Y) ;;
infix || ;;

(Note that this code is not valid EventML code because || is not a valid identifier.)

Disjoint union

The disjoint union class combinator. X (+) Y is a class of type A + B that recognizes both X-events and Y-events. The observations made by X are tagged with inl and the observations made by Y are tagged with inr:

class X (+) Y = ((\_.\x.{inl(x)}) o X) || ((\_.\x.{inr(x)}) o Y) ;;

If (and only if) e is both an X-event and a Y-event, X (+) Y(e) is a bag with two elements.

SM1-class, …, Memory1, …

For any n, the combinators SMnclass and Memoryn are defined in section 4.