Correct Metric Semantics for a Biologically-Inspired Formalism

We investigate the semantics of a biologically-inspired formalism. This formalism was initially introduced by Cardelli as a "strand algebra" for DNA computing. For such a language we study and relate new formal semantic models. The mathematical framework is given by complete metric spaces in which the Banach fixed point theorem is used, various semantic functions are defined as fixed points of appropriate higher-order mappings. We define a new denotational semantics and compare it with the operational semantics introduced by Cardelli. We establish the formal relation between the operational and the denotational semantics by using an abstraction operator and a fixed point argument. In this way we establish the correctness of the denotational semantics with respect to the operational semantics.