% file:     set_utils.pl
% date:     February 16, 2005
% author:   Douglas M. Auclair (DMA)
% synopsis: Provides the axioms of the Zermelo-Fraenkel Set theory
%           (ZF) for finite, ground sets.

:- module(set_utils, [
	set/1,
        union/3,
	intersection/3,
	difference/3,
	disjunction/3,
	separate/4,
	replace/4,
	power_set/2,
	subset/2,

        ':='/2, '=:'/2, '<~'/2, c/2,
        s/2, zero/1
]).

:- op(200, xfy, n).
:- op(200, xfy, u).
:- op(200, xfy, v).
:- op(200, xfy, c).
:- op(200, xfy, <~).
:- op(200, xfx, ..).
:- op(701, xfy, :=).
:- op(701, yfx,  =:).

% modified: February 16, 2005, DMA
% changed:  setof to findall to keep the In variable free on the
%           outside of the (temporary) binding scope.  Activated the
%           power set predicate.

% modified: February 17, 2005, DMA
% changed:  Added the set function evaluator, which allowed me, with
%           very little fuss, to add the Peano series operators.
%           Yikes!  The set representation of the Peano series!  Fancy
%           that, Hedda!  Also added subset/2, a nondeterministic
%           version of power_set/2 (returning each subset (sometimes
%           more than once .. oh, well!) one subset at a time).  Added
%           the '..'/2 operator to expand the term 1..10 to the first
%           ten numbers (starting at 1, BTW). 1..N is set-syntactic
%           sugar for the Peano number N (some people just prefer
%           looking at Arabic numerals better than the set
%           representation for some reason ...).

% modified: February 18, 2005, DMA
% changed:  Changed subset so that it does the subset check first (and
%           better) if both the set and subset are ground, only if
%           subset is a var does it attempt to generate a subset
%           result from the set.

% modified: March 24, 2005, DMA
% changed:  Converted all functional arguments to be phi-term
%           equivalents, using library(combinators) to handle the
%           conversions and functional composition.

:- use_module(library(list_utils), [
        prepend/3,
	takeout/3,
	permute/2,
	unfold/5
]).
:- use_module(library(list_utils), [map_reversed/4]).
:- use_module(library(syntax), ['<-'/2, '~'/1, '=>'/2, '<=>'/2,
	                        sinon/2, try/3]).

:- op(200,  yfx, <-).
:- op(200,   fx, try).
:- op(900,   fy, ~).
:- op(920,  xfy,  =>).
:- op(920,  xfy, <=>).
:- op(1100, xfy, sinon).

:- ensure_loaded(library(lists)).

% ----------------------------------------------------------------------
% Set "arithmetic"

% Functional activation, X := Fn, in the family of 'is'/2.  We explode
% the 'function', then, call it with X as the out parameter, so Fn, in
% the ':='/2 form is written S := X n Y, but it reduces, through term
% rewriting, to n(S, X, Y) where S is the out parameter.  Note that S,
% the out parameter, is the FIRST argument, just because I hate
% append, principally.

X := Fn :-
  Fn =.. [Functor|Args],
  evaluate_arguments(Args, [], Sets),
  Predicate =.. [Functor|[X|Sets]],
  Predicate.

Fn =: X :- X := Fn.
%    The evaluation goes in the opposite direction ... HA! Do that in
%    Pascal!  An the structure of this predicate is oh-so-symmetrical!

% ... with the above, we can do the following:
s([[]], []).
s([[Prior|DownTo0], Prior|DownTo0], [Prior|DownTo0]).
zero([]).
% oh, my!

X <~ Set :- takeout_equivalent_member(X, Set, _).
%    For sets, [1,2] <~ [[2,1]|Whatever] works.

intersection(L1, L2, Ans) :-
%    Gives the members that are common to all the sets
  separate(psi(X, set_utils:(X <~ L2)), L1, [], Ans).

union(Set1, Set2, Ans) :-
%    Gives a new set that all the (unique, of course) members of both
%    sets.
  separate(complement(X, set_utils:(X <~ Set2)), Set1, [], UniqueSet1s),
  append(UniqueSet1s, Set2, Ans).

% set difference Set0 - SubSet1 =: SubSet2

difference(Set, [], Set).
difference(Set, [H|T], Ans) :-
  takeout_equivalent_member(H, Set, Subset),
  difference(Subset, T, Ans).

disjunction(Set1, Set2, Ans) :-
%    Disjoint := A u B - A n B, the uncommon members ... put another
%    way, disjunction is the opposite of intersection, given the
%    universe := A u B.
  separate(complement(X, set_utils:(X <~ Set2)), Set1, [], UniqueSet1s),
  separate(complement(X, set_utils:(X <~ Set1)), Set2, UniqueSet1s, Ans).

% The Separation Schema: keeps only the members that meet Predicate
% (Predicate is of the structure predicate(X, Test) where Test uses X)
separate(Predicate, Set) --> map_reversed(Predicate, Set).

% The Replacement Schema: transforms the members of a set into new
% members (Out) of the new set by applying the BinaryTest (a predicate
% with an out argument, Out) to each of the original members (In).
% BinaryTest uses both In and Out in its clause body.
replace(Fn, List) --> map_reversed(Fn, List).

% set/1 tests to see if this is a set: all members are unique.

set([]).
set([S|Et]) :- list_utils:takeout(X, [S|Et], Z) => ~ set_utils:(X <~ Z).

power_set(List, AllSubsets) :-
%    given the set S = [a,b], P(S) = [[a,b], [a], [b], []]
  setof(Perm, permute(List, Perm), Perms),
  replace(phi(L0, L1, list_utils:unfold(psi(X, X = []), i,
				        lambda([_|T], T), L0, L1)),
          Perms, [], Bag),

  % now that we have a list of lists of lists, let's generalize those
  % members to the outermost list, adding them only if they haven't
  % shown up already
  reduce_to_set_of_sets(Bag, [[]], AllSubsets).

subset(Subset, Set) :-
%    Sees if Subset is Set or a part of set.
  subset_both_ground(Subset, Set) ->
    test_subset(Subset, Set)
  ;
    generate_subset(Subset, Set).

Subset c Set :- subset(Subset, Set).
%    The set notation operator for subset.

% ----------------------------------------------------------------------
% SET OPERATORS

p(Powerset, Set) :- power_set(Set, Powerset).
n(Intersection, X, Y) :- intersection(X, Y, Intersection).
u(Union, X, Y) :- union(X, Y, Union).
'-'(Difference, X, Y) :- difference(X, Y, Difference).
v(Disjunction, X, Y) :- disjunction(X, Y, Disjunction).

% ... and one perl one ...
'..'(Count, X, Y) :- unfold(psi(A, A > Y), i, "`+1", X, Count).

% ----------------------------------------------------------------------
% INTERNAL IMPLEMENTATION PREDICATES

% subset_both_ground/2 sees if both Subset and Set are ground sets.

subset_both_ground(A, B) :- is_list(A), is_list(B).

test_subset(Subset, Set) :-
%    Sees if Subset is a subset of the Set.
  set_utils:(X <~ Subset) => set_utils:(X <~ Set).

% generate_subset/2 constructs a subset from the given set

generate_subset(Set, Set).
%    the base case is the subset IS the set.

generate_subset(Subset, Set) :-
%    otherwise we make a subset by removing some of its members
  takeout(_, Set, Sset),
  generate_subset(Subset, Sset).

% evaluate_arguments converts any set functions to their resulting,
% normalized, sets.

evaluate_arguments([]) --> reverse.
%    order of arguments is important for, e.g., set-difference.
evaluate_arguments([Set|Sets]) -->
  evaluate(Set),
  evaluate_arguments(Sets).

evaluate(Arg) -->
%    If Arg is a set, put it back on the arg-list, otherwise evaluate
%    it first.
  { (is_list(Arg); number(Arg)) -> Set = Arg; Set := Arg },
  prepend(Set).

% reduce_to_set_of_sets/3 is not necessary to ZF, by any stretch, but
% it is useful defining the power set.

reduce_to_set_of_sets([]) --> [].
reduce_to_set_of_sets([Set|Sets]) -->
  prepend_set_elements(Set),
  reduce_to_set_of_sets(Sets).

prepend_set_elements([]) --> [].
prepend_set_elements([H|T], In, Out) :-
  (Set <- In, (X <- Set <=> X <- H) -> NewIn = In; NewIn = [H|In]),
  prepend_set_elements(T, NewIn, Out).

takeout_equivalent_member(X, Set, Subset) :-
%    For sets [1,2,3] == [3,1,2] so we need to weaken takeout/3 to
%    work with set equivalence
  (is_list(X) ->
     separate(predicate(L, syntax:(S <- L <=> S <- X)), Set, [], [TO|_])
   ;
     TO = X),
  takeout(TO, Set, Subset).