Early and late semantics

In the context of process calculus, early and late semantics correspond to two particular ways of understanding the semantics of input actions.

Intuition

Suppose that we have some processes P, which support an input prefix of the form

a(x). P

Intuitively, this prefix reads a value v from channel a, binds it to x, and continues as P[v/x].

Operationally, the semantics of this can be given in two ways.

In the early semantics version, this is given by allowing the process to emit a label for every value v:

\frac{
  v \textsf{ val}
}{
  a(x). P \xrightarrow{a(v)} P[v/x]
}

If the set of values is infinite, this means that a(x). P may evolve to infinitely many processes.

In the late semantics, this is given by allowing the binding of x to occur as a label instead:

\frac{
  
}{
  a(x). P \xrightarrow{a(x)} P
}

References

• The notion of early and late semantics appears to have been introduced in section 2.3 of

@article{milner_1992,
	title = {A calculus of mobile processes, {II}},
	volume = {100},
	doi = {10.1016/0890-5401(92)90009-5},
	pages = {41--77},
	number = {1},
	journaltitle = {Information and Computation},
	author = {Milner, Robin and Parrow, Joachim and Walker, David},
	date = {1992}
}

• A much more detailed discussion appears in

@article{milner_1993,
	title = {Modal logics for mobile processes},
	volume = {114},
	doi = {10.1016/0304-3975(93)90156-N},
	pages = {149--171},
	number = {1},
	journaltitle = {Theoretical Computer Science},
	author = {Milner, Robin and Parrow, Joachim and Walker, David},
	date = {1993},
}

• A proof that early and late semantics coincide for testing equivalence of CCS is given in

@article{ingolfsdottir_1995,
	title = {Late and early semantics coincide for testing},
	volume = {146},
	doi = {10.1016/0304-3975(94)00304-2},
	pages = {341--349},
	number = {1},
	journaltitle = {Theoretical Computer Science},
	author = {Ingólfsdóttir, Anna},
	date = {1995},
}