In: Proceedingsof the Fifth Annual IEEE Symposium on Logic in Computer Science, 1990, Philadelphia, PA, USA, pages 200-207. Los Alamitos, CA, USA: IEEE Comput. Soc. Press, 1990.
Abstract: The relevance of a form of cut elimination theorem for linear logic tensor theories to the concept of a process on a Petri net is discussed. The discussion is based on two definitions of processes given by E. Best and R. Devillers (1987). It is noted that the cut reduced proofs form a process under the finer of these definitions. Using a strongly normalizing rewrite system and a weak Church-Rosser theorem, it is shown that each class of the coarser process definition contains exactly one of these finer classes which can therefore be viewed as a normal process representative. The relevance of these rewrite rules to the categorical approach of P. Degano is also discussed.
Keywords: normal process representatives; cut elimination theorem; linear logic tensor theory; (strongly) normalizing rewrite system; (weak) Church-Rosser theorem; categorical approach.