path: root/src/algebra/boolean.spad.pamphlet

\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('ref::OutputForm, [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
    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}
<<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::Byte)
    unknown == per(1::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}