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 ProgramsSusumu YAMASAKI  Publication IEICE TRANSACTIONS on Information and Systems   Vol.E79-D   No.6   pp.840-854Publication Date: 1996/06/25Online ISSN:  DOI: Print ISSN: 0916-8532Type of Manuscript: PAPERCategory: Software TheoryKeyword: logic program,  fixpoint theory,  narrowing,  semantics,  domain theory,  Full Text: PDF>> Buy this Article Summary:  There have been semantics for logic programs as sets of definite clauses over sequence domains in [2],[6]. The sequence of substitutions caused by resolutions for logic programs can be captured by a fixpoint of a functional [3],[16]. In [15], 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[16]. 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 [18], 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 [7], and [11]. 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.