module rels.

% The following compute the reflective, symmetric, and transitive
% closures of binary relations.

type reflective, symmetric, transitive  (A -> A -> o) -> A -> A -> o.

reflective R X Y :- X = Y; R X Y.

symmetric R X Y :- R X Y ; R Y X.

transitive R X Y :- R X Y.
transitive R X Z :- R X Y, transitive R Y Z.

% The following compute various relations on binary relations.

type union          (A -> B -> o) -> (A -> B -> o) -> A -> B -> o.
type compose        (A -> B -> o) -> (B -> C -> o) -> A -> C -> o.
type iter           (A -> B -> B -> o) -> list A -> B -> B -> o.
type pre_post       (A -> o) -> (A -> B -> o) -> (B -> o) -> o.

union R S X Y   :- R X Y; S X Y.

compose R S X Y :- R X Z, S Z Y.

iter P nil    X X.
iter P (Z::L) X Y :- P Z X M, iter P L M Y.

pre_post R S T :- R X, S X Y, T Y.