Theoretically

〈pi-Calculus in (Co)Inductive Type Theory〉才看到 syntax 定義就暗喊不妙 ─ 那定義是 inductive 的！這樣如果要表示一個 coninductively-defined process 的話，就得用 replication operator '!' 模擬。例如持續往 channel x 輸出 t 的 process 'tick' 可自然地寫成

如果用 replication operator 模擬就得寫成

等於是無窮多個 processes 在接力。如果用起來真的很不方便，大概就要整套 pi-Calculus 重寫一次了…

--
理論上用 inductive definition 當然很快樂 XD。