For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Sequence Domains and Fixpoint Semantics for Logic Programs
IEICE TRANSACTIONS on Information and Systems
Publication Date: 1996/06/25
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Software Theory
logic program, fixpoint theory, narrowing, semantics, domain theory,
Full Text: PDF>>
There have been semantics for logic programs as sets of definite clauses over sequence domains in ,. The sequence of substitutions caused by resolutions for logic programs can be captured by a fixpoint of a functional ,. In , a functional is regarded as a behaviour of a dataflow network, the semantics over sequence domains induces dataflow computing for logic programs. Also it may provide a transformation of logic programs to functional programs. Motivated by dataflow computing constructions for logic programming, this paper deals with fixpoint semantics over sequence domains for logic programs with equations and negations. A transformation, representing deductions caused by resolutions and narrowings, is associated with a logic program with equations, modified from the operator in , so that it may be represented by a continuous functional over a sequence domain, and its least fixpoint is well-defined. An explicit construction of such a continuous functional of sequence variables is necessary for dataflow computing, and we should prove that the functional of sequence variables can exactly represent the transformation concerned with sets. For a general logic program, a functional is constructed over a sequence domain so that it may reflect a consistency-preserving renewal function for the pair of atom sets on the basis of the 3-valued logic approach as in , and . It is a problem to construct the domain for the functional representing a generation of atom sets interpreted as true and negation as failure in the generation, for general logic programs. The functional is monotonic over a complete partial order and its least fixpoint is well-defined, although the least fixpoint is not always obtained by the limit of finite computing, because of the functional being not necessarily continuous.