On denotational versus predicative semantics (Q753499)

The paper succeeds to make a detailed analysis of two alternative styles for defining the semantics of programming languages: the denotational (or descriptive) style, and the predicative (or prespective) style. The results comprise: specific definitions of the two approaches, relationship between the two semantics over the variation of the following coordinates: deterministic and non-deterministic programs, computational induction and fixed-point induction approaches to recursion and its interaction to non-determinism, different notions of program correctness: partial, robust, and total correctness. Sections 2 and 3 overview the syntax standard definitions and the operational basis for dealing with program functions and relations: states and streams, their specific definitions and properties. Section 4 offers a first series of basic results when analyzing the more restricted case of deterministic programs. Channel communication (not introducing non-determinism) and parallel composition are represented by distinct operators, all the language constructs being strict and monotonic. Within the predicative semantics, a recursive definition is interpreted in two semantically equivalent ways: by computational induction (as the least upper bound of functional iteration) and by fixed-point induction (as the least fixed- point of the respective functional). These definitions lead to rather distinct formulas of channel connections. The consistency theorem of the section establishes the equivalence by structural induction of the denotational and predicative semantics. It is essential to specify, in the Consistency Theorem context, the considered type of correctness: (1) partial correctness as specifying a superset of input-output behaviours of the program for producing a correct answer, if any; (2) robust correctness as specifying a subset of input-output behaviours of the program that gurantee the outcomes; (3) total correctness as describing the precise set of possible input-output behaviours of the program. Section 5 completes the results of the preceding section: the considered approach to non-determinism is to represent programs by sets of functions rather than by set-valued functions. This approach offers better solutions to the problems arising from the connection between non- determinism and recursion (e.g. choice distribution over recursion, least fixed-point definitions, types of correctness). Section 6 analyses the two semantics and their relationship for partial and robust correctness of (non-deterministic) programs. Section 7 outlines the program non- termination problems. Some of the authors' conclusions deserve to be reminded: (1) Fixed-point induction is best suited for robust correctness, while computational induction is best suited for partial correctness; (2) In the presence of recursion, the non-deterministic choice is better to be defined by sets of functions rather than by set- valued functions, for partial or total correctness; (3) In order to obtain the proper framework for reasoning about the programs which we deal with, it is necessary to carefully choose the framework parameters, since the denotational semantics aims at implementations, while the predicative semantics aims at proofs.