Denotational Versus Declarative Semantics for Functional Programming

Denotational semantics is the usual mathematical semantics for functional programming languages. It is higher order (H.O.) in the sense that the semantic domain D includes [D → D] as a subdomain. On the other hand, the usual declarative semantics for logic programs is first order (F.O.) and given by the least Herbrand model. In this paper, we take a restricted kind of H.O. conditional rewriting systems as computational paradigm for functional programming. For these systems, we define both H.O. denotational and F.O. declarative semantics as two particular instances of algebraic semantics over continuous applicative algebras. For the declarative semantics, we prove soundness and completeness of rewriting, as well as an initiality result. We show that both soundness and completeness fail w.r.t. the denotational semantics and we present a natural restriction of rewriting that avoids unsoundness. We conjecture that this restricted rewriting is complete for computing denotation ally valid F.O. results.