No CrossRef data available.
A general framework for lazy functional logic programming with algebraic polymorphic types
Published online by Cambridge University Press: 16 May 2001
Abstract
We propose a general framework for first-order functional logic programming, supporting lazy functions, non-determinism and polymorphic datatypes whose data constructors obey a set [Cscr ] of equational axioms. On top of a given [Cscr ], we specify a program as a set [Rscr ] of [Cscr ]-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 [Cscr ]-based rewriting calculi and a notion of model. We get soundness and completeness for [Cscr ]-based rewriting w.r.t. models, existence of free models for all programs, and type preservation results. As operational semantics, we develop a sound and complete procedure for goal solving, which is based on the combination of lazy narrowing with unification modulo [Cscr ]. Our framework is quite expressive for many purposes, such as solving action and change problems, or realizing the GAMMA computation model.
- Type
- Regular paper
- Information
- Copyright
- © 2001 Cambridge University Press