EXPRESSIBILITY OF THE SEMANTICS OF SEQUENTIAL PROGRAMS IN FIRST-ORDER LOGIC

Article type: Research Article

Authors: Hungar, Hardi

Affiliations: Department of Computer Science, University Oldenburg, D-26111 Oldenburg, Germany, [email protected]

Abstract: The notion of an expressive interpretation was originally introduced by Cook in order to formulate completeness results for Hoare-style proof systems. An interpretation is called expressive for a programming language if the input/output relation of every program can be expressed by a first-order formula. Various necessary or sufficient conditions for an interpretation to be expressive are known. In this paper a characterization is given which improves on these results. It holds for a wide spectrum of programming languages. An interpretation is expressive iff it is either 1. uniformly locally finite or 2. weakly arithmetic and it has evaluation predicates (which return the truth value of a boolean expression, given its gödel number and the values of its free variables). Besides this characterization, it is investigated which first-order signatures allow nontrivial (i.e. non uniformly locally finite) expressive interpretations. Signatures which have (besides constants) only one unary function symbol and only unary relation symbols, have only trivial expressive interpretations. All other signatures allow nontrivial expressive interpretations as well.

DOI: 10.3233/FI-1994-2145

Journal: Fundamenta Informaticae, vol. 21, no. 4, pp. 345-365, 1994