reduce-historical/r37/packages/redlog/clbnf.red

% ----------------------------------------------------------------------
% $Id: clbnf.red,v 1.8 1999/04/13 13:10:55 sturm Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm
% ----------------------------------------------------------------------
% $Log: clbnf.red,v $
% Revision 1.8  1999/04/13 13:10:55  sturm
% Updated comments for exported procedures.
%
% Revision 1.7  1999/04/01 11:26:47  dolzmann
% Reformatted one procedure.
%
% Revision 1.6  1999/03/22 17:07:12  dolzmann
% Changed copyright information.
% Reformatted comments.
%
% Revision 1.5  1999/03/21 13:34:06  dolzmann
% Corrected comments.
%
% Revision 1.4  1996/10/07 11:45:47  sturm
% Added fluids for CVS and copyright information.
%
% Revision 1.3  1996/07/13 10:53:07  dolzmann
% Added black box implementations cl_bnfsimpl, cl_sacatlp, and cl_sacat.
%
% Revision 1.2  1996/07/07 14:34:19  sturm
% Turned some cl calls into service calls.
%
% Revision 1.1  1996/03/22 10:31:27  sturm
% Moved and split.
%
% ----------------------------------------------------------------------
lisp <<
   fluid '(cl_bnf_rcsid!* cl_bnf_copyright!*);
   cl_bnf_rcsid!* := "$Id: clbnf.red,v 1.8 1999/04/13 13:10:55 sturm Exp $";
   cl_bnf_copyright!* := "(c) 1995-1996 by A. Dolzmann and T. Sturm"
>>;

module clbnf;
% Common logic boolean normal forms. Submodule of [cl]. This module
% provides CNF and DNF computation.

%DS
% <SG-DNF> ::= <GOR> . <SGCL>
% <SGCL> ::= (<SGCONJ>,...)
% <SGCONJ> ::= <GAND> . <SATOTVL>
% <GOR> ::= ['or] | ['and]
% <GAND> ::= ['and] | ['or] "opposite to <GOR>"
% <SATOTVL> ::= (<TRUTH VALUE>) | (<ATOMIC FORMULA>, ...)

procedure cl_dnf(f);
   % Common logic disjunctive normal form. [f] is a formula. Returns a
   % DNF of [f].
   rl_simpl(cl_gdnf(f,'or),nil,-1);

procedure cl_cnf(f);
   % Common logic conjunctive normal form. [f] is a formula. Returns a
   % CNF of [f].
   rl_simpl(cl_gdnf(f,'and),nil,-1);

procedure cl_gdnf(f,gor);
   % Common logic generic disjunctive normal form. [f] is a formula;
   % [gor] is one of [and], [or]. Returns a G-DNF of [f].
   begin scalar strictgdnf,gdnf,svrlsiexpla;
      f := rl_simpl(rl_nnf f,nil,-1);
      svrlsiexpla := !*rlsiexpla;
      !*rlsiexpla := nil;
      (strictgdnf := cl_strict!-gdnf(f,gor)) where !*rlbnfsm=nil;
      if !*rlbnfsm then
	 strictgdnf := gor . cl_subsume(rl_argn strictgdnf,gor);
      !*rlsiexpla := svrlsiexpla;
      gdnf := cl_unstrict(strictgdnf,gor);
      return gdnf
   end;

procedure cl_strict!-gdnf(f,gor);
   % Common logic strict generic disjunctive normal form. [f] is a
   % formula; [gor] is one of [and], [or]. Returns a strict g-DNF,
   % i.e. a formula upto unary [and]'s and [or]'s, which is in g-DNF.
   begin scalar w;
      w := cl_mkstrict(rl_simpl(cl_strict!-gdnf1(f,gor),nil,-1),gor);
      return rl_bnfsimpl(w,gor)
   end;

procedure cl_subsume(gcl,gor);
   % Common logic subsume. [gcl] is a generic conjunction list; [gor]
   % is one of [and], [or]. Returns a generic conjunction list
   % equivalent to [gcl]. Performs simplification by subsumption.
   begin scalar w;
      if null gcl or null cdr gcl then return gcl;
      w := cl_subsume1(gcl,gor);
      if car w then <<
	 cddr w := cl_subsume(cddr w,gor);
	 return cdr w
      >>;
      return cl_subsume(cdr w,gor)
   end;

procedure cl_subsume1(gcl,gor);
   % Common logic subsume 1. [gcl] is a generic conjunction list;
   % [gor] is one of [and], [or]. A pair $(c,l)$ is returned, where
   % $c$ is [nil] or a list of atomic formulas and $l$ is a generic
   % conjunction list. [gcl] is modified. The subsumption relation
   % beween [car gcl] and all elements of [cdr gcl] is tested. If $c$
   % is nil, [car gcl] was suberflous. $l$ is the modified [gcl] in
   % which all superflous conjunctions are deleted. If $c$ is non-nil,
   % it is [car gcl] and [car gcl] cannot be dropped. If [cl_setrel]
   % is used this requires, that [!*rlsiso] and [!*rlidentify] are on.
   begin scalar a,w,x,scgcl,oscgcl;
      x := cdar gcl;
      oscgcl := gcl;
      scgcl := cdr gcl;
      while scgcl do <<
	 a := car scgcl; scgcl := cdr scgcl;
	 w := if !*rlbnfsm then
 	    rl_subsumption(x,cdr a,gor)
 	 else
 	    cl_setrel(x,cdr a,gor);
	 if w eq 'keep1 then
	    cdr oscgcl := scgcl
	 else if w eq 'keep2 then
	    x := scgcl := nil
	 else
	    oscgcl := cdr oscgcl
      >>;
      if null x then gcl := cdr gcl;
      return x . gcl
   end;

procedure cl_setrel(l1,l2,gor);
   % Common logic set relation. [l1] and [l2] are list of atomic
   % formulas. [gor] is one of [and], [or]. Returns [nil], [keep1], or
   % [keep2]. If [l1] is a subset of [l2] [keep1] is returned; if [l2]
   % is a subset of [l1] [keep2] is returned otherwise [nil] is
   % returned.
   begin scalar state,a1,hlp;
      while l1 and l2 and car l1 eq car l2 do <<
	 l1 := cdr l1;
	 l2 := cdr l2
      >>;
      if null (l1 and l2) then <<
      	 if null (l1 or l2) then return 'keep1;  % both equal.
       	 return l2 and 'keep1 or 'keep2
      >>;
      state := 'keep1;
      if rl_ordatp(car l1,car l2) then <<
	 hlp := l1; l1 := l2; l2 := hlp;
	 state := 'keep2
      >>;
      repeat <<
	 a1 := car l1; l1 := cdr l1;
	 l2 := memq(a1,l2);
	 if null l2 then a1 := l1 := nil
      >> until null l1;
      return a1 and state
   end;

procedure cl_strict!-gdnf1(f,gor);
   % Common logic disjunctive normal form in strict representation.
   % [f] is a formula containing no first-order operators but $\land$
   % and $\lor$; [gor] is one of ['and], ['or]. Returns a strict g-DNF
   % of [f], i.e. a g-disjunction of g-conjunctions of atomic formulas
   % including unary $\lor$ and $\land$ if necessary.
   begin scalar gand,op,subgdnfl,noop,noopgdnf;
      gand := if gor eq 'or then 'and else 'or;
      op := rl_op f;
      if op eq gor then
	 return rl_mkn(gor,for each subf in rl_argn(f) join
	    rl_argn(cl_strict!-gdnf(subf,gor)));
      if op eq gand then <<
	 subgdnfl := for each subf in rl_argn(f) collect
	    cl_strict!-gdnf(subf,gor);
	 % Switch to noop form.
	 noop := for each subf in subgdnfl collect
	    for each gconj in rl_argn subf collect rl_argn gconj;
	 % Computing the cartesian product of the conjunctive lists is
	 % now equivalent to an application of the law of
	 % distributivity, though the result is not flat yet.
	 noopgdnf := cl_bnf!-cartprod noop;
	 % Switch back to our normal representation.
	 return rl_mkn(gor,for each gconj in noopgdnf collect
	    rl_mkn(gand,for each x in gconj join append(x,nil)))
      >>;
      if rl_cxp op and not rl_tvalp op then
      	 rederr {"cl_strict!-gdnf: illegal operator",op,"in BNF computation"};
      return rl_mkn(gor,{rl_mkn(gand,{f})})
   end;

procedure cl_mkstrict(f,gor);
   % Common logic make strict. [f] is a g-DNF. Returns a strict g-DNF,
   % possibly including one truth value.
   begin scalar op,gand;
      gand := cl_flip gor;
      op := rl_op f;
      if not rl_cxp op or rl_tvalp op then
 	 return rl_mkn(gor,{rl_mkn(gand,{f})});
      if op eq gand then
 	 return rl_mkn(gor,{f});
      if op neq gor then
 	 rederr {"BUG IN cl_mkstrict"};
      return rl_mkn(gor,for each subf in rl_argn f collect
	 if rl_op subf eq gand then subf else rl_mkn(gand,{subf}))
   end;

procedure cl_unstrict(sgdnf,gor);
   % Common logic unstrict, [sdnf] is a sg-DNF; [gor] is one of [and],
   % [or]. Returns a g-DNF.
   rl_smkn(gor,for each conj in rl_argn sgdnf collect
      % A unary g-and does not have a cddr, ignore it.
      if cdr rl_argn conj then conj else car rl_argn conj);


procedure cl_bnf!-cartprod(s);
   % Common logic boolean normal form cartesian product. [s] is a list
   % $(s_1,...,s_n)$ of lists. Returns $s_1 \times ... \times s_n$ as
   % a list of $n$-element lists. The empty set and singletons are
   % their own cartesian product.
   if null s or null cdr s then s else cl_bnf!-cartprod1 s;

procedure cl_bnf!-cartprod1(s);
   % Common logic boolean normal form cartesian product. [s] is a list
   % $(s_1,...,s_n)$ of lists with $n \geq 2$. Returns $s_1 \times ...
   % \times s_n$ as a list of $n$-element lists.
   begin scalar w;
      if null cdr s then
      	 return for each m in car s collect {m};
      w := cl_bnf!-cartprod1 cdr s;
      return for each m in car s join
      	 for each y in w collect m . y
   end;

procedure cl_sac(sgdnf,gor);
   % Common logic subsumption and cut. [sgdnf] is a sg-DNF; [gor] is
   % one of [or], [and]. Returns a sg-DNF equivalent to [sgdnf]. This
   % procedures performs simplifications based on order theoretical
   % subsumption and cut. There are no possible applications of order
   % theoretical subsumption and cut between subformulas of the
   % returned sg-DNF.
   begin scalar w,gand;
      if rl_tvalp car rl_argn car rl_argn sgdnf then return sgdnf;
      gand := cl_flip(gor);
      % switch to noop form
      w := for each x in rl_argn sgdnf collect
	 rl_argn x;
      w := cl_applysac(w,gor);
      if w eq 'break then
	 return rl_mkn(gor,{rl_mkn(gand,{cl_cflip('true,gor eq 'or)})});
      w := for each x in w join
	 if x then
	    {rl_mkn(gand,x)}
	 else
	    nil;
      if null w then
	 return rl_mkn(gor,{rl_mkn(gand,{cl_cflip('true,gor eq 'or)})});
      return gor . w
   end;

procedure cl_applysac(l,gor);
   % Common logic apply subsumption and cut. [l] is a list of lists of
   % atomic formulas; [gor] is one of [or], [and]. Returns ['break] or
   % a list $k$ of list of atomic formulas. If ['break] is returned
   % [l] is as a g-DNF equivalent to ['true] in case of ['gor eq 'or]
   % and equivalent to ['false] in case ['gor eq 'and]. The lists are
   % considered as generic disjunctive normal forms and are in this
   % sense equivalent. There is no possible application of order
   % theoretical subsumption or cut between elements of $k$.
   begin scalar w,ll,res;
      ll := l;
      while ll do <<
	 w := cl_applysac1(car ll,res,gor);
	 if w eq 'break then <<
	    ll := nil;
	    res := 'break
	 >> else <<
	    ll := cdr ll;
	    if car w then
	       res := cdar w . cdr w
	    else
	       res := cdr w
	 >>
      >>;
      return res
   end;

procedure cl_applysac1(c,l,gor);
   % Common logic apply subsumption and cut 1. [c] is a list of atomic
   % formulas; [l] is a list of list of atomic formulas; [gor] is one
   % of [or], [and]. Returns ['break] or a pair $(c' . \lambda)$. If
   % ['break] is returned [l] is as a g-DNF equivalent to ['true] in
   % case of ['gor eq 'or] and equivalent to ['false] in case ['gor eq
   % 'and]. $c'$ is either [nil] or a pair $(\tau . \gamma)$, where
   % $\tau$ is one of [T] and [nil] and $\gamma$ is a list of atomic
   % formulas. $\lambda$ is a list of list of atomic formulas. If $c'$
   % is [nil] then the conjunction over [c] is implied by a
   % conjunction over an element in [l]. If $\tau$ is [T] then
   % $\gamma$ is equal to $c$, otherwise $\gamma$ is the result of a
   % cut between $c$ and an element of $l$. In all cases there is no
   % possible application of subsumption or cut between $\gamma$ and
   % an arbitrary element of $\lambda$. [l] is modified.
   begin scalar w,flg;
      flg:=T;
      repeat <<
	 w := cl_applysac2(c,l,gor);
	 if w eq 'break then <<
	    w := '(nil);  % leave the loop
	    flg := 'break
	 >>;
	 if car w and null caar w then <<
	    flg:=nil;
	    c := cdar w;
	    l := cdr w
	 >>;
      >> until null car w or caar w;
      if flg eq 'break then
	 return 'break;
      if null car w then
	 return w;
      return (flg . cdar w) . cdr w
   end;

procedure cl_applysac2(c,l,gor);
   % Common logic apply subsumption and cut 1. [c] is a list of atomic
   % formulas; [l] is a list of list of atomic formulas; [gor] is one
   % of [or], [and]. Returns ['break] or a pair ($c'$ . $\lambda$). If
   % ['break] is returned [l] is as a g-DNF equivalent to ['true] in
   % case of ['gor eq 'or] and equivalent to ['false] in case ['gor eq
   % 'and]. $c'$ is either [nil] or a pair $(\tau . \gamma)$, where
   % $\tau$ is one of [T] and [nil] and $\gamma$ is a list of atomic
   % formulas. $\lambda$ is a list of list of atomic formulas. If $c'$
   % is [nil] then the conjunction over [c] is implied by a
   % conjunction over an element in [l]. If $\tau$ is [T] then
   % $\gamma$ is equal to $c$, otherwise $\gamma$ is the result of a
   % cut between $c$ and an element of $l$. [l] is modified. If
   % ['break] is returned then the formula $['gor]([c],\phi)$ is
   % equivalent to ['true] in the case ['gor eq 'or] or to ['false] in
   % the case ['gor eq 'and].
   begin scalar w,ll;
      if null l then return ( (T . c) . nil);
      ll := l;
      while ll and ((w := cl_subandcut(c, car ll,gor)) eq 'keep1) do
	 ll := cdr ll;
      if null w then return 'break;
      if null ll then return ((T . c) . nil);
      if w eq 'keep2 then return (nil . ll);
      if w neq 'failed then  % [w] is the result of the cut
	                     % between [c] and [car ll].
	 return (nil . w) . cdr ll;
      % We know, that there is no interaction between [c] and [car ll]
      w := cl_applysac2(c,cdr ll,gor);
      if w eq 'break then
	 return 'break;
      cdr ll := cdr w;
      return car w . ll;
   end;

procedure cl_subandcut(l1,l2,gor);
   % Common logic subsumption and cut. [l1] and [l2] are sorted lists
   % of atomic formulas; [gor] is one of ['or], ['and]. Returns
   % ['failed], ['keep1], ['keep2] or a list of atomic formulas. Both
   % [l1] and [l2] are considered as conjunctions. ['keep1] is
   % returned if [l2] subsumes [l1]; ['keep2] is returned if [l1]
   % subsumes [l2]. If a list [l] of atomic formulas is returned then
   % [l] is the result of a cut between [l1] and [l2]. Both
   % subsumption and cut means order theoretical generalizations of
   % the respective notions of the propositional calculus.
   begin scalar state,w,x; integer c;
      x := l1;  % Save one of [l1] and [l2] for computing a cut.
      % Determing the maximal common prefix of [l1] and [l2] and its length.
      while l1 and l2 and (car l1 equal car l2) do <<
	 c := c+1;
	 l1 := cdr l1; l2 := cdr l2
      >>;
      if null (l1 and l2) then <<  % on of [l1] and [l2] are empty
      	 if null (l1 or l2) then return 'keep1;  % both equal.
	 % [l1] is a ``subset'' of [l2] or vice versa.
       	 return (l2 and 'keep1) or 'keep2
      >>;
      % We have [l1 and l2] and [car l1 neq car l2].
      state := 'keep1;
      w := rl_sacat(car l1,car l2,gor);  % [w neq 'keep]
      if w eq 'keep2 then <<
	 state := 'keep2;
	 % swap [l1] and [l2] upto the first element.
	 w := cdr l1; l1 := cdr l2; l2 := w
      >> else if w eq 'keep1 then <<
	 l1 := cdr l1; l2 := cdr l2
      >> else if w then
	 return cl_trycut(x,c,w,cdr l1,cdr l2)
      else if rl_ordatp(car l1,car l2) then <<  % [car l1 neq car l2]
	 state := 'keep2;
	 w := l1; l1 := l2; l2 := w
      >>;
      % Now [l1] is ``shorter'' than [l2]; no cuts are possible.
      while l1 do <<
	 w := cl_sacatl(car l1, l2,gor);
      	 l2 := cdr w; w := car w;
	 l1 := cdr l1;
	 if w neq 'keep1 then
	    l1 := nil  % Leave the loop.
      >>;
      if w eq 'keep1 then return state;
      return 'failed
   end;

procedure cl_trycut(l,c,at,l1,l2);
   % Common logic try cut. [l], [l1], and [l2] are lists of atomic
   % formulas; [c] is an integer; [at] is an atomic formula or
   % ['drop]. Returns ['failed] or a sorted list $\lambda$ of atomic
   % formulas. If a cut beween [l1] and [l2] are possible then a list
   % of atomic formulas is returned, otherwise [nil] is returned. [l]
   % is a list $(a_1,...,a_n)$, [l1] is a list $(c_1,...,c_m)$.
   % $lambda$ is a list $(a_1,...,a_c,b,c_1,...,c_m)$, where $b$ is
   % the atomic formula [at] if [at] is not [drop], otherwise $b$ is
   % ommitted.
   begin scalar a;
      if null l1 and null l2 then <<
	 l := for i := 1 : c collect <<
	    a := car l; l := cdr l; a
	 >>;
	 if at eq 'drop then
	    return sort(l,'rl_ordatp);
	 return sort(at . l,'rl_ordatp)
      >>;
      if l1 neq l2 then return 'failed;
      % [l1] and [l2] are equal.
      for i:=1:c do << l1 := car l . l1; l := cdr l >>;
      if at neq 'drop then
	 l1 := at . l1;
      return sort(l1,'rl_ordatp)
   end;

procedure cl_sacatl(a,l,gor);
   % Common logic subsume and cut atomic formula list. [a] is an
   % atomic formula; [l] is a sorted list of atomic formulas; [gor] is
   % one of [or], [and]. Returns a pair $(\alpha . \lambda)$ where
   % $\alpha$ is a relation, ['keep1], or [nil]; [l] is a possibly
   % empty list of atomic formulas. $\alpha$ is [T] if [a] is implied
   % by an atomic formula from [l]; if $\alpha$ is [nil] then neither
   % [a] is implied by an atomic formula from [l] nor a cut between
   % [a] and an atomic formula from [l] is possible, otherwise
   % $\alpha$ is the result of such a cut. $\lambda$ is the rest of
   % [l] not involved in the computation of $\alpha$.
   begin scalar w;
      if null l then
      	 return '(nil . nil);
      if not rl_sacatlp(a,l) then
      	 return (nil . l);
      w := rl_sacat(a,car l,gor);
      if not w then
      	 return cl_sacatl(a,cdr l,gor);
      if w memq '(keep1 keep) then
      	 return ('keep1 . cdr l);
      if w eq 'keep2 then
      	 return (nil . cdr l);
      return (w . cdr l)  % [w] is a relation or [drop]
   end;

procedure cl_bnfsimpl(sgdnf,gor);
   % Common logic boolean normal form simplification. [sgdnf] is an
   % SG-DNF; [gor] is one of the operators [and], [or]. Returns an
   % SG-DNF equivalent to [sgdnf]. Performs simplification of [gcl].
   % Accesses switch [rlbnfsac].
   if !*rlbnfsac then cl_sac(sgdnf,gor) else sgdnf;

procedure cl_sacatlp(a,l);
   % Common logic subsumption and cut atomic formula list predicate.
   % [a] is an atomic formula; [l] is a list of atomic formulas.
   % Returns [T] a subsumption or cut beween [a] and an element of [l]
   % is possible.
   T;

procedure cl_sacat(a1,a2,gor);
   % Common logic subsumption and cut atomic formula. [a1] and [a2]
   % are atomic formulas; [gor] is one of the operators [or], [and].
   % Returns [nil], one of the identifiers [keep], [keep1], [keep2],
   % [drop], or an atomic formula. The return value [nil] indicates
   % that neither a cut nor a subsumption can be applied. If [keep] is
   % returned, then the atomic formulas are identical. In the case of
   % [keep1] or [keep2] the corresponding atomic formula can be kept,
   % and the other one can be dropped. If an atomic formula $a$ is
   % returned, then this atomic formula is the result of the cut
   % beween [a1] and [a2]. If [drop] is returned, then a cut with
   % result [true] or [false] can be performed.
   if a1 = a2 then 'keep else nil;

endmodule;  % [clbnf]

end;