id: 00176722
dt: a
an: 00176722
au: Chen, Hong; Hsiang, Jieh
ti: Logic programming with recurrence domains.
so: Automata, languages and programming, Proc. 18th Int. Colloq., Madrid/Spain
    1991, Lect. Notes Comput. Sci. 510, 20-34 (1991).
py: 1991
pu: Berlin etc.: Springer-Verlag
la: EN
cc: 
ut: infinite sets of terms; extension of Horn logic programs; non-regular- tree
    languages; unification
ci: Zbl 0753.00027
li: 
ab: Summary: [For the entire collection see Zbl 0753.00027.] We present a
    formalism for finitely representing infinite sets of terms. This
    formalism, called $ω$-terms, enables us to reason finitely about
    certain recursive types. We present an extension of Horn logic
    programs, called $ω$-Prolog, which allows a finite schematization of
    infinitely many clauses via predicates with $ω$-terms as arguments. We
    show that for every $ω$-Prolog program there is an equivalent Horn
    logic program. That is, incorporating $ω$-terms into first order logic
    programming does not change its denotational semantics.
    Computationally, however, $ω$-Prolog has the advantages of (1)
    representing infinitely many answers finitely, (2) avoiding repetition
    in computation and thus achieving better efficiency, (3) allowing
    infinite queries, and (4) avoiding certain non-termination of Prolog
    programs. The $ω$-terms play a similar role as regular-trees and
    sort-expressions in explicitly defining abstract data types. It differs
    from the others in that it allows us to define certain non-regular-tree
    languages such as $\{(a\sp n,b\sp n,c\sp n)$: $n\in{\cal N}\}$. We
    present a finite and complete algorithm for unification between
    $ω$-terms, with which we can also compute the intersection of the
    languages defined by $ω$- terms.
rv: