A Semantic Framework for Functional Logic Programming with Algebraic Polymorphic Types

We propose a formal framework for functional logic programming, supporting lazy functions, non-determinism and polymorphic datatypes whose data constructors obey a given set C of equational axioms. On top of a given C, we specify a program as a set R of C-based conditional rewriting rules for defined functions. We argue that equational logic does not supply the proper semantics for such programs. Therefore, we present an alternative logic which includes C-based rewriting calculi and a notion of model. We get soundness and completeness for C-based rewriting w.r.t. models, existence of free models for all programs, and type preservation results.