diff options
Diffstat (limited to 'src/interp/simpbool.boot.pamphlet')
| -rw-r--r-- | src/interp/simpbool.boot.pamphlet | 225 |
1 files changed, 0 insertions, 225 deletions
diff --git a/src/interp/simpbool.boot.pamphlet b/src/interp/simpbool.boot.pamphlet deleted file mode 100644 index 88021ab9..00000000 --- a/src/interp/simpbool.boot.pamphlet +++ /dev/null @@ -1,225 +0,0 @@ -\documentclass{article} -\usepackage{axiom} -\begin{document} -\title{\$SPAD/src/interp simpbool.boot} -\author{The Axiom Team} -\maketitle -\begin{abstract} -\end{abstract} -\eject -\tableofcontents -\eject -\section{License} -<<license>>= --- Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd. --- All rights reserved. --- --- Redistribution and use in source and binary forms, with or without --- modification, are permitted provided that the following conditions are --- met: --- --- - Redistributions of source code must retain the above copyright --- notice, this list of conditions and the following disclaimer. --- --- - Redistributions in binary form must reproduce the above copyright --- notice, this list of conditions and the following disclaimer in --- the documentation and/or other materials provided with the --- distribution. --- --- - Neither the name of The Numerical ALgorithms Group Ltd. nor the --- names of its contributors may be used to endorse or promote products --- derived from this software without specific prior written permission. --- --- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS --- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED --- TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A --- PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER --- OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, --- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, --- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR --- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF --- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING --- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS --- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - -@ -<<*>>= -<<license>> - -)package "BOOT" - -simpBool x == dnf2pf reduceDnf be x - -reduceDnf u == --- (OR (AND ..b..) b) ==> (OR b ) - atom u => u - for x in u repeat - ok := true - for y in u repeat - x = y => 'skip - dnfContains(x,y) => return (ok := false) - ok = true => acc := [x,:acc] - nreverse acc - -dnfContains([a,b],[c,d]) == fn(a,c) and fn(b,d) where - fn(x,y) == and/[member(u,x) for u in y] - -prove x == - world := [p for y in listOfUserIds x | (p := getPredicate y)] => - 'false = be mkpf([['NOT,x],:world],'AND) => true - 'false = be mkpf([x,:world],'AND) => false - x - 'false = (y := be x) => 'false - y = 'true => true - dnf2pf y - -simpBoolGiven(x,world) == - world => - 'false = be mkpf([['NOT,x],:world],'AND) => true - 'false = (y := be mkpf([x,:world],'AND)) => false - (u := andReduce(dnf2pf y,world)) is ['AND,:v] and - (w := SETDIFFERENCE(v,world)) ^= v => simpBool ['AND,:w] - u - 'false = (y := be x) => false - 'true = y => true - dnf2pf y - -andReduce(x,y) == - x is ['AND,:r] => - y is ['AND,:s] => mkpf(S_-(r,s),'AND) - mkpf(S_-(r,[s]),'AND) - x -dnf2pf(x) == - x = 'true => 'T - x = 'false => nil - atom x => x - mkpf( - [mkpf([:[k for k in b],:[['not,k] for k in a]],'AND) for [a,b] in x],'OR) -be x == b2dnf x -b2dnf x == - x = 'T => 'true - x = NIL => 'false - atom x => bassert x - [op,:argl] := x - MEMQ(op,'(AND and)) => band argl - MEMQ(op,'(OR or)) => bor argl - MEMQ(op,'(NOT not)) => bnot first argl - bassert x -band x == - x is [h,:t] => andDnf(b2dnf h,band t) - 'true -bor x == - x is [a,:b] => orDnf(b2dnf a,bor b) - 'false -bnot x == notDnf b2dnf x -bassert x == [[nil,[x]]] -bassertNot x == [[[x],nil]] -------------------------Disjunctive Normal Form Code----------------------- --- dnf is true | false | [coaf ... ] --- coaf is true | false | [item ... ] --- item is anything - -orDnf(a,b) == -- or: (dnf, dnf) -> dnf - a = 'false => b - b = 'false => a - a = 'true or b = 'true => 'true - null a => b --null list means false - a is [c] = coafOrDnf(c,b) - coafOrDnf(first a,orDnf(rest a,b)) - -andDnf(a,b) == -- and: (dnf, dnf) -> dnf - a = 'true => b - b = 'true => a - a = 'false or b = 'false => 'false - null a => 'false --null list means false - a is [c] => coafAndDnf(c,b) - x := coafAndDnf(first a,b) - y := andDnf(rest a,b) - x = 'false => y - y = 'false => x - ordUnion(x,y) - -notDnf l == -- not: dnf -> dnf - l = 'true => 'false - l = 'false => 'true - null l => 'true --null list means false - l is [x] => notCoaf x - andDnf(notCoaf first l,notDnf rest l) - -coafOrDnf(a,l) == -- or: (coaf, dnf) -> dnf - a = 'true or l = 'true => 'true - a = 'false => l - member(a,l) => l - y := notCoaf a - x := ordIntersection(y,l) - null x => orDel(a,l) - x = l => 'true - x = y => ordSetDiff(l,x) - ordUnion(notDnf ordSetDiff(y,x),l) - -coafAndDnf(a,b) == --and: (coaf, dnf) -> dnf - a = 'true => b - a = 'false => 'false - [c,:r] := b - null r => coafAndCoaf(a,c) - x := coafAndCoaf(a,c) --dnf - y := coafAndDnf(a,r) --dnf - x = 'false => y - y = 'false => x - ordUnion(x,y) - -coafAndCoaf([a,b],[p,q]) == --and: (coaf,coaf) -> dnf - ordIntersection(a,q) or ordIntersection(b,p) => 'false - [[ordUnion(a,p),ordUnion(b,q)]] - -notCoaf [a,b] == [:[[nil,[x]] for x in a],:[[[x],nil] for x in b]] - -list1 l == - l isnt [h,:t] => nil - null h => list1 t - [[h,nil,nil],:list1 t] -list2 l == - l isnt [h,:t] => nil - null h => list2 t - [[nil,h,nil],:list2 t] -list3 l == - l isnt [h,:t] => nil - null h => list3 t - [[nil,nil,h],:list3 t] -orDel(a,l) == - l is [h,:t] => - a = h => t - ?ORDER(a,h) => [a,:l] - [h,:orDel(a,t)] - [a] -ordList l == - l is [h,:t] and t => orDel(h,ordList t) - l -ordUnion(a,b) == - a isnt [c,:r] => b - b isnt [d,:s] => a - c=d => [c,:ordUnion(r,s)] - ?ORDER(a,b) => [c,:ordUnion(r,b)] - [d,:ordUnion(s,a)] -ordIntersection(a,b) == - a isnt [h,:t] => nil - member(h,b) => [h,:ordIntersection(t,b)] - ordIntersection(t,b) -ordSetDiff(a,b) == - b isnt [h,:t] => a - member(h,a) => ordSetDiff(delete(h,a),t) - ordSetDiff(a,t) -------------- -testPredList u == - for x in u repeat - y := simpBool x - x = y => nil - pp x - pp '"==========>" - pp y -@ -\eject -\begin{thebibliography}{99} -\bibitem{1} nothing -\end{thebibliography} -\end{document} |