%
/*
    rel_x.pro
    Tema: Relaciones
    Clase: Teoría Computacional, Matemáticas Discretas
    Alberto Pacheco, apacheco@itch.edu.mx, Nov'98, Ago'99, Oct'00
    Amzi! 16-bit Logic Explorer Prolog 3.3
    Versión generalizada con archivo separado para definición de relaciones

    PROPIEDADES:
    reflexiva(R), irreflexiva(NR),
    simetrica(S), asimetrica(NS), antisimetrica(AS),
    transitiva(T).

    INSTRUCCIONES:
    % Consulte 'relx.pro' y ejecute:
    ?- main.
    % Espeficique archivo-de-datos: rel_d1 ó rel_d2 ó rel_d3
*/

%-- UTILERIAS
xry(R,X,Y) :- rel(R,X,Y), X\=Y.
xrx(R,X,X) :- rel(R,X,X).
rel(R,X,Y) :- mk_rel(R,X,Y,T), T.
not_rel(R,X,Y) :- mk_rel(R,X,Y,T), not(T).
mk_rel(R,X,Y,T) :- functor(T,R,2), arg(1,T,X), arg(2,T,Y).

/*
    Glosario:
    si -->  'si y solo si'
    #  -->  x#A : x 'pertenece a' conjunto A
    <= -->  X<=Y : conjunto X 'es un subconjunto' de Y
    /\ -->  Intersección de conjuntos
    \/ -->  Unión de conjuntos
    0  -->  Conjunto vacío
    S  -->  Universo de discurso, R <= SxS
    E  -->  Relación de equivalencia = {  # R | x # S }
*/

%-- (R) R es reflexiva si para toda x#S, existe xRx
%--     R es reflexiva si E<=R
reflexiva(R) :- % false
    rel(R,X,_),
    not_rel(R,X,X),
    !, fail.
reflexiva(R) :- % false
    rel(R,_,X),
    not_rel(R,X,X),
    !, fail.
reflexiva(_). % true

%-- (NR) R es anti/irreflexiva si para toda x#S, no existe xRx
%--      R /\ E = 0
irreflexiva(R) :-
    xrx(R,X,X),
    !, fail.
irreflexiva(_).

%-- (S) R es simetrica, si para cada xRy existe yRx (xRx inclusive)
simetrica(R) :-
    rel(R,X,Y), % con xRx
    not_rel(R,Y,X),
    !, fail.
simetrica(_).

%-- (NS) R es asimetrica, si para cada xRy no existe yRx, ni xRx
asimetrica(R) :-
    xry(R,X,Y),
    rel(R,Y,X),
    !, fail.
asimetrica(R) :-
    xrx(R,X,X),
    !, fail.
asimetrica(_).

%-- (AS) R es antisimetrica, si para cada xRy no existe yRx, pero si xRx
antisimetrica(R) :-
    xry(R,X,Y),
    rel(R,Y,X),
    !, fail.
antisimetrica(R) :-
    not_rel(R,X,X),
    !, fail.
antisimetrica(_).

%-- (T) R es transitiva si siempre que se tiene xRy y yRz existe xRz (sin xRx)
transitiva(R) :-
    xry(R,X,Y), xry(R,Y,Z), % sin xRx
    not_rel(R,X,Z),
    !, fail.
transitiva(R) :- % sin xRx
    xry(R,X,Y),
    xry(R,Y,Z),
    rel(R,X,Z).

%-- LISTA DE PROPIEDADES A VERIFICAR
prop(reflexiva,'(R) ').
prop(irreflexiva,'(NR) ').
prop(simetrica,'(S) ').
prop(asimetrica,'(NS) ').
prop(antisimetrica,'(AS) ').
prop(transitiva,'(T) ').

test(R) :- !, prop(P,A), run(R,P,A), fail. % TODAS LAS PROPIEDADES PARA RELACION R
test(_).

run(R,P,A) :- functor(T,P,1), arg(1,T,R), T, !, write(A), write(P), nl.

pr(R) :- % Oct'00
	mk_rel(R,X,Y,T), findall([X,Y],rel(R,X,Y),L), 
	write(R), write('='), write(L), nl.


%-- rel_d3 style utilities (Oct'00)

mk_set(R,X) :-
    functor(T,R,1),
    arg(1,T,X),
    not(T),
    try_rule(R,X),
    assertz(T). % , write(T), write(' ').
mk_set(_,_).

try_rule(R,X) :- % Oct'00
    clause(rule(R,X),_), !, rule(R,X).
try_rule(_,_).

new_set(ID,Actual,Final) :-
    Actual =< Final,
    mk_set(ID,Actual),
    Nvo is Actual + 1,
    new_set(ID,Nvo,Final).
new_set(ID,_,_):-
    functor(T,ID,1), arg(1,T,X), 
    findall(X,T,L), write(ID), write('='), write(L), nl.

% rule(ID,Acutal) can be defined by user, eg. "x es par"


%-- PROGRAMA PPAL

main :- % TODAS LAS RELACIONES/PROPIEDADES
    write('** Propiedades de Relaciones **'), nl, nl, % Oct'00
    write('Anote nombre del programa (sin extensión): '), % Oct'00
    read_string(S), % Oct'00
    reconsult(S), % <- Oct'00 -> consult(rel_d3), % d,d0,d1,d2,d3,d4
    init,
    !,
      data(R),
      pr(R), % <- Oct'00 -> listing(R),
      test(R),
    fail.
main.

%