Metric Denotational Semantics for BPPA
Thuy Duong Vu · 2005
Abstract. Program algebra (PGA) is a basic and simple concept of a programming language which has been formulated by Bergstra and Loots in [9, 10]. Behaviors for programs in PGA can be given in the Basic Po-larized Process Algebra (BPPA). Based on the theory of metric spaces as introduced in [5], we give a denotational semantics for BPPA. Models of BPPA are considered as complete metric spaces of a suitable mathemat-ical structure. We show that a space consisting of projective sequences is an appropriate model for BPPA. Furthermore, using Banach's xed point theorem, we prove that the specication of a regular process in this space has a unique solution. This result suggests a model consisting of regular processes. We complete the paper by comparing several models of BPPA. 1