\documentclass{article} \usepackage{axiom} \title{src/algebra boolean.spad} \author{Stephen M. Watt, Michael Monagan, Gabriel Dos~Reis} \begin{document} \maketitle \begin{abstract} \end{abstract} \tableofcontents \eject \section{category PROPLOG PropositionalLogic} <>= )abbrev category PROPLOG PropositionalLogic ++ Author: Gabriel Dos Reis ++ Date Created: Januray 14, 2008 ++ Date Last Modified: September 20, 2008 ++ Description: This category declares the connectives of ++ Propositional Logic. PropositionalLogic(): Category == SetCategory 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 PROPFRML PropositionalFormula} <>= )set mess autoload on )abbrev domain PROPFRML PropositionalFormula ++ Author: Gabriel Dos Reis ++ Date Created: Januray 14, 2008 ++ Date Last Modified: January 16, 2008 ++ Description: This domain implements propositional formula build ++ over a term domain, that itself belongs to PropositionalLogic PropositionalFormula(T: PropositionalLogic): PropositionalLogic with coerce: T -> % ++ coerce(t) turns the term `t' into a propositional formula coerce: Symbol -> % ++ coerce(t) turns the term `t' into a propositional variable. variables: % -> Set Symbol ++ variables(p) returns the set of propositional variables ++ appearing in the proposition `p'. term?: % -> Boolean ++ term? p returns true when `p' really is a term term: % -> T ++ term p extracts the term value from `p'; otherwise errors. variable?: % -> Boolean ++ variables? p returns true when `p' really is a variable. variable: % -> Symbol ++ variable p extracts the variable name from `p'; otherwise errors. not?: % -> Boolean ++ not? p is true when `p' is a logical negation notOperand: % -> % ++ notOperand returns the operand to the logical `not' operator; ++ otherwise errors. and?: % -> Boolean ++ and? p is true when `p' is a logical conjunction. andOperands: % -> Pair(%, %) ++ andOperands p extracts the operands of the logical conjunction; ++ otherwise errors. or?: % -> Boolean ++ or? p is true when `p' is a logical disjunction. orOperands: % -> Pair(%,%) ++ orOperands p extracts the operands to the logical disjunction; ++ otherwise errors. implies?: % -> Boolean ++ implies? p is true when `p' is a logical implication. impliesOperands: % -> Pair(%,%) ++ impliesOperands p extracts the operands to the logical ++ implication; otherwise errors. equiv?: % -> Boolean ++ equiv? p is true when `p' is a logical equivalence. equivOperands: % -> Pair(%,%) ++ equivOperands p extracts the operands to the logical equivalence; ++ otherwise errors. == add FORMULA ==> Union(base: T, var: Symbol, unForm: %, binForm: Record(op: Symbol, lhs: %, rhs: %)) per(f: FORMULA): % == f pretend % rep(p: %): FORMULA == p pretend FORMULA coerce(t: T): % == per [t]$FORMULA coerce(s: Symbol): % == per [s]$FORMULA not p == per [p]$FORMULA binaryForm(o: Symbol, l: %, r: %): % == per [[o, l, r]$Record(op: Symbol, lhs: %, rhs: %)]$FORMULA p and q == binaryForm('_and, p, q) p or q == binaryForm('_or, p, q) implies(p,q) == binaryForm('implies, p, q) equiv(p,q) == binaryForm('equiv, p, q) variables p == p' := rep p p' case base => empty()$Set(Symbol) p' case var => { p'.var } p' case unForm => variables(p'.unForm) p'' := p'.binForm union(variables(p''.lhs), variables(p''.rhs))$Set(Symbol) -- returns true if the proposition `p' is a formula of kind -- indicated by `o'. isBinaryNode?(p: %, o: Symbol): Boolean == p' := rep p p' case binForm and p'.binForm.op = o -- returns the operands of a binary formula node binaryOperands(p: %): Pair(%,%) == p' := (rep p).binForm pair(p'.lhs,p'.rhs)$Pair(%,%) term? p == rep p case base term p == term? p => (rep p).base userError "formula is not a term" variable? p == rep p case var variable p == variable? p => (rep p).var userError "formula is not a variable" not? p == rep p case unForm notOperand p == not? p => (rep p).unForm userError "formula is not a logical negation" and? p == isBinaryNode?(p,'_and) andOperands p == and? p => binaryOperands p userError "formula is not a conjunction formula" or? p == isBinaryNode?(p,'_or) orOperands p == or? p => binaryOperands p userError "formula is not a disjunction formula" implies? p == isBinaryNode?(p, 'implies) impliesOperands p == implies? p => binaryOperands p userError "formula is not an implication formula" equiv? p == isBinaryNode?(p,'equiv) equivOperands p == equiv? p => binaryOperands p userError "formula is not an equivalence equivalence" -- Unparsing grammar. -- -- Ideally, the following syntax would the external form -- Formula: -- EquivFormula -- -- EquivFormula: -- ImpliesFormula -- ImpliesFormula <=> EquivFormula -- -- ImpliesFormula: -- OrFormula -- OrFormula => ImpliesFormula -- -- OrFormula: -- AndFormula -- AndFormula or OrFormula -- -- AndFormula -- NotFormula -- NotFormula and AndFormula -- -- NotFormula: -- PrimaryFormula -- not NotFormula -- -- PrimaryFormula: -- Term -- ( Formula ) -- -- Note: Since the token '=>' already means a construct different -- from what we would like to have as a notation for -- propositional logic, we will output the formula `p => q' -- as implies(p,q), which looks like a function call. -- Similarly, we do not have the token `<=>' for logical -- equivalence; so we unparser `p <=> q' as equiv(p,q). -- -- So, we modify the nonterminal PrimaryFormula to read -- PrimaryFormula: -- Term -- implies(Formula, Formula) -- equiv(Formula, Formula) formula: % -> OutputForm coerce(p: %): OutputForm == formula p primaryFormula(p: %): OutputForm == term? p => term(p)::OutputForm variable? p => variable(p)::OutputForm if rep p case binForm then p' := (rep p).binForm p'.op = 'implies or p'.op = 'equiv => return elt(outputForm p'.op, [formula p'.lhs, formula p'.rhs])$OutputForm paren(formula p)$OutputForm notFormula(p: %): OutputForm == not? p => elt(outputForm '_not, [notFormula((rep p).unForm)])$OutputForm primaryFormula p andFormula(p: %): OutputForm == and? p => p' := (rep p).binForm -- ??? idealy, we should be using `and$OutputForm' but -- ??? a bug in the compiler currently prevents that. infix(outputForm '_and, notFormula p'.lhs, andFormula p'.rhs)$OutputForm notFormula p orFormula(p: %): OutputForm == or? p => p' := (rep p).binForm -- ??? idealy, we should be using `or$OutputForm' but -- ??? a bug in the compiler currently prevents that. infix(outputForm '_or, andFormula p'.lhs, orFormula p'.rhs)$OutputForm andFormula p formula p == -- Note: this should be equivFormula, but see the explanation above. orFormula p @ \section{domain REF Reference} <>= )abbrev domain REF Reference ++ Author: Stephen M. Watt ++ Date Created: ++ Change History: ++ Basic Operations: deref, elt, ref, setelt, setref, = ++ Related Constructors: ++ Keywords: reference ++ Description: \spadtype{Reference} is for making a changeable instance ++ of something. Reference(S:Type): Type with ref : S -> % ++ ref(n) creates a pointer (reference) to the object n. elt : % -> S ++ elt(n) returns the object n. setelt: (%, S) -> S ++ setelt(n,m) changes the value of the object n to m. -- alternates for when bugs don't allow the above deref : % -> S ++ deref(n) is equivalent to \spad{elt(n)}. setref: (%, S) -> S ++ setref(n,m) same as \spad{setelt(n,m)}. _= : (%, %) -> Boolean ++ a=b tests if \spad{a} and b are equal. if S has SetCategory then SetCategory == add Rep := Record(value: S) p = q == EQ(p, q)$Lisp ref v == [v] elt p == p.value setelt(p, v) == p.value := v deref p == p.value setref(p, v) == p.value := v if S has SetCategory then coerce p == prefix(message("ref"@String), [p.value::OutputForm]) @ \section{category LOGIC Logic} <>= )abbrev category LOGIC Logic ++ Author: ++ Date Created: ++ Change History: ++ Basic Operations: ~, /\, \/ ++ Related Constructors: ++ Keywords: boolean ++ Description: ++ `Logic' provides the basic operations for lattices, ++ e.g., boolean algebra. Logic: Category == BasicType with _~: % -> % ++ ~(x) returns the logical complement of x. _/_\: (%, %) -> % ++ \spadignore { /\ }returns the logical `meet', e.g. `and'. _\_/: (%, %) -> % ++ \spadignore{ \/ } returns the logical `join', e.g. `or'. add _\_/(x: %,y: %) == _~( _/_\(_~(x), _~(y))) @ \section{domain BOOLEAN Boolean} <>= )abbrev domain BOOLEAN Boolean ++ Author: Stephen M. Watt ++ Date Created: ++ Date Last Changed: September 20, 2008 ++ Basic Operations: true, false, not, and, or, xor, nand, nor, implies ++ Related Constructors: ++ Keywords: boolean ++ Description: \spadtype{Boolean} is the elementary logic with 2 values: ++ true and false Boolean(): Join(OrderedFinite, Logic, PropositionalLogic, ConvertibleTo InputForm) with true: % ++ true is a logical constant. false: % ++ false is a logical constant. xor : (%, %) -> % ++ xor(a,b) returns the logical exclusive {\em or} ++ of Boolean \spad{a} and b. nand : (%, %) -> % ++ 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. test: % -> % ++ test(b) returns b and is provided for compatibility with the new compiler. == add test a == a nt(a: %): % == NOT(a)$Lisp true == 'T pretend % false == NIL$Lisp sample() == true not b == nt b _~ b == (b => false; true) _and(a, b) == AND(a,b)$Lisp _/_\(a, b) == AND(a,b)$Lisp _or(a, b) == OR(a,b)$Lisp _\_/(a, b) == OR(a,b)$Lisp xor(a, b) == (a => nt b; b) nor(a, b) == (a => false; nt b) nand(a, b) == (a => nt b; true) a = b == EQ(a, b)$Lisp implies(a, b) == (a => b; true) equiv(a,b) == EQ(a, b)$Lisp a < b == (b => nt a; false) size() == 2 index i == even?(i::Integer) => false true lookup a == a => 1 2 random() == even?(random()$Integer) => false true convert(x:%):InputForm == convert x => 'true 'false coerce(x:%):OutputForm == outputForm x => 'true 'false @ \section{domain IBITS IndexedBits} <>= )abbrev domain IBITS IndexedBits ++ Author: Stephen Watt and Michael Monagan ++ Date Created: ++ July 86 ++ Change History: ++ Oct 87 ++ Basic Operations: range ++ Related Constructors: ++ Keywords: indexed bits ++ Description: \spadtype{IndexedBits} is a domain to compactly represent ++ large quantities of Boolean data. IndexedBits(mn:Integer): BitAggregate() with -- temporaries until parser gets better Not: % -> % ++ Not(n) returns the bit-by-bit logical {\em Not} of n. Or : (%, %) -> % ++ Or(n,m) returns the bit-by-bit logical {\em Or} of ++ n and m. And: (%, %) -> % ++ And(n,m) returns the bit-by-bit logical {\em And} of ++ n and m. == add range: (%, Integer) -> Integer --++ range(j,i) returnes the range i of the boolean j. minIndex u == mn range(v, i) == i >= 0 and i < #v => i error "Index out of range" coerce(v):OutputForm == t:Character := char "1" f:Character := char "0" s := new(#v, space()$Character)$String for i in minIndex(s)..maxIndex(s) for j in mn.. repeat s.i := if v.j then t else f s::OutputForm new(n, b) == BVEC_-MAKE_-FULL(n,TRUTH_-TO_-BIT(b)$Lisp)$Lisp empty() == BVEC_-MAKE_-FULL(0,0)$Lisp copy v == BVEC_-COPY(v)$Lisp #v == BVEC_-SIZE(v)$Lisp v = u == BVEC_-EQUAL(v, u)$Lisp v < u == BVEC_-GREATER(u, v)$Lisp _and(u, v) == (#v=#u => BVEC_-AND(v,u)$Lisp; map("and",v,u)) _or(u, v) == (#v=#u => BVEC_-OR(v, u)$Lisp; map("or", v,u)) xor(v,u) == (#v=#u => BVEC_-XOR(v,u)$Lisp; map("xor",v,u)) setelt(v:%, i:Integer, f:Boolean) == BIT_-TO_-TRUTH(BVEC_-SETELT(v, range(v, i-mn), TRUTH_-TO_-BIT(f)$Lisp)$Lisp)$Lisp elt(v:%, i:Integer) == BIT_-TO_-TRUTH(BVEC_-ELT(v, range(v, i-mn))$Lisp)$Lisp Not v == BVEC_-NOT(v)$Lisp And(u, v) == (#v=#u => BVEC_-AND(v,u)$Lisp; map("and",v,u)) Or(u, v) == (#v=#u => BVEC_-OR(v, u)$Lisp; map("or", v,u)) @ \section{domain BITS Bits} <>= )abbrev domain BITS Bits ++ Author: Stephen M. Watt ++ Date Created: ++ Change History: ++ Basic Operations: And, Not, Or ++ Related Constructors: ++ Keywords: bits ++ Description: \spadtype{Bits} provides logical functions for Indexed Bits. Bits(): Exports == Implementation where Exports == BitAggregate() with bits: (NonNegativeInteger, Boolean) -> % ++ bits(n,b) creates bits with n values of b Implementation == IndexedBits(1) add bits(n,b) == new(n,b) @ \section{Kleene's Three-Valued Logic} <>= )abbrev domain KTVLOGIC KleeneTrivalentLogic ++ Author: Gabriel Dos Reis ++ Date Created: September 20, 2008 ++ Date Last Modified: September 20, 2008 ++ Description: ++ This domain implements Kleene's 3-valued propositional logic. KleeneTrivalentLogic(): Public == Private where Public == PropositionalLogic with false: % ++ the definite falsehood value unknown: % ++ the indefinite `unknown' true: % ++ the definite truth value _case: (%,[| false |]) -> Boolean ++ x case false holds if the value of `x' is `false' _case: (%,[| unknown |]) -> Boolean ++ x case unknown holds if the value of `x' is `unknown' _case: (%,[| true |]) -> Boolean ++ s case true holds if the value of `x' is `true'. Private == add Rep == Byte -- We need only 3 bits, in fact. false == per(0::NonNegativeInteger::Byte) unknown == per(1::NonNegativeInteger::Byte) true == per(2::Byte) x = y == rep x = rep y x case true == x = true x case false == x = false x case unknown == x = unknown not x == x case false => true x case unknown => unknown false x and y == x case false => false x case unknown => y case false => false unknown y x or y == x case false => y x case true => x y case true => y unknown implies(x,y) == x case false => true x case true => y y case true => true unknown equiv(x,y) == x case unknown => x x case true => y not y coerce(x: %): OutputForm == x case true => outputForm 'true x case false => outputForm 'false outputForm 'unknown @ \section{License} <>= --Copyright (c) 1991-2002, The Numerical Algorithms Group Ltd. --All rights reserved. --Copyright (C) 2007-2008, Gabriel Dos Reis. --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. @ <<*>>= <> <> <> <> <> <> <> <> <> @ \eject \begin{thebibliography}{99} \bibitem{1} nothing \end{thebibliography} \end{document}