🚀 go-pugleaf

In article <9102181728.AA03502@ucbvax.Berkeley.EDU> ludemann@mlpvm1.iinus1.ibm.com writes:
>
>It's easy to print out "infinite" data structures in Prolog.
>Here are some examples (these are from IBM-Prolog; I think that
>Prolog-II and Prolog-III do something similar).  I've used the
>mode where the goal is printed out both before and after execution:
>     <-X = f(X) .
>      goal : <- V1 = f(V1) .
>      0ms success
>      <- f(@(1)) = f(f(@(1))) .
>     <- X = f(g(X)) .
>      goal : <- V1 = f(g(V1)) .
>      0ms success
>      <- f(g(@(2))) = f(g(f(g(@(2))))) .
>     <- X = f(f(X)) .
>      goal : <- V1 = f(f(V1)) .
>      0ms success
>      <- f(f(@(2))) = f(f(f(f(@(2))))) .
>
>Even though I seldom use them, it's nice to know that I can
>use circular graphs if I want and that my Prolog won't go into
>an infinite loop while unifying them or printing them (by the
>way, the overhead of handling circular structures is almost nil).
>
>If we can think of fixed-points of recursive programs, I see
>no reason why we can't also think of fixed-points of circular
>data structures.
>

I totally agree with what ludemann stated above. In a paper "Logic 
Programming with Recurrence Domains" which we submitted to ICALP 91, we
proposed a term schemata to explicitly encode certain recursive datatypes.
Here is the abstract of our paper:

   In this paper we present a formalism for finitely representing infinite
   set of terms. This formalism, called {\em $\omega$-terms}, enables us to
   reason finitely about certain recursive types. We present an extension of
   Horn logic programs, called $\omega$-Prolog, which allows a finite 
   schematization of infinitely many clauses via predicates with 
   $\omega$-terms as arguments. We show that for every $\omega$-Prolog
   program there is an equivalent Horn logic program. That is, incorporating 
   $\omega$-terms into first order logic programming does not change its
   denotational semantics.
   Computationally, however, $\omega$-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 $\omega$-terms play a similar role as regular-trees [MiR~85] and
   sort-expressions [Com~90] 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^n, b^n, c^n): n \in \cN\}$.
   We present a finite and complete algorithm for unification between
   $\omega$-terms, with which we can also compute the intersection of the 
   languages defined by $\omega$-terms. 

The following is an example to show the operational difference of
\omega-Prolog and Prolog:

Let  a^n  denote  the concatenation of n a's and * denote the concatenation 
operator. The following are three programs which differ from each other only
on their last facts. Each program is associated with a query.

	         (1) p(x) :- r(x, y, z), q(z).  
	         (2) r(a, b, c). 
	         (3) r(a* x, b* y, c* z) :- r(x, y,z). 
  (4) q(c^{20}).       (4') q(d).               (4'') q(x). 

  (G) :- p(x).         (G') :-p(x).             (G'') :- setof(p(x), p(x), S).

In the first program the query p(x) requires 20 backtracking steps through
clause (2) in order to get p(a^{20}). In the second example 
the  query p(x) does not terminate due to the infinite backtracking
through r(x,y,z), and since none of the bindings for z of r(x,y,z) satisfies 
q(d). The third example computes the fixpoints of p(x). It does not terminate
since there are infinitely many bindings x <- a,  x <-  a^2, x <- a^3, ..., 
such that p(x) is true.

In our paper, we encode the denotation of predicate r by a term schemata

   r(H(a*_, N, a), H(b*_, N, b),  H(c*_, N, c)) where

H is a special functor whose first argument denotes recurring patterns and 
N is a special variable served as both counter and synchronizer. 

After such encoding, the 
 the first query returns       x <-a20, N <- 20
 the second query returns      fail
 the third query returns       x <- H(a*_, N, a)

Although our intention is to use such term schemata to represent an infinite
set of FINITE terms, we think that the term schemata can be straightforwardly
extended to denote fixed-points of circular data structures. Thus 

One can think that unifying  X = f(g(X)) returns  X <- H(f(g(_)), N, X).

If you are interested in the paper, you can direct your request to

hongch@sbcs.sunysb.edu or

or 

Hong Chen
Department of Computer Science
State Univ of New York
Stony Brook, NY 11794