Parallel evaluation for pairs

Robert J. Simmons, Frank Pfenning

This example is derived from Figure 5 in Substructural Operational Semantics as Ordered Logic Programming.

Parallel evaluation for pairs, plus unit

eunit : eval(unit) ->> return unit.

epair₁ : eval(pair E₁ E₂) ->> comp(pair₁) • eval(E₁) • eval(E₂).
epair₂ : comp(pair₁) • return(V₁) • return(V₂) ->> return(pair V₁ V₂).

elet₁ : eval(split E (λx₁.λx₂. E' x₁ x₂)) ->> comp(split₁ E') • eval(E).
elet₂ : eval(split₁ (λx₁.λx₂. E' x₁ x₂)) • return(pair V₁ V₂) ->> eval(E' V₁ V₂).

Example traces

The is no real computation to do in the language fragment described here; however, the fact way in which the evaluation of pairs produces multiple active eval predicates is apparent.

These traces also reveal something about the fact that the underlying operational semantics of the programming language we have implemented works; the interpreter attempts to apply rules starting at the left-hand side of the context and working towards the right-hand side. This means that, in this example, the left half of the pair is always evaluated first.

%trace * eval(pair unit (pair unit unit)).

eval(pair unit (pair unit unit))

comp(pair₁)•eval(unit)•eval(pair unit unit)

comp(pair₁)•return(unit)•eval(pair unit unit)

comp(pair₁)•return(unit)•comp(pair₁)•eval(unit)•eval(unit)

comp(pair₁)•return(unit)•comp(pair₁)•return(unit)•eval(unit)

comp(pair₁)•return(unit)•comp(pair₁)•return(unit)•return(unit)

comp(pair₁)•return(unit)•return(pair unit unit)

return(pair unit (pair unit unit))

%trace * eval(pair (pair unit unit) (pair unit unit)).

eval(pair (pair unit unit) (pair unit unit))

comp(pair₁)•eval(pair unit unit)•eval(pair unit unit)

comp(pair₁)•comp(pair₁)•eval(unit)•eval(unit)•eval(pair unit unit)

comp(pair₁)•comp(pair₁)•return(unit)•eval(unit)•eval(pair unit unit)

comp(pair₁)•comp(pair₁)•return(unit)•return(unit)•eval(pair unit unit)

comp(pair₁)•return(pair unit unit)•eval(pair unit unit)

comp(pair₁)•return(pair unit unit)•comp(pair₁)•eval(unit)•eval(unit)

comp(pair₁)•return(pair unit unit)•comp(pair₁)•return(unit)•eval(unit)

comp(pair₁)•return(pair unit unit)•comp(pair₁)•return(unit)•return(unit)

comp(pair₁)•return(pair unit unit)•return(pair unit unit)

return(pair (pair unit unit) (pair unit unit))