| 總結: | Following previous work on CCS, we propose a compositional model for the
$\pi$-calculus in which processes are interpreted as sheaves on certain simple
sites. Such sheaves are a concurrent form of innocent strategies, in the sense
of Hyland-Ong/Nickau game semantics. We define an analogue of fair testing
equivalence in the model and show that our interpretation is intensionally
fully abstract for it. That is, the interpretation preserves and reflects fair
testing equivalence; and furthermore, any innocent strategy is fair testing
equivalent to the interpretation of some process. The central part of our work
is the construction of our sites, relying on a combinatorial presentation of
$\pi$-calculus traces in the spirit of string diagrams.
|
|---|
