(* Exercise 4.1 Consider the following recursive types describing a calculus of communicating processes in the style of CCS, and its operational semantics. *) Inductive Process : Set := dead : Process | say : nat->Process->Process | listen : (nat->Process)->Process | par : Process->Process->Process. Inductive Action : Set := Transmit : nat->Action | Receive : nat->Action. Inductive Trans : Process ->Action->Process->Prop := tsay : (v:nat) (p:Process) (Trans (say v p) (Transmit v) p) | tlisten: (f:nat->Process) (v:nat) (p :Process) ((f v)=p)-> (Trans (listen f) (Receive v) p) | tpar1 : (p1,p2,p3,p4:Process) (v:nat) (Trans p1 (Transmit v) p2)-> (Trans p3 (Receive v) p4)-> (Trans (par p1 p3) (Transmit v) (par p2 p4)) | tpar2 : (p1,p2,p3,p4:Process) (v:nat) (Trans p1 (Receive v) p2)-> (Trans p3 (Transmit v) p4)-> (Trans (par p1 p3) (Transmit v) (par p2 p4)) | tpar3 : (p1,p2,p3,p4:Process) (v:nat) (Trans p1 (Receive v) p2)-> (Trans p3 (Receive v) p4)-> (Trans (par p1 p3) (Receive v) (par p2 p4)). (* 1. Prove that dead cannot evolve any further. 2. Show that any communicating system where there is at least two process in parallel evolves into a system also verifying this property. 3. Prove that in one reduction step, the process (par (listen [x:nat](say x dead)) (say O dead)) can only evolve into (par (say O dead) dead). 4. Czy relacja Trans jest konfluentna? Udowodnij, ze tak, lub ze nie. 5. Zastanow sie, czy relacja Trans jest silnie normalizujaca. Pokaz przyklad procesow, ktore ewoluuja do samych siebie w wielu krokach, badz udowodnij, ze takich nie ma. 6. Zaproponuj kolejny ciekawy lemat do udowodnienia i udowodnij go :) *)