Fully Abstract Denotational Models for Nonuniform Concurrent Languages

摘要

Full abstractness of denotational models with respect to operational ones for twoconcurrent languages is investigated. The languages are nonuniform in the following sense: they have individual variables which store values, and the elementary actions are (mainly) value assignments to these variables. The first language L1 has parallel composition but no communication, whereas the second one L2 has CSP-like communications in addition. For each of Li (i = 1, 2), an operational model Oi is introduced in terms of a Plotkin-style transition system, while a denotational model Di for Li is defined compositionally using interpreted operations of the language, with meanings of recursive programs as fixed points in appropriate complete metric spaces. The full abstractness is shown by means of a context with parallel composition: given two statements s1 and s2 with different denotational meanings, a suitable statement T is constructed such that the operational meanings of (s1 is equivalent to T) and (s2 is equivalent to T) are distinct. A combinatorial method for constructing such T is proposed. Thereby the full abstractness of D1 and D2 with respect to O1 and O2 respectively is established. That is, Di is most abstract of those models C which are compositional and satisfy Oi = alpha circle C for some abstraction function alpha (i = 1, 2).