SIGPL2018Summer

pic.mod

module pic. %% file "pic.mod"

% eq X X.
% neq X Y :- eq X Y => fail.

one (inp X P) (dn X Y) (P Y).
one (out X Y P) (up X Y) P.
one (taup P) tau P.
one (par P Q) A (par P1 Q) :- one P A P1.
one (par P Q) A (par P Q1) :- one Q A Q1.
one (par P Q) tau (par P1 Q1) :- one P (up X Y) P1
                               , one Q (dn X Y) Q1.
one (par P Q) tau (par P1 Q1) :- one P (dn X Y) P1
                               , one Q (up X Y) Q1.
one (plus P Q) A P1 :- one P A P1.
one (plus P Q) A Q1 :- one Q A Q1.
one (nu P) A (nu Q) :- pi x\ one (P x) A (Q x).
one (mat X X P) A Q :- one P A Q.
% one (mis X Y P) A Q :- neq X Y, one P A Q.

%%%% scope extrusion %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
oneb (nu P) (up X) Q :- pi y\ one (P y) (up X y) (Q y). % open
one (par P Q) tau (nu y\ par (P1 y) Q1) :- % close
    oneb P (up X) P1, (pi y\ one Q (dn X y) Q1).
one (par P Q) tau (nu y\ par P1 (Q1 y)) :- % close
    (pi y\ one P (dn X y) P1), oneb Q (up X) Q1.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

oneb (par P Q) A (x\ par (P1 x) Q) :- oneb P A P1.
oneb (par P Q) A (x\ par P (Q1 x)) :- oneb Q A Q1.
oneb (plus P Q) A P1 :- oneb P A P1.
oneb (plus P Q) A Q1 :- oneb Q A Q1.
oneb (nu P) A (y\nu x\Q x y) :- pi x\ oneb (P x) A (y\Q x y).
oneb (mat X X P) A Q :- oneb P A Q.
% oneb (mis X Y P) A Q :- neq X Y, oneb P A Q. 

pic.sig

sig pic. %% file "pic.sig"

kind n  type.
kind p  type.
kind a  type.

type a, b  n.

type up  n -> n -> a.
type dn  n -> n -> a.
type tau           a.

type null  p.
type inp   n -> (n -> p) -> p.
type out   n -> n -> p -> p.
type taup  p -> p.
type par   p -> p -> p.
type plus  p -> p -> p.
type nu    (n -> p) -> p.
type mat   n -> n -> p -> p.
% type mis   n -> n -> p -> p.

% type fail   o.
% type eq    n -> n -> o.
% type neq   n -> n -> o.

type one   p -> a -> p -> o.
type oneb  p -> (n -> a) -> (n -> p) -> o.

pic.thm

Specification "pic".

CoDefine bisim : p -> p -> prop by
bisim P Q
  := (forall A P1, {one P A P1} -> exists Q1, {one Q A Q1} /\ bisim P1 Q1)
  /\ (forall X P1, {oneb P (up X) P1} -> exists Q1, {oneb Q (up X) Q1} /\
                                         nabla w, bisim (P1 w) (Q1 w))
  /\ (forall A Q1, {one Q A Q1} -> exists P1, {one P A P1} /\ bisim Q1 P1)
  /\ (forall X Q1, {oneb Q (up X) Q1} -> exists P1, {oneb P (up X) P1} /\
                                         nabla w, bisim (P1 w) (Q1 w)).

% Bisimulation is an equivalence

Theorem bisim_refl : forall P, bisim P P.
abort.

Theorem bisim_sym : forall P Q, bisim P Q -> bisim Q P.
abort.

Theorem bisim_trans : forall P Q R, bisim P Q -> bisim Q R -> bisim P R. 
abort.