This simple module implements the directive coinductive/1 as described in "Co-Logic Programming: Extending Logic Programming with Coinduction" by Luke Simon et al. The idea behind coinduction is that a goal succeeds if it unifies to a parent goal. This enables some interesting programs, notably on infinite trees (cyclic terms).
:- use_module(library(coinduction)). :- coinductive p/1. p([1|T]) :- p(T).
This predicate is true for any cyclic list containing only 1-s, regardless of the cycle-length.
- The declaration :- coinductive name/arity, ... defines predicates as coinductive. The predicate definition is wrapped such that goals unify with their ancestors. This directive must precede all clauses of the predicate.