Operational Semantics for Affine HOPLA

                         Mikkel Nygaard
                         September 2005


These notes describe an operational semantics for Affine
HOPLA [Win98].

The operational semantics is based on relations of the form 

  C(-) |- t --> t'        (|- C(t):!P)

Inutitively, the proces C(t) may perform an (atomic, anonymous)
action and become t'. Contexts are built from destructor terms
of Affine HOPLA and, as such, are *linear* meaning that for C(t)
to be active, t has to be active. 

An alternative view (contexts as actions, see e.g. [Sob04]) is
that t may perform the action C and become t'. But this then
involves open terms (t) and contexts (C) which don't correspond
to atomic actions like those for HOPLA. I am greatful to Dave
Turner at Cambridge for suggesting the simpler view above.

A standard transition system a la HOPLA [NW02b] with transitions 

  t --a--> t'    (|- t:P, P:a:P')

can be understood as a derived notion by defining a set of
contexts C_a that correspond to atomic actions and then saying
t --a--> t' if C_a(-) |- t --> t'.


                     Operational Semantics

Linear contexts:

C ::= - | C u | pi_b C | [C > !x => t] | rep C | [u > x*y => C] 
    | [C > x*y => C'(x)] | [C > x*y => C'(y)]

We'll use the shorthand [e => C] for C in sequence e of tensor
matches:

   [epsilon => C]  =_def  C
[e, u > x*y => C]  =_def  [e => [u > x*y => C]]

Operational rules (typing information omitted):

Rules for rec, sum and prefix:

C(-) |- t[rec x.t/x] --> t'
---------------------------
C(-) |- rec x.t --> t'

C(-) |- t_j --> t'
------------------------ j in I
C(-) |- sum_i t_i --> t'

---------------------------
[e => -] |- !t --> [e => t]


Rules for variables, moving focus from right to left of tensor matches

C([- > x*y => C'(x)]) |- u --> t'
---------------------------------
C([u > x*y => C'(-)]) |- x --> t'

C([- > x*y => C'(y)]) |- u --> t'
---------------------------------
C([u > x*y => C'(-)]) |- y --> t'


Beta-reduction rules for constructors

C([e => -]) |- t[u/x] --> t'
----------------------------
C([e => -] u) |- \x.t --> t'

C([e => -]) |- t --> t'
-----------------------------
C(pi_b [e => -]) |- bt --> t'

C([e => -]) |- t --> t'
-------------------------------
C(rep [e => -]) |- abs t --> t'

C([e => -]) |- t[u/x] --> t'
------------------------------------
C([[e => -] > !x => t]) |- !u --> t'

C([e => C'(-)[u2/y]]) |- u1 --> t'
--------------------------------------------
C([[e => -] > x*y => C'(x)]) |- u1*u2 --> t'

C([e => C'(-)[u1/x]]) |- u2 --> t'
--------------------------------------------
C([[e => -] > x*y => C'(y)]) |- u1*u2 --> t'


Rules for moving destructor terms into context:

C(- u) |- t --> t'
------------------
C(-) |- t u --> t'

C(pi_b -) |- t --> t'
---------------------
C(-) |- pi_b t --> t'

C(rep -) |- t --> t'
--------------------
C(-) |- rep t --> t'

C([- > !x => t]) |- u --> t'
----------------------------
C(-) |- [u > !x => t] --> t'

C([u > x*y => -]) |- t --> t'
-----------------------------
C(-) |- [u > x*y => t] --> t'


                  Properties of the Semantics


Commutativity of contexts:

C(-) |- t --> t'    iff   - |- C(t) --> t'

Proof: By structural induction on C.


Conjecture on composition of contexts:

  [C(-) > !x => C'(x)] |- t --> t'

      iff there exists t'' s.t.

  C(-) |- t --> t''  and   C'(-) |- t'' --> t'


Type-correctness:

Suppose |- C(t):!P. If C(-) |- t --> t', then |- t':P.

Proof: By rule induction.


Soundness (w.r.t path semantics [NW04]):

If C(-) |- t --> t', then [[!t']] is a subset of [[C(t)]].

Proof: By rule induction (also: follows by strong
correspondence).


Adequacy:

If [[C(t)]] != Ø, then there exists t' s.t. C(-) |- t --> t'.

Proof: Follows by strong correspondence.


Strong Correspondence (w.r.t. presheaf semantics [NW02a]):

Suppose |- C(t):!P. Then [[C(t)]] iso sum_d [[!t_d]] where d
ranges over derivations C(-) |- t --> t_d.

Proof: In three steps as in [NW02a]:
Step 1: Define ordinal size measure on terms of finitary fragment.
Step 2: Prove the result for finitary fragment by well-founded induction.
Step 3: Extend to full fragment using standard technique.
[To be completed]

                     HOPLA-like Transitions

We derive an operational semantics with HOPLA-like transitions
for terms of all types [NW02, NW04].

Actions:

  a ::= ! | ba | u->a | abs a | a*bot | bot*a

Corresponding contexts C_a (by induction on a):

      C_! = -
     C_ba = C_a(pi_b -)
   C_u->a = C_a(- u)
  C_abs a = C_a(rep -)
  C_a*bot = [- > x*y => [C_a(x) > !x' => !(x'*y)]]
  C_bot*a = [- > x*y => [C_a(y) > !y' => !(x*y')]]

Transitions:

  C_a(-) |- t --> t'
  ------------------
  t --a--> t'

---where |- t:P, P:a:P' (so that |- C_a(t):!P' and |- t':P').



                      Example derivations


Example 1. Nondeterministic dataflow process Two, producing an
inifinite sequence of a's and b's on two output lines. It is
nondeterministic, but the two lines are "entangled" such that
the output on one line determines the output on the other line,
schematically:

   __________
  |          | aaba...
  |   Two    |------
  |          | aaba...
  |__________|------
  
Formally, the term is

    Two = rec S.[S > x*y => a!x*a!y + b!x*b!y]

We expect

    Two --a*bot--> [Two > x*y => x*a!y] 

i.e.

    C_a*bot(-) |- Two --> [Two > x*y => x*a!y]

Here's the derivation:

-----------------------------------------------------
[Two > x*y => -] |- !(x*a!y) --> [Two > x*y => x*a!y]
--------------------------------------------------------------------
[Two > x*y => [- > !z' => !(x'*a!y)]] |- !x --> [Two > x*y => x*a!y]
--------------------------------------------------------------------------
[Two > x*y => [pi_a - > !z' => !(x'*a!y)]] |- a!x --> [Two > x*y => x*a!y]
--------------------------------------------------------------------------
C_a*bot([Two > x*y => -]) |- a!x*a!y --> [Two > x*y => x*a!y]
-----------------------------------------------------------------------
C_a*bot([Two > x*y => -]) |- a!x*a!y + b!x*b!y --> [Two > x*y => x*a!y]
-----------------------------------------------------------------------
C_a*bot(-) |- [Two > x*y => a!x*a!y + b!x*b!y] --> [Two > x*y => x*a!y]
-----------------------------------------------------------------------
C_a*bot(-) |- Two --> [Two > x*y => x*a!y]


Example 2. Considers the "problematic" term [(\z.t)*u > x*y => x
y] (cf. [Nyg03]).

    C_a(-) |- t[u/z] --> t'
    -----------------------
    C_a(- u) |- \z.t --> t'
    ----------------------------------------
    C_a([- > x*y => x y]) |- (\z.t)*u --> t'
    ----------------------------------------
    C_a([(\z.t)*u > x*y => - y]) |- x --> t'
    ----------------------------------------
    C_a([(\z.t)*u > x*y => -]) |- x y --> t'
    ----------------------------------------
    C_a(-) |- [(\z.t)*u > x*y => x y] --> t'
    
and so
    
    [(\z.t)*u > x*y => x y] --a--> t'   iff   t[u/z] --a--> t'

as wanted.


                           References


[Win98] G. Winskel: A Linear Metalanguage for Concurrency. AMAST'98.

[NW02a] M. Nygaard and G. Winskel: Linearity on Process Languages. LICS'02.

[NW02b] M. Nygaard and G. Winskel: HOPLA---A Higher-Order
Process Language. CONCUR'02.

[NW04]  M. Nygaard and G.Winskel: Domain Theory for
Concurrency. TCS 316:153-190, 2004.

[Nyg03] M. Nygaard: Domain Theory for Concurrency. PhD
Thesis. University of Aarhus, 2003.

[Sob04] P. Sobocinski. Deriving process congruences from
reaction rules. PhD Thesis. University of Aarhus, 2004.