Process Algebra

  • Day1
    • Yoshiki explained why he needs encoding of process algebra; he plans to write a communication protocol as a term in process algebra and generate a set of possible sequences of atomic action which meets the term. In order to do it, he plans to write a calculator which, for a given term E in ACP (one of the equational theories in process algebra), gives a guarded term equivalent to E.
    • We had a sketch of a proof that such calculator exists; i.e., we showed, given an ACP term E, there is a sequence (a_i, E_i) of pairs of an atomic term a_i and a term E_i such that E is equivalent to Sigma_{i=1}^{i < N} a_i . E_i .
    • It seems straightforward to extract a calculator out of the (informal) proof of the above proposiion.
  • Day2
    • Nisse showed an old code for CBS(Prasad's) using mixed induction-coinduction.
    • Discussed where to use least and greatest fixed points. Nice explanation by Yoshiki wasn't bought by Nisse/Simon.
    • Algorithm for canonicalising ACP terms(expansion from parallel terms to sequential terms)
    • Writing down the proof of the above.
  • Day3 Y explained his interpretation of semantics to Martin. Became clear there are three relations between terms that shouldn't be confused.
    1. Eta equality ---> leading to ACP algebra
    2. Rewriting rel between the equiv class of terms ---> op.sem.
    3. Rewriting of parallel terms to sequential terms
    Y emphasis: 1 and 2 shouldn't be confused. (Mixed induction coinduction ...) (Presence or absence of infinite terms) (Y approach: finite terms + rewrite relation) (Nisse approach: infinite terms)
    Started implementing the 3rd rew. rules.
  • Day4: Implemented expansion from para terms to sequential terms.
  • Day5: The 1st goal (expansion) achieved. Vaguely thinking about semantics. Gathering material to be put in Agda Wiki, including Simon's expansion function and Nisse's CBS formalization.