coinduction.pl -- Co-Logic Programming

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.

See also

- "Co-Logic Programming: Extending Logic Programming with Coinduction" by Luke Simon et al.

bug

- Programs mixing normal predicates and coinductive predicates must be stratified. The theory does not apply to normal Prolog calling coinductive predicates, calling normal Prolog predicates, etc.

Stratification is not checked or enforced in any other way and thus left as a responsibility to the user.

 coinductive(:Spec)

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.