% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
%                                                                           %
% File:            sets.dtr                                                 %
% Purpose:         define set operators                                     %
% Author:          Lionel Moser, December, 1991                             %
% Email:           moser@bnr.ca                                             %
% Documentation:   Cognitive Science Research Paper CSRP 216, Univ. Sussex  %
% Related files:   arglogic.dtr, arglists.dtr, clogic.dtr, sets.dtr         %
% Version:         6.01                                                     %
%                                                                           %
%      Copyright (c) University of Sussex 1991.  All rights reserved.       %
%                                                                           %
% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

# load 'clogic.dtr'.

% Moser, Lionel, "Lexical constraints in DATR," Cognitive Science
%   Research Paper CSRP 216, University of Sussex, Brighton,
%   1992.
% 
%   DATR contains no special features to support testing of
%   equality, negation, disjunction, or multiple inheritance.
%   Nevertheless, given an appropriate interpretation it is
%   possible, within DATR's existing syntax and semantics, to
%   represent these operations.  In this paper we review the
%   technique known as `negative path extension', and show how
%   it can be used to reconstruct negation, disjunction, and
%   equality testing.  We then show how these operations can be
%   used to define what are essentially meta-level constraints
%   on DATR lexical derivation.

# vars $terminal1 $terminal2:  1 2 3 4 5 6 7 8 9 0.

% Member:<atom ; list_of_atoms ;> ==
%       true    -   if item is in list,
%       false   -   if atom is not in list.
%

% Member:<<val> ; <list> ;>

Member:
    <$terminal1 ; $terminal1> == true
    <$terminal1 ; ;> == false
    <$terminal1 ; > == <reduce $terminal1 ;>
    <reduce $terminal1 ; $terminal2> == <$terminal1 ;>.

% Some theorems:
%
% Member:
%   <1 ; ;> = false
%   <1 ; 1 2 3 ;> = true
%   <1 ; 2 3 ;> = false
%   <1 ; 2 1 3 ;> = true
%   <1 ; 2 3 1 ;> = true

% Subset takes a cross-product of $terminal1, so requires $terminal2
% to be defined identically to $terminal1.
%
% Subset:< X0 X1 X2 ... Xn ; Y0 Y1 Y2 ... Ym ;> ==
%          true    - if every Xi is in Y
%          false    - otherwise

Subset:
    <;> == true
    <$terminal1 ;> == Member
    <$terminal1 $terminal2> == And:<Member:<$terminal1 ; Arg2 ;>
                                    Subset:<$terminal2> ;>.

% Some theorems:
%
% Subset:
%   <; ;> = true
%   <; 1 2 3 2 ;> = true
%   <1 ; 1 2 3 2 ;> = true
%   <1 ; 2 3 2 2 ;> = false
%   <2 1 ; 2 3 2 2 ;> = false
%   <2 1 3 ; 2 3 2 2 1 ;> = true.

% Union:<X0 X1 ... Xn ; Y0 Y1 ... Ym ;> == X U Y
% We define X U Y as Y + (Y - X)

X2: <> == Arg1.
Y2: <> == Arg2.

Union:
    <;> == Y2
    <$terminal1> == <If:<Member:<$terminal1 ; Y2 ; !> > $terminal1>
    <then $terminal1> == Union:<>
    <else $terminal1> == Union:<X2:<> ; Y2:<> $terminal1 ; !>.

% Some theorems:
%
% Union:
%   <1 2 3 ; 1 2 3 ;> = 1 2 3
%   <; 1 2 3 ;> = 1 2 3
%   <1 2 3 ; 2 3 ;> = 2 3 1
%   <1 2 3 4 5 ; ;> = 1 2 3 4 5
%   <1 3 5 ; 2 4 6 ;> = 2 4 6 1 3 5
%   <; ;> = .

% Intersection:<X0 X1 ... Xn ; Y0 Y1 ... Ym ; ;> == XiY  % initial call
% Intersection:<X0 X1 ... Xn ; Y0 Y1 ... Ym ; XiY ;>     % recursive call

X1: <> == Arg1.
Y1: <> == Arg2.
XiY:<> == Arg3.   % X intersection Y

Intersection:
    <;> == XiY
    <$terminal1> == <If:<Member:<$terminal1 ; Y1 ; !> > $terminal1>
    <then $terminal1> == Intersection:< X1:<> ; Y1:<> ; XiY:<> $terminal1 ; !>
    <else $terminal1> == Intersection:<>.

% Some theorems:
%
% Intersection:
%   <1 2 3 ; 1 2 3 ; ;> = 1 2 3
%   <; 1 2 3 ; ;> = 
%   <1 2 3 ; 2 3 ; ;> = 2 3
%   <1 2 3 4 5 ; ; ;> = 
%   <1 3 5 ; 2 4 6 ; ;> = 
%   <1 3 5 ; 2 4 3 6 ; ;> = 3.

% Setequal:<Set1 ; Set2 ; !> ==
%     true  - if Set1 and Set2 are the same
%     false - otherwise

Setequal:
    <> == <If:<Subset>>                         % Set1 <= Set2?
    <then> == Subset:<Arg2:<> ; Arg1:<> ; !>    % Set2 <= Set1?
    <else> == false.

% Some theorems:
%
% Setequal:
%   <; ;> = true
%   <1 ; 1 ;> = true
%   <1 2 ; 1 2 ;> = true
%   <3 2 ; 2 3 ;> = true
%   <1 2 3 4 5 ; 5 4 3 2 1 ;> = true.

% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

# show
    <1 2 3 4 5 ; 5 4 3 2 1 ;> 
    <1 2 3 4 5 ; ; ;> 
    <1 2 3 4 5 ; ;> 
    <1 2 3 ; 1 2 3 ; ;> 
    <1 2 3 ; 1 2 3 ;> 
    <1 2 3 ; 2 3 ; ;> 
    <1 2 3 ; 2 3 ;> 
    <1 2 ; 1 2 ;> 
    <1 3 5 ; 2 4 3 6 ; ;> 
    <1 3 5 ; 2 4 6 ; ;> 
    <1 3 5 ; 2 4 6 ;> 
    <1 ; 1 2 3 2 ;> 
    <1 ; 1 2 3 ;> 
    <1 ; 1 ;> 
    <1 ; 2 1 3 ;> 
    <1 ; 2 3 1 ;> 
    <1 ; 2 3 2 2 ;> 
    <1 ; 2 3 ;> 
    <1 ; ;>
    <2 1 3 ; 2 3 2 2 1 ;> 
    <2 1 ; 2 3 2 2 ;> 
    <3 2 ; 2 3 ;> 
    <; 1 2 3 2 ;> 
    <; 1 2 3 ; ;> 
    <; 1 2 3 ;> 
    <; ;>.

% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

% The next line is the Revision Control System Archive Id: do not delete it.
% $Id: archive.dtr,v 1.1 1997/04/09 20:40:33 root Exp $