diff options
Diffstat (limited to 'src/algebra')
| -rw-r--r-- | src/algebra/Makefile.in | 2 | ||||
| -rw-r--r-- | src/algebra/Makefile.pamphlet | 2 | ||||
| -rw-r--r-- | src/algebra/boolean.spad.pamphlet | 436 |
3 files changed, 182 insertions, 258 deletions
diff --git a/src/algebra/Makefile.in b/src/algebra/Makefile.in index a974ad21..7fe8dd8f 100644 --- a/src/algebra/Makefile.in +++ b/src/algebra/Makefile.in @@ -377,7 +377,7 @@ axiom_algebra_layer_0 = \ KOERCE.o KONVERT.o MSYSCMD.o ODEIFTBL.o \ OM.o OMCONN.o OMDEV.o OUT.o \ PRIMCAT.o PRINT.o PTRANFN.o SPFCAT.o \ - TYPE.o UTYPE.o + TYPE.o UTYPE.o PROPLOG.o axiom_algebra_layer_0_nrlibs = \ $(axiom_algebra_layer_0:.$(OBJEXT)=.NRLIB/code.$(OBJEXT)) diff --git a/src/algebra/Makefile.pamphlet b/src/algebra/Makefile.pamphlet index 45f1f2bd..70a3f05c 100644 --- a/src/algebra/Makefile.pamphlet +++ b/src/algebra/Makefile.pamphlet @@ -205,7 +205,7 @@ axiom_algebra_layer_0 = \ KOERCE.o KONVERT.o MSYSCMD.o ODEIFTBL.o \ OM.o OMCONN.o OMDEV.o OUT.o \ PRIMCAT.o PRINT.o PTRANFN.o SPFCAT.o \ - TYPE.o UTYPE.o + TYPE.o UTYPE.o PROPLOG.o axiom_algebra_layer_0_nrlibs = \ $(axiom_algebra_layer_0:.$(OBJEXT)=.NRLIB/code.$(OBJEXT)) diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet index 84632fa5..85b2c056 100644 --- a/src/algebra/boolean.spad.pamphlet +++ b/src/algebra/boolean.spad.pamphlet @@ -1,14 +1,39 @@ \documentclass{article} \usepackage{axiom} + +\title{src/algebra boolean.spad} +\author{Stephen M. Watt, Michael Monagan, Gabriel Dos~Reis} + \begin{document} -\title{\$SPAD/src/algebra boolean.spad} -\author{Stephen M. Watt, Michael Monagan} \maketitle \begin{abstract} \end{abstract} -\eject + \tableofcontents \eject + +\section{category PROPLOG PropositionalLogic} +<<category PROPLOG PropositionalLogic>>= +)abbrev category PROPLOG PropositionalLogic +++ Author: Gabriel Dos Reis +++ Date Created: Januray 14, 2008 +++ Date Last Modified: January 14, 2008 +++ Description: This category declares the connectives of +++ Propositional Logic. +PropositionalLogic(): Category == with + "not": % -> % + ++ not p returns the logical negation of `p'. + "and": (%, %) -> % + ++ p and q returns the logical conjunction of `p', `q'. + "or": (%, %) -> % + ++ p or q returns the logical disjunction of `p', `q'. + implies: (%,%) -> % + ++ implies(p,q) returns the logical implication of `q' by `p'. + equiv: (%,%) -> % + ++ equiv(p,q) returns the logical equivalence of `p', `q'. +@ + + \section{domain REF Reference} <<domain REF Reference>>= )abbrev domain REF Reference @@ -131,20 +156,13 @@ Logic: Category == BasicType with ++ Description: \spadtype{Boolean} is the elementary logic with 2 values: ++ true and false -Boolean(): Join(OrderedSet, Finite, Logic, ConvertibleTo InputForm) with +Boolean(): Join(OrderedSet, Finite, Logic, PropositionalLogic, ConvertibleTo InputForm) with true : constant -> % ++ true is a logical constant. false : constant -> % ++ false is a logical constant. _^ : % -> % ++ ^ n returns the negation of n. - _not : % -> % - ++ not n returns the negation of n. - _and : (%, %) -> % - ++ a and b returns the logical {\em and} of Boolean \spad{a} and b. - _or : (%, %) -> % - ++ a or b returns the logical inclusive {\em or} - ++ of Boolean \spad{a} and b. xor : (%, %) -> % ++ xor(a,b) returns the logical exclusive {\em or} ++ of Boolean \spad{a} and b. @@ -152,9 +170,6 @@ Boolean(): Join(OrderedSet, Finite, Logic, ConvertibleTo InputForm) with ++ nand(a,b) returns the logical negation of \spad{a} and b. nor : (%, %) -> % ++ nor(a,b) returns the logical negation of \spad{a} or b. - implies: (%, %) -> % - ++ implies(a,b) returns the logical implication - ++ of Boolean \spad{a} and b. test: % -> Boolean ++ test(b) returns b and is provided for compatibility with the new compiler. == add @@ -178,6 +193,7 @@ Boolean(): Join(OrderedSet, Finite, Logic, ConvertibleTo InputForm) with nand(a, b) == (test a => nt b; true) a = b == BooleanEquality(a, b)$Lisp implies(a, b) == (test a => b; true) + equiv(a,b) == BooleanEquality(a, b)$Lisp a < b == (test b => not(test a);false) size() == 2 @@ -212,250 +228,157 @@ code and copy the {\bf BOOLEAN.o} file to the {\bf OUT} directory. This is eventually forcibly replaced by a recompiled version. <<BOOLEAN.lsp BOOTSTRAP>>= -(|/VERSIONCHECK| 2) +(/VERSIONCHECK 2) + +(PUT '|BOOLEAN;test;$B;1| '|SPADreplace| '(XLAM (|a|) |a|)) + +(DEFUN |BOOLEAN;test;$B;1| (|a| $) |a|) + +(DEFUN |BOOLEAN;nt| (|b| $) (COND (|b| 'NIL) ('T 'T))) + +(PUT '|BOOLEAN;true;$;3| '|SPADreplace| '(XLAM NIL 'T)) + +(DEFUN |BOOLEAN;true;$;3| ($) 'T) + +(PUT '|BOOLEAN;false;$;4| '|SPADreplace| '(XLAM NIL NIL)) + +(DEFUN |BOOLEAN;false;$;4| ($) NIL) + +(DEFUN |BOOLEAN;not;2$;5| (|b| $) (COND (|b| 'NIL) ('T 'T))) + +(DEFUN |BOOLEAN;^;2$;6| (|b| $) (COND (|b| 'NIL) ('T 'T))) + +(DEFUN |BOOLEAN;~;2$;7| (|b| $) (COND (|b| 'NIL) ('T 'T))) + +(DEFUN |BOOLEAN;and;3$;8| (|a| |b| $) (COND (|a| |b|) ('T 'NIL))) + +(DEFUN |BOOLEAN;/\\;3$;9| (|a| |b| $) (COND (|a| |b|) ('T 'NIL))) + +(DEFUN |BOOLEAN;or;3$;10| (|a| |b| $) (COND (|a| 'T) ('T |b|))) + +(DEFUN |BOOLEAN;\\/;3$;11| (|a| |b| $) (COND (|a| 'T) ('T |b|))) + +(DEFUN |BOOLEAN;xor;3$;12| (|a| |b| $) + (COND (|a| (|BOOLEAN;nt| |b| $)) ('T |b|))) -(PUT - (QUOTE |BOOLEAN;test;2$;1|) - (QUOTE |SPADreplace|) - (QUOTE (XLAM (|a|) |a|))) - -(DEFUN |BOOLEAN;test;2$;1| (|a| |$|) |a|) - -(DEFUN |BOOLEAN;nt| (|b| |$|) - (COND (|b| (QUOTE NIL)) - ((QUOTE T) (QUOTE T)))) - -(PUT - (QUOTE |BOOLEAN;true;$;3|) - (QUOTE |SPADreplace|) - (QUOTE (XLAM NIL (QUOTE T)))) - -(DEFUN |BOOLEAN;true;$;3| (|$|) - (QUOTE T)) - -(PUT - (QUOTE |BOOLEAN;false;$;4|) - (QUOTE |SPADreplace|) - (QUOTE (XLAM NIL NIL))) - -(DEFUN |BOOLEAN;false;$;4| (|$|) NIL) - -(DEFUN |BOOLEAN;not;2$;5| (|b| |$|) - (COND - (|b| (QUOTE NIL)) - ((QUOTE T) (QUOTE T)))) - -(DEFUN |BOOLEAN;^;2$;6| (|b| |$|) - (COND - (|b| (QUOTE NIL)) - ((QUOTE T) (QUOTE T)))) - -(DEFUN |BOOLEAN;~;2$;7| (|b| |$|) - (COND - (|b| (QUOTE NIL)) - ((QUOTE T) (QUOTE T)))) - -(DEFUN |BOOLEAN;and;3$;8| (|a| |b| |$|) - (COND - (|a| |b|) - ((QUOTE T) (QUOTE NIL)))) - -(DEFUN |BOOLEAN;/\\;3$;9| (|a| |b| |$|) - (COND - (|a| |b|) - ((QUOTE T) (QUOTE NIL)))) - -(DEFUN |BOOLEAN;or;3$;10| (|a| |b| |$|) - (COND - (|a| (QUOTE T)) - ((QUOTE T) |b|))) - -(DEFUN |BOOLEAN;\\/;3$;11| (|a| |b| |$|) - (COND - (|a| (QUOTE T)) - ((QUOTE T) |b|))) - -(DEFUN |BOOLEAN;xor;3$;12| (|a| |b| |$|) - (COND - (|a| (|BOOLEAN;nt| |b| |$|)) - ((QUOTE T) |b|))) - -(DEFUN |BOOLEAN;nor;3$;13| (|a| |b| |$|) - (COND - (|a| (QUOTE NIL)) - ((QUOTE T) (|BOOLEAN;nt| |b| |$|)))) - -(DEFUN |BOOLEAN;nand;3$;14| (|a| |b| |$|) - (COND - (|a| (|BOOLEAN;nt| |b| |$|)) - ((QUOTE T) (QUOTE T)))) - -(PUT - (QUOTE |BOOLEAN;=;3$;15|) - (QUOTE |SPADreplace|) - (QUOTE |BooleanEquality|)) - -(DEFUN |BOOLEAN;=;3$;15| (|a| |b| |$|) - (|BooleanEquality| |a| |b|)) - -(DEFUN |BOOLEAN;implies;3$;16| (|a| |b| |$|) - (COND - (|a| |b|) - ((QUOTE T) (QUOTE T)))) - -(DEFUN |BOOLEAN;<;3$;17| (|a| |b| |$|) - (COND - (|b| - (COND - (|a| (QUOTE NIL)) - ((QUOTE T) (QUOTE T)))) - ((QUOTE T) (QUOTE NIL)))) - -(PUT - (QUOTE |BOOLEAN;size;Nni;18|) - (QUOTE |SPADreplace|) - (QUOTE (XLAM NIL 2))) - -(DEFUN |BOOLEAN;size;Nni;18| (|$|) 2) - -(DEFUN |BOOLEAN;index;Pi$;19| (|i| |$|) - (COND - ((SPADCALL |i| (QREFELT |$| 26)) (QUOTE NIL)) - ((QUOTE T) (QUOTE T)))) - -(DEFUN |BOOLEAN;lookup;$Pi;20| (|a| |$|) - (COND - (|a| 1) - ((QUOTE T) 2))) - -(DEFUN |BOOLEAN;random;$;21| (|$|) - (COND - ((SPADCALL (|random|) (QREFELT |$| 26)) (QUOTE NIL)) - ((QUOTE T) (QUOTE T)))) - -(DEFUN |BOOLEAN;convert;$If;22| (|x| |$|) - (COND - (|x| (SPADCALL (SPADCALL "true" (QREFELT |$| 33)) (QREFELT |$| 35))) - ((QUOTE T) - (SPADCALL (SPADCALL "false" (QREFELT |$| 33)) (QREFELT |$| 35))))) - -(DEFUN |BOOLEAN;coerce;$Of;23| (|x| |$|) - (COND - (|x| (SPADCALL "true" (QREFELT |$| 38))) - ((QUOTE T) (SPADCALL "false" (QREFELT |$| 38))))) - -(DEFUN |Boolean| NIL - (PROG NIL - (RETURN - (PROG (#1=#:G82461) - (RETURN - (COND - ((LETT #1# - (HGET |$ConstructorCache| (QUOTE |Boolean|)) - |Boolean|) - (|CDRwithIncrement| (CDAR #1#))) - ((QUOTE T) - (|UNWIND-PROTECT| - (PROG1 - (CDDAR - (HPUT - |$ConstructorCache| - (QUOTE |Boolean|) - (LIST (CONS NIL (CONS 1 (|Boolean;|)))))) - (LETT #1# T |Boolean|)) - (COND - ((NOT #1#) - (HREM |$ConstructorCache| (QUOTE |Boolean|)))))))))))) - -(DEFUN |Boolean;| NIL - (PROG (|dv$| |$| |pv$|) - (RETURN - (PROGN - (LETT |dv$| (QUOTE (|Boolean|)) . #1=(|Boolean|)) - (LETT |$| (GETREFV 41) . #1#) - (QSETREFV |$| 0 |dv$|) - (QSETREFV |$| 3 (LETT |pv$| (|buildPredVector| 0 0 NIL) . #1#)) - (|haddProp| |$ConstructorCache| (QUOTE |Boolean|) NIL (CONS 1 |$|)) - (|stuffDomainSlots| |$|) |$|)))) - -(MAKEPROP - (QUOTE |Boolean|) - (QUOTE |infovec|) - (LIST - (QUOTE - #(NIL NIL NIL NIL NIL NIL - (|Boolean|) - |BOOLEAN;test;2$;1| - (CONS IDENTITY - (FUNCALL (|dispatchFunction| |BOOLEAN;true;$;3|) |$|)) - (CONS IDENTITY - (FUNCALL (|dispatchFunction| |BOOLEAN;false;$;4|) |$|)) - |BOOLEAN;not;2$;5| - |BOOLEAN;^;2$;6| - |BOOLEAN;~;2$;7| - |BOOLEAN;and;3$;8| - |BOOLEAN;/\\;3$;9| - |BOOLEAN;or;3$;10| - |BOOLEAN;\\/;3$;11| - |BOOLEAN;xor;3$;12| - |BOOLEAN;nor;3$;13| - |BOOLEAN;nand;3$;14| - |BOOLEAN;=;3$;15| - |BOOLEAN;implies;3$;16| - |BOOLEAN;<;3$;17| - (|NonNegativeInteger|) - |BOOLEAN;size;Nni;18| - (|Integer|) - (0 . |even?|) - (|PositiveInteger|) - |BOOLEAN;index;Pi$;19| - |BOOLEAN;lookup;$Pi;20| - |BOOLEAN;random;$;21| - (|String|) - (|Symbol|) - (5 . |coerce|) - (|InputForm|) - (10 . |convert|) - |BOOLEAN;convert;$If;22| - (|OutputForm|) - (15 . |message|) - |BOOLEAN;coerce;$Of;23| - (|SingleInteger|))) - (QUOTE - #(|~=| 20 |~| 26 |xor| 31 |true| 37 |test| 41 |size| 46 |random| 50 - |or| 54 |not| 60 |nor| 65 |nand| 71 |min| 77 |max| 83 |lookup| 89 - |latex| 94 |index| 99 |implies| 104 |hash| 110 |false| 115 - |convert| 119 |coerce| 124 |and| 129 |^| 135 |\\/| 140 |>=| 146 - |>| 152 |=| 158 |<=| 164 |<| 170 |/\\| 176)) - (QUOTE NIL) - (CONS - (|makeByteWordVec2| 1 (QUOTE (0 0 0 0 0 0 0))) - (CONS - (QUOTE - #(|OrderedSet&| NIL |Logic&| |SetCategory&| NIL |BasicType&| NIL)) - (CONS - (QUOTE - #((|OrderedSet|) - (|Finite|) - (|Logic|) - (|SetCategory|) - (|ConvertibleTo| 34) - (|BasicType|) - (|CoercibleTo| 37))) - (|makeByteWordVec2| - 40 - (QUOTE - (1 25 6 0 26 1 32 0 31 33 1 34 0 32 35 1 37 0 31 38 2 0 6 0 0 - 1 1 0 0 0 12 2 0 0 0 0 17 0 0 0 8 1 0 6 0 7 0 0 23 24 0 0 0 - 30 2 0 0 0 0 15 1 0 0 0 10 2 0 0 0 0 18 2 0 0 0 0 19 2 0 0 0 - 0 1 2 0 0 0 0 1 1 0 27 0 29 1 0 31 0 1 1 0 0 27 28 2 0 0 0 0 - 21 1 0 40 0 1 0 0 0 9 1 0 34 0 36 1 0 37 0 39 2 0 0 0 0 13 1 - 0 0 0 11 2 0 0 0 0 16 2 0 6 0 0 1 2 0 6 0 0 1 2 0 6 0 0 20 2 - 0 6 0 0 1 2 0 6 0 0 22 2 0 0 0 0 14)))))) - (QUOTE |lookupComplete|))) - -(MAKEPROP (QUOTE |Boolean|) (QUOTE NILADIC) T) +(DEFUN |BOOLEAN;nor;3$;13| (|a| |b| $) + (COND (|a| 'NIL) ('T (|BOOLEAN;nt| |b| $)))) +(DEFUN |BOOLEAN;nand;3$;14| (|a| |b| $) + (COND (|a| (|BOOLEAN;nt| |b| $)) ('T 'T))) + +(PUT '|BOOLEAN;=;2$B;15| '|SPADreplace| '|BooleanEquality|) + +(DEFUN |BOOLEAN;=;2$B;15| (|a| |b| $) (|BooleanEquality| |a| |b|)) + +(DEFUN |BOOLEAN;implies;3$;16| (|a| |b| $) (COND (|a| |b|) ('T 'T))) + +(PUT '|BOOLEAN;equiv;3$;17| '|SPADreplace| '|BooleanEquality|) + +(DEFUN |BOOLEAN;equiv;3$;17| (|a| |b| $) (|BooleanEquality| |a| |b|)) + +(DEFUN |BOOLEAN;<;2$B;18| (|a| |b| $) + (COND (|b| (SPADCALL |a| (QREFELT $ 23))) ('T 'NIL))) + +(PUT '|BOOLEAN;size;Nni;19| '|SPADreplace| '(XLAM NIL 2)) + +(DEFUN |BOOLEAN;size;Nni;19| ($) 2) + +(DEFUN |BOOLEAN;index;Pi$;20| (|i| $) + (COND ((SPADCALL |i| (QREFELT $ 28)) 'NIL) ('T 'T))) + +(DEFUN |BOOLEAN;lookup;$Pi;21| (|a| $) (COND (|a| 1) ('T 2))) + +(DEFUN |BOOLEAN;random;$;22| ($) + (COND ((SPADCALL (|random|) (QREFELT $ 28)) 'NIL) ('T 'T))) + +(DEFUN |BOOLEAN;convert;$If;23| (|x| $) + (COND + (|x| (SPADCALL (SPADCALL "true" (QREFELT $ 35)) (QREFELT $ 37))) + ('T (SPADCALL (SPADCALL "false" (QREFELT $ 35)) (QREFELT $ 37))))) + +(DEFUN |BOOLEAN;coerce;$Of;24| (|x| $) + (COND + (|x| (SPADCALL "true" (QREFELT $ 40))) + ('T (SPADCALL "false" (QREFELT $ 40))))) + +(DEFUN |Boolean| () + (PROG () + (RETURN + (PROG (#0=#:G1458) + (RETURN + (COND + ((LETT #0# (HGET |$ConstructorCache| '|Boolean|) |Boolean|) + (|CDRwithIncrement| (CDAR #0#))) + ('T + (UNWIND-PROTECT + (PROG1 (CDDAR (HPUT |$ConstructorCache| '|Boolean| + (LIST + (CONS NIL (CONS 1 (|Boolean;|)))))) + (LETT #0# T |Boolean|)) + (COND + ((NOT #0#) (HREM |$ConstructorCache| '|Boolean|))))))))))) + +(DEFUN |Boolean;| () + (PROG (|dv$| $ |pv$|) + (RETURN + (PROGN + (LETT |dv$| '(|Boolean|) . #0=(|Boolean|)) + (LETT $ (GETREFV 43) . #0#) + (QSETREFV $ 0 |dv$|) + (QSETREFV $ 3 (LETT |pv$| (|buildPredVector| 0 0 NIL) . #0#)) + (|haddProp| |$ConstructorCache| '|Boolean| NIL (CONS 1 $)) + (|stuffDomainSlots| $) + $)))) + +(MAKEPROP '|Boolean| '|infovec| + (LIST '#(NIL NIL NIL NIL NIL NIL (|Boolean|) |BOOLEAN;test;$B;1| + (CONS IDENTITY + (FUNCALL (|dispatchFunction| |BOOLEAN;true;$;3|) $)) + (CONS IDENTITY + (FUNCALL (|dispatchFunction| |BOOLEAN;false;$;4|) $)) + |BOOLEAN;not;2$;5| |BOOLEAN;^;2$;6| |BOOLEAN;~;2$;7| + |BOOLEAN;and;3$;8| |BOOLEAN;/\\;3$;9| |BOOLEAN;or;3$;10| + |BOOLEAN;\\/;3$;11| |BOOLEAN;xor;3$;12| + |BOOLEAN;nor;3$;13| |BOOLEAN;nand;3$;14| + |BOOLEAN;=;2$B;15| |BOOLEAN;implies;3$;16| + |BOOLEAN;equiv;3$;17| (0 . |not|) |BOOLEAN;<;2$B;18| + (|NonNegativeInteger|) |BOOLEAN;size;Nni;19| (|Integer|) + (5 . |even?|) (|PositiveInteger|) |BOOLEAN;index;Pi$;20| + |BOOLEAN;lookup;$Pi;21| |BOOLEAN;random;$;22| (|String|) + (|Symbol|) (10 . |coerce|) (|InputForm|) (15 . |convert|) + |BOOLEAN;convert;$If;23| (|OutputForm|) (20 . |message|) + |BOOLEAN;coerce;$Of;24| (|SingleInteger|)) + '#(~= 25 ~ 31 |xor| 36 |true| 42 |test| 46 |size| 51 |random| + 55 |or| 59 |not| 65 |nor| 70 |nand| 76 |min| 82 |max| 88 + |lookup| 94 |latex| 99 |index| 104 |implies| 109 |hash| + 115 |false| 120 |equiv| 124 |convert| 130 |coerce| 135 + |and| 140 ^ 146 |\\/| 151 >= 157 > 163 = 169 <= 175 < 181 + |/\\| 187) + 'NIL + (CONS (|makeByteWordVec2| 1 '(0 0 0 0 0 0 0 0)) + (CONS '#(|OrderedSet&| NIL |Logic&| |SetCategory&| NIL + NIL |BasicType&| NIL) + (CONS '#((|OrderedSet|) (|Finite|) (|Logic|) + (|SetCategory|) (|ConvertibleTo| 36) + (|PropositionalLogic|) (|BasicType|) + (|CoercibleTo| 39)) + (|makeByteWordVec2| 42 + '(1 6 0 0 23 1 27 6 0 28 1 34 0 33 35 1 + 36 0 34 37 1 39 0 33 40 2 0 6 0 0 1 1 + 0 0 0 12 2 0 0 0 0 17 0 0 0 8 1 0 6 0 + 7 0 0 25 26 0 0 0 32 2 0 0 0 0 15 1 0 + 0 0 10 2 0 0 0 0 18 2 0 0 0 0 19 2 0 + 0 0 0 1 2 0 0 0 0 1 1 0 29 0 31 1 0 + 33 0 1 1 0 0 29 30 2 0 0 0 0 21 1 0 + 42 0 1 0 0 0 9 2 0 0 0 0 22 1 0 36 0 + 38 1 0 39 0 41 2 0 0 0 0 13 1 0 0 0 + 11 2 0 0 0 0 16 2 0 6 0 0 1 2 0 6 0 0 + 1 2 0 6 0 0 20 2 0 6 0 0 1 2 0 6 0 0 + 24 2 0 0 0 0 14))))) + '|lookupComplete|)) + +(MAKEPROP '|Boolean| 'NILADIC T) @ \section{domain IBITS IndexedBits} <<domain IBITS IndexedBits>>= @@ -579,6 +502,7 @@ Bits(): Exports == Implementation where <<domain BOOLEAN Boolean>> <<domain IBITS IndexedBits>> <<domain BITS Bits>> +<<category PROPLOG PropositionalLogic>> @ \eject \begin{thebibliography}{99} |