λProlog module finite-pic

sig finite-pic. % Three syntactic types are used: name (for names), action (for % actions), and proc (for processes). The type o denotes the type of % propositions. % The constructors for proc are 'null', 'taup', 'match', 'plus', % 'par', and 'nu' denote, respectively, the mull process, the tau % prefix, match prefix, the non-deterministic choice operator, the % parallel composition, and the restriction operator of the % pi-calculus. The input and output prefixes are encoded as in and % out. kind name, proc type. type null proc. type taup proc -> proc. type plus, par proc -> proc -> proc. type match, out name -> name -> proc -> proc. type in name -> (name -> proc) -> proc. type nu (name -> proc) -> proc. kind action type. type tau action. type up, dn name -> name -> action. % One step transition for free transitions type one proc -> action -> proc -> o. % One step transition for binding transitions type oneb proc -> (name -> action) -> (name -> proc) -> o.

module finite-pic. % Finite pi-calculus specification % A specification of the late transition system for the pi calculus. % This specification involves the bang constructor. % bound input oneb (in X M) (dn X) M. % free output one (out X Y P) (up X Y) P. % tau one (taup P) tau P. % match prefix one (match X X P) A Q :- one P A Q. oneb (match X X P) A M :- oneb P A M. % sum one (plus P Q) A R :- one P A R. one (plus P Q) A R :- one Q A R. oneb (plus P Q) A M :- oneb P A M. oneb (plus P Q) A M :- oneb Q A M. % par one (par P Q) A (par P1 Q) :- one P A P1. one (par P Q) A (par P Q1) :- one Q A Q1. oneb (par P Q) A (x\par (M x) Q) :- oneb P A M. oneb (par P Q) A (x\par P (N x)) :- oneb Q A N. % restriction one (nu x\P x) A (nu x\Q x) :- pi x\ one (P x) A (Q x). oneb (nu x\P x) A (y\ nu x\Q x y) :- pi x\ oneb (P x) A (y\ Q x y). % open oneb (nu x\M x) (up X) N :- pi y\ one (M y) (up X y) (N y). % close one (par P Q) tau (nu y\ par (M y) (N y)) :- oneb P (dn X) M , oneb Q (up X) N. one (par P Q) tau (nu y\ par (M y) (N y)) :- oneb P (up X) M , oneb Q (dn X) N. % comm one (par P Q) tau (par (M Y) T) :- oneb P (dn X) M, one Q (up X Y) T. one (par P Q) tau (par R (M Y)) :- oneb Q (dn X) M, one P (up X Y) R.