Abstract
This is an attempt at a direct semantic formalization of first-order relational-functional languages (the characteristic RELFUN subset) in terms of a generalized model concept. Function-defining conditional equations (or, footed clauses) and active call-by-value expressions (in clause premises) are integrated into first-order theories. Herbrand models are accomodated to relational-functional programs by not only containing ground atoms but also ground molecules, i.e. specific function applications paired with values. Extending SLD-resolution toward innermost conditional narrowing of relational-functional clauses, SLV-resolution is introduced, which, e.g., flattens active expressions. The T p -operator is generalized analogously, e.g. by unnesting ground-clause premises. Soundness and completeness proofs for SLV-resolution naturally extend the corresponding results in logic programming.
Preview
Unable to display preview. Download preview PDF.
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
(1999). A direct semantic characterization of RELFUN. In: A Tight, Practical Integration of Relations and Functions. Lecture Notes in Computer Science, vol 1712. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0103294
Download citation
DOI: https://doi.org/10.1007/BFb0103294
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66644-8
Online ISBN: 978-3-540-48064-8
eBook Packages: Springer Book Archive