Weeknotes 2026-W31 [2026-W31]

This weeknotes is two days late, but I was suffering from a bout of rheumatoid symptoms so that's my excuse.

One of the most common birds in Canberra is also one of the loveliest.

CCS with Termination [loc-0051]

As part of Xin Lu's project we needed to come up with a version of CCS that supports explicit termination in the style of ACP. There is a paper by Luca Aceto and Matthew Hennessy which introduces a termination predicate, but they require that a nondeterministic choice P + Q is judged terminating (written P + Q \checkmark ) only when both P \checkmark and Q \checkmark . In other words, a process is only terminating if it has no choice but to terminate.

In our case, we want a judgement for possible termination, not guaranteed termination. So we had to come up with our own notions. We've formalised this in Isabelle, but what follows is the same but presented as Forester notes. Eventually, these notes may become part of another research notebook or even lecture notes.

DefinitionSyntax of (non-recursive) CCS [pa-0001]

The Calculus of Communicating Systems (CCS) is a process algebra with the following basic syntax.

\begin {array}{lcll} \alpha & & & \text {(names)}\\ a & ::= & \alpha \mid \overline {\alpha } \mid \tau & \text {(actions, co-actions, and internal moves)}\\ P & ::= & \textbf {0} & \\ & \mid & a.P & \text {(action prefixing)} \\ & \mid & \sum _{i \in I} P_i & \text {(nondeterministic choice)} \\ & \mid & P | Q & \text {(parallel composition)} \\ & \mid & P \setminus \alpha & \text {(restriction)} \\ & \mid & P [ f ] & \text {(renaming)} \end {array}

In the above, f denotes a valid renaming function that satisfies the side-condition \forall a.\; f(\overline {a}) = \overline {f(a)}. Here we have naturally extended the co-action notation (\overline {\alpha }) to an operation on actions a, where \overline {\overline {a}} = a and \overline {\tau } = \tau .

We allow for infinite sums in nondeterministic choice. To recover finite choice, we use a two element index set like \mathbb {B} = \{\top ,\bot \}, as follows:

P + Q \equiv \sum _{i \in \mathbb {B}} R_i\; \text {where}\ R_\top = P\ \text {and}\ R_\bot = Q

DefinitionOperational semantics for (non-recursive) CCS [pa-0002]

We assign an operational semantics to CCS by describing a series of transition rules P \xrightarrow {a} Q inductively as follows:

\begin {gather*} \dfrac { }{a.P \xrightarrow {a} P} \quad \dfrac {P_k \xrightarrow {a} P'}{\sum _{i \in I} P_i \xrightarrow {a} P'} \\[2em] \dfrac { P \xrightarrow {a} P'}{P|Q \xrightarrow {a} P'|Q} \quad \dfrac { Q \xrightarrow {a} Q'}{P|Q \xrightarrow {a} P|Q'} \dfrac { P \xrightarrow {a} P' \quad Q \xrightarrow {\overline {a}} Q'}{P|Q \xrightarrow {\tau } P'|Q'} \\[2em] \dfrac { P \xrightarrow {a} P' \quad a \notin \{\alpha , \overline {\alpha }\}}{ P\setminus \alpha \xrightarrow {a} P' \setminus \alpha } \quad \dfrac { P \xrightarrow {a} P'}{ P [ f ] \xrightarrow {f(a)} P' [ f ]} \end {gather*}

Let the relation P \xrightarrow {\sigma }^\ast Q denote the reflexive, transitive closure of the above step relation, where \sigma denotes a finite trace (a finite sequence of actions):

\dfrac { }{P \xrightarrow {\varepsilon }^\ast P} \quad \dfrac {P \xrightarrow {a} P' \quad P' \xrightarrow {\sigma }^\ast Q}{P \xrightarrow {a\sigma }^\ast Q}

DefinitionPartial trace semantics for (non-recursive) CCS [pa-0003]

A simple denotational semantics for CCS is in terms of partial traces: finite sequences of actions.

\begin {array}{lcl} \llbracket \textbf {0} \rrbracket _\text {PT} & = & \{ \varepsilon \} \\ \llbracket a.P \rrbracket _\text {PT} & = & \{ a\sigma \mid \sigma \in \llbracket P \rrbracket _\text {PT} \} \cup \{ \varepsilon \}\\ \llbracket \sum _{i \in I} P_i \rrbracket _\text {PT} & = & \{ \varepsilon \} \cup \bigcup _{i \in I} \llbracket P_i \rrbracket _\text {PT} \\ \llbracket P|Q \rrbracket _\text {PT} & = & \bigcup _{\sigma \in \llbracket P \rrbracket _\text {PT}} \bigcup _{\rho \in \llbracket Q \rrbracket _\text {PT}} \sigma \bowtie \rho \\ \llbracket P \setminus \alpha \rrbracket _\text {PT} & = & \{ \sigma \in \llbracket P \rrbracket _\text {PT} \mid \alpha \notin \sigma \land \overline {\alpha } \notin \sigma \} \\ \llbracket P [ f ] \rrbracket _\text {PT} & = & \{ \hat {f}(\sigma ) \mid \sigma \in \llbracket P \rrbracket _\text {PT} \} \end {array}

The trace merge operator \bowtie is defined as follows:

\begin {array}{lcl} \sigma \bowtie \varepsilon &=& \{\sigma \} \\ \varepsilon \bowtie \sigma &=& \{\sigma \} \\ a\sigma \bowtie b\rho &=& \{ a\varsigma \mid \varsigma \in \sigma \bowtie b\rho \} \\ &\cup & \{ b\varsigma \mid \varsigma \in a\sigma \bowtie \rho \} \\ &\cup & \{ \tau \varsigma \mid \varsigma \in \sigma \bowtie \rho \land a = \overline {b} \} \\ \end {array}

TheoremSoundness and adequacy of partial trace semantics for (non-recursive) CCS [pa-0004]

The finite partial trace denotational semantics of CCS gives exactly those finite partial traces reachable via the operational semantics.

\llbracket P \rrbracket _\text {PT} = \{ \sigma \mid \exists Q.\ P \xrightarrow {\sigma }^\ast Q \}

Proof.

Proved by induction on P.

Explicit termination for (non-recursive) CCS [pa-0005]

We add to syntax of CCS an additional process constant, \textbf {1}, which, like \mathbf {0}, has no rules in the operational semantics, and whose finite partial traces are just \llbracket \textbf {1} \rrbracket _\text {PT} = \{\varepsilon \}.

The difference between \textbf {0} and \textbf {1} only comes in once we introduce a notion of possible successful termination. Intuitively, we want the ability to denote when it is OK for a process to stop.

DefinitionPossible termination predicate for CCS with \textbf {1} [pa-0006]

We define an inductive judgement P \checkmark , where P is a process in CCS augmented with an additional process constant \textbf {1}:

\begin {gather*} \dfrac { }{ \textbf {1} \checkmark } \quad \dfrac {P_k \checkmark }{\sum _{i \in I} P_i \checkmark } \\[2em] \dfrac { P \checkmark \quad Q \checkmark }{P|Q \checkmark } \dfrac { P \checkmark }{ P\setminus \alpha \checkmark } \quad \dfrac { P \checkmark }{ P [ f ] \checkmark } \end {gather*}

DefinitionFinite completed trace semantics for CCS with \textbf {1} [pa-0007]

We offer a denotational semantics for CCS augmented with a \textbf {1} constant, denoting successful termination. Unlike our partial trace semantics, this semantics only includes finite completed traces — traces where the process has terminated.

\begin {array}{lcl} \llbracket \textbf {0} \rrbracket _\text {CT} & = & \emptyset \\ \llbracket \textbf {1} \rrbracket _\text {CT} & = & \{ \varepsilon \} \\ \llbracket a.P \rrbracket _\text {CT} & = & \{ a\sigma \mid \sigma \in \llbracket P \rrbracket _\text {CT} \}\\ \llbracket \sum _{i \in I} P_i \rrbracket _\text {CT} & = & \bigcup _{i \in I} \llbracket P_i \rrbracket _\text {CT} \\ \llbracket P|Q \rrbracket _\text {CT} & = & \bigcup _{\sigma \in \llbracket P \rrbracket _\text {CT}} \bigcup _{\rho \in \llbracket Q \rrbracket _\text {CT}} \sigma \bowtie \rho \\ \llbracket P \setminus \alpha \rrbracket _\text {CT} & = & \{ \sigma \in \llbracket P \rrbracket _\text {CT} \mid \alpha \notin \sigma \land \overline {\alpha } \notin \sigma \} \\ \llbracket P [ f ] \rrbracket _\text {CT} & = & \{ \hat {f}(\sigma ) \mid \sigma \in \llbracket P \rrbracket _\text {CT} \} \end {array}

The trace merge operator \bowtie is defined exactly as in the partial trace semantics.

TheoremSoundness and adequacy of finite completed trace semantics for CCS [pa-0008]

The finite completed trace semantics of CCS gives exactly those finite partial traces reachable via the operational semantics that end in a terminating state.

\llbracket P \rrbracket _\text {CT} = \{ \sigma \mid \exists Q.\ P \xrightarrow {\sigma }^\ast Q \land Q \checkmark \}

Proof.

Proved by induction on P.

DefinitionA translation to turn partial traces into completed traces [pa-0009]

Define a syntactic transformation on CCS terms (augmented with \textbf {1}) \Upsilon as follows:

\begin {array}{lcl} \Upsilon (\textbf {0}) &=& \textbf {1} \\ \Upsilon (\textbf {1}) &=& \textbf {1} \\ \Upsilon (a.P) &=& \textbf {1} + a.\Upsilon (P) \\ \Upsilon (\sum _{i \in I} P_i) &=& \textbf {1} + \sum _{i \in I} \Upsilon (P_i) \\ \Upsilon (P | Q) &=& \Upsilon (P) | \Upsilon (Q)\\ \Upsilon (P \setminus \alpha ) &=& \Upsilon (P) \setminus \alpha \\ \Upsilon (P [ f ]) &=& \Upsilon (P) [ f ] \end {array}

TheoremCorrectness of the \Upsilon translation [pa-000A]

Our syntactic transformation \Upsilon gives a process whose completed traces are the same as the partial traces of the original process.

\llbracket P \rrbracket _\text {PT} = \llbracket \Upsilon (P) \rrbracket _\text {CT}

Proof.

A very straightforward structural induction on P, where each case follows from the definitions.

The Dark Night of Mathematics [loc-0054]

You know the drill by now. Another article I read about the damage LLMs are doing to our intellectual pursuits. This is a deeply personal reflection from a mathematician, Kirwin Hampshire: The Dark Night of Mathematics.

There is nothing I can do. There may be nothing you can do. I have no prescriptions, policy recommendations, or coherent call to action. I just want to be honest and open about my emotional and spiritual response. I want to feel seen. I want folks like me to feel seen. I need the architects of our new mathematical paradigm to look me in the eye and acknowledge our shared humanity and soul before they deliver the coup de grâce. I need, most of all, for us to understand what we are really doing.

Church Music Corner › 10th Sunday after Pentecost 2026 [loc-0053]

Deus in adiutórium meum inténde: Dómine ad adiuvándum me festína: confundántur et revereántur inimíci mei, qui quærunt ánimam meam.

I was once again the director of our choir at All Saints Ainslie, for the special Missing Persons Sunday today, with representatives from the Australian Federal Police present to offer special reflections and awareness about those who are missing in our territory and support their loved ones, many of whom were in attendance. We performed Rachmaninoff's Bogoroditse Devo:

Богородице Дево, радуйся, Rejoice, virgin mother of God,
Благодатная Марие, Господь с тобою. Mary, full of grace, the Lord is with you.
Благословена ты в женах, Blessed are you among women,
и благословен плод чрева твоего, and blessed is the fruit of your womb,
яко Спаса родила еси душ наших. for you have borne the Saviour of our souls.

References

    Reference. Adding Action Refinement to a Finite Process Algebra [aceto-hennessy-1994]

    Context

      Liam O'Connor › Weeknotes [loc-001B]