\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}
<<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}
<<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}
<<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}
<<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}
<<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
nt: % -> %
test a == a
nt b == (b => false; true)
true == 'T pretend %
false == NIL$Lisp
sample() == true
not b == NOT(b)$Lisp
_~ b == (b => false; true)
_and(a, b) == AND(a,b)$Lisp
_/_\(a, b) == (a => b; false)
_or(a, b) == OR(a,b)$Lisp
_\_/(a, b) == (a => true; b)
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 ==
x => convert("true"::Symbol)
convert("false"::Symbol)
coerce(x:%):OutputForm ==
x => message "true"
message "false"
@
\section{domain IBITS IndexedBits}
<<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}
<<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}
<<domain KTVLOGIC KleeneTrivalentLogic>>=
)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}
<<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.
@
<<*>>=
<<license>>
<<domain REF Reference>>
<<category LOGIC Logic>>
<<domain BOOLEAN Boolean>>
<<domain IBITS IndexedBits>>
<<domain BITS Bits>>
<<category PROPLOG PropositionalLogic>>
<<domain PROPFRML PropositionalFormula>>
<<domain KTVLOGIC KleeneTrivalentLogic>>
@
\eject
\begin{thebibliography}{99}
\bibitem{1} nothing
\end{thebibliography}
\end{document}