# 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.
- Eta equality ---> leading to ACP algebra
- Rewriting rel between the equiv class of terms ---> op.sem.
- 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.