aboutsummaryrefslogtreecommitdiff
path: root/src/algebra/boolean.spad.pamphlet
diff options
context:
space:
mode:
Diffstat (limited to 'src/algebra/boolean.spad.pamphlet')
-rw-r--r--src/algebra/boolean.spad.pamphlet481
1 files changed, 0 insertions, 481 deletions
diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet
index dcdf0562..3ad4b2ff 100644
--- a/src/algebra/boolean.spad.pamphlet
+++ b/src/algebra/boolean.spad.pamphlet
@@ -12,386 +12,6 @@
\tableofcontents
\eject
-\section{Categories an domains for logic}
-
-<<category BOOLE BooleanLogic>>=
-)abbrev category BOOLE BooleanLogic
-++ Author: Gabriel Dos Reis
-++ Date Created: April 04, 2010
-++ Date Last Modified: April 04, 2010
-++ Description:
-++ This is the category of Boolean logic structures.
-BooleanLogic(): Category == Logic with
- not: % -> %
- ++ \spad{not x} returns the complement or negation of \spad{x}.
- and: (%,%) -> %
- ++ \spad{x and y} returns the conjunction of \spad{x} and \spad{y}.
- or: (%,%) -> %
- ++ \spad{x or y} returns the disjunction of \spad{x} and \spad{y}.
- add
- not x == ~ x
- x and y == x /\ y
- x or y == x \/ y
-@
-
-<<category PROPLOG PropositionalLogic>>=
-)abbrev category PROPLOG PropositionalLogic
-++ Author: Gabriel Dos Reis
-++ Date Created: Januray 14, 2008
-++ Date Last Modified: May 27, 2009
-++ Description: This category declares the connectives of
-++ Propositional Logic.
-PropositionalLogic(): Category == Join(BooleanLogic,SetCategory) with
- true: %
- ++ true is a logical constant.
- false: %
- ++ false is a logical constant.
- 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: February, 2011
-++ Description: This domain implements propositional formula build
-++ over a term domain, that itself belongs to PropositionalLogic
-PropositionalFormula(T: SetCategory): Public == Private where
- Public == Join(PropositionalLogic, CoercibleFrom T) with
- isAtom : % -> Maybe T
- ++ \spad{isAtom f} returns a value \spad{v} such that
- ++ \spad{v case T} holds if the formula \spad{f} is a term.
-
- isNot : % -> Maybe %
- ++ \spad{isNot f} returns a value \spad{v} such that
- ++ \spad{v case %} holds if the formula \spad{f} is a negation.
-
- isAnd : % -> Maybe Pair(%,%)
- ++ \spad{isAnd f} returns a value \spad{v} such that
- ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
- ++ is a conjunction formula.
-
- isOr : % -> Maybe Pair(%,%)
- ++ \spad{isOr f} returns a value \spad{v} such that
- ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
- ++ is a disjunction formula.
-
- isImplies : % -> Maybe Pair(%,%)
- ++ \spad{isImplies f} returns a value \spad{v} such that
- ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
- ++ is an implication formula.
-
- isEquiv : % -> Maybe Pair(%,%)
- ++ \spad{isEquiv f} returns a value \spad{v} such that
- ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
- ++ is an equivalence formula.
-
- conjunction: (%,%) -> %
- ++ \spad{conjunction(p,q)} returns a formula denoting the
- ++ conjunction of \spad{p} and \spad{q}.
-
- disjunction: (%,%) -> %
- ++ \spad{disjunction(p,q)} returns a formula denoting the
- ++ disjunction of \spad{p} and \spad{q}.
-
- Private == add
- Rep == Union(T, Kernel %)
- import Kernel %
- import BasicOperator
- import KernelFunctions2(Identifier,%)
- import List %
-
- -- Local names for proposition logical operators
- macro FALSE == '%false
- macro TRUE == '%true
- macro NOT == '%not
- macro AND == '%and
- macro OR == '%or
- macro IMP == '%implies
- macro EQV == '%equiv
-
- -- Return the nesting level of a formula
- level(f: %): NonNegativeInteger ==
- f' := rep f
- f' case T => 0
- height f'
-
- -- A term is a formula
- coerce(t: T): % ==
- per t
-
- false == per constantKernel FALSE
- true == per constantKernel TRUE
-
- ~ p ==
- per kernel(operator(NOT, 1::Arity), [p], 1 + level p)
-
- conjunction(p,q) ==
- per kernel(operator(AND, 2), [p, q], 1 + max(level p, level q))
-
- p /\ q == conjunction(p,q)
-
- disjunction(p,q) ==
- per kernel(operator(OR, 2), [p, q], 1 + max(level p, level q))
-
- p \/ q == disjunction(p,q)
-
- implies(p,q) ==
- per kernel(operator(IMP, 2), [p, q], 1 + max(level p, level q))
-
- equiv(p,q) ==
- per kernel(operator(EQV, 2), [p, q], 1 + max(level p, level q))
-
- isAtom f ==
- f' := rep f
- f' case T => just(f'@T)
- nothing
-
- isNot f ==
- f' := rep f
- f' case Kernel(%) and is?(f', NOT) => just(first argument f')
- nothing
-
- isBinaryOperator(f: Kernel %, op: Symbol): Maybe Pair(%, %) ==
- not is?(f, op) => nothing
- args := argument f
- just pair(first args, second args)
-
- isAnd f ==
- f' := rep f
- f' case Kernel % => isBinaryOperator(f', AND)
- nothing
-
- isOr f ==
- f' := rep f
- f' case Kernel % => isBinaryOperator(f', OR)
- nothing
-
- isImplies f ==
- f' := rep f
- f' case Kernel % => isBinaryOperator(f', IMP)
- nothing
-
-
- isEquiv f ==
- f' := rep f
- f' case Kernel % => isBinaryOperator(f', EQV)
- nothing
-
- -- 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 ==
- p' := rep p
- p' case T => p'@T::OutputForm
- case constantIfCan p' is
- c@Identifier => c::OutputForm
- otherwise =>
- is?(p', IMP) or is?(p', EQV) =>
- args := argument p'
- elt(operator(p')::OutputForm,
- [formula first args, formula second args])$OutputForm
- paren(formula p)$OutputForm
-
- notFormula(p: %): OutputForm ==
- case isNot p is
- f@% => elt(outputForm 'not, [notFormula f])$OutputForm
- otherwise => primaryFormula p
-
- andFormula(f: %): OutputForm ==
- case isAnd f is
- p@Pair(%,%) =>
- -- ??? idealy, we should be using `and$OutputForm' but
- -- ??? a bug in the compiler currently prevents that.
- infix(outputForm 'and, notFormula first p,
- andFormula second p)$OutputForm
- otherwise => notFormula f
-
- orFormula(f: %): OutputForm ==
- case isOr f is
- p@Pair(%,%) =>
- -- ??? idealy, we should be using `or$OutputForm' but
- -- ??? a bug in the compiler currently prevents that.
- infix(outputForm 'or, andFormula first p,
- orFormula second p)$OutputForm
- otherwise => andFormula f
-
- formula f ==
- -- Note: this should be equivFormula, but see the explanation above.
- orFormula f
-
-@
-
-<<package PROPFUN1 PropositionalFormulaFunctions1>>=
-)abbrev package PROPFUN1 PropositionalFormulaFunctions1
-++ Author: Gabriel Dos Reis
-++ Date Created: April 03, 2010
-++ Date Last Modified: April 03, 2010
-++ Description:
-++ This package collects unary functions operating on propositional
-++ formulae.
-PropositionalFormulaFunctions1(T): Public == Private where
- T: SetCategory
- Public == Type with
- dual: PropositionalFormula T -> PropositionalFormula T
- ++ \spad{dual f} returns the dual of the proposition \spad{f}.
- atoms: PropositionalFormula T -> Set T
- ++ \spad{atoms f} ++ returns the set of atoms appearing in
- ++ the formula \spad{f}.
- simplify: PropositionalFormula T -> PropositionalFormula T
- ++ \spad{simplify f} returns a formula logically equivalent
- ++ to \spad{f} where obvious tautologies have been removed.
- Private == add
- macro F == PropositionalFormula T
- inline Pair(F,F)
-
- dual f ==
- f = true$F => false$F
- f = false$F => true$F
- isAtom f case T => f
- (f1 := isNot f) case F => not dual f1
- (f2 := isAnd f) case Pair(F,F) =>
- disjunction(dual first f2, dual second f2)
- (f2 := isOr f) case Pair(F,F) =>
- conjunction(dual first f2, dual second f2)
- error "formula contains `equiv' or `implies'"
-
- atoms f ==
- (t := isAtom f) case T => { t }
- (f1 := isNot f) case F => atoms f1
- (f2 := isAnd f) case Pair(F,F) =>
- union(atoms first f2, atoms second f2)
- (f2 := isOr f) case Pair(F,F) =>
- union(atoms first f2, atoms second f2)
- empty()$Set(T)
-
- -- one-step simplification helper function
- simplifyOneStep(f: F): F ==
- (f1 := isNot f) case F =>
- f1 = true$F => false$F
- f1 = false$F => true$F
- (f1' := isNot f1) case F => f1' -- assume classical logic
- f
- (f2 := isAnd f) case Pair(F,F) =>
- first f2 = false$F or second f2 = false$F => false$F
- first f2 = true$F => second f2
- second f2 = true$F => first f2
- f
- (f2 := isOr f) case Pair(F,F) =>
- first f2 = false$F => second f2
- second f2 = false$F => first f2
- first f2 = true$F or second f2 = true$F => true$F
- f
- (f2 := isImplies f) case Pair(F,F) =>
- first f2 = false$F or second f2 = true$F => true$F
- first f2 = true$F => second f2
- second f2 = false$F => not first f2
- f
- (f2 := isEquiv f) case Pair(F,F) =>
- first f2 = true$F => second f2
- second f2 = true$F => first f2
- first f2 = false$F => not second f2
- second f2 = false$F => not first f2
- f
- f
-
- simplify f ==
- (f1 := isNot f) case F => simplifyOneStep(not simplify f1)
- (f2 := isAnd f) case Pair(F,F) =>
- simplifyOneStep(conjunction(simplify first f2, simplify second f2))
- (f2 := isOr f) case Pair(F,F) =>
- simplifyOneStep(disjunction(simplify first f2, simplify second f2))
- (f2 := isImplies f) case Pair(F,F) =>
- simplifyOneStep(implies(simplify first f2, simplify second f2))
- (f2 := isEquiv f) case Pair(F,F) =>
- simplifyOneStep(equiv(simplify first f2, simplify second f2))
- f
-@
-
-<<package PROPFUN2 PropositionalFormulaFunctions2>>=
-)abbrev package PROPFUN2 PropositionalFormulaFunctions2
-++ Author: Gabriel Dos Reis
-++ Date Created: April 03, 2010
-++ Date Last Modified: April 03, 2010
-++ Description:
-++ This package collects binary functions operating on propositional
-++ formulae.
-PropositionalFormulaFunctions2(S,T): Public == Private where
- S: SetCategory
- T: SetCategory
- Public == Type with
- map: (S -> T, PropositionalFormula S) -> PropositionalFormula T
- ++ \spad{map(f,x)} returns a propositional formula where
- ++ all atoms in \spad{x} have been replaced by the result
- ++ of applying the function \spad{f} to them.
- Private == add
- macro FS == PropositionalFormula S
- macro FT == PropositionalFormula T
- map(f,x) ==
- x = true$FS => true$FT
- x = false$FS => false$FT
- (t := isAtom x) case S => f(t)::FT
- (f1 := isNot x) case FS => not map(f,f1)
- (f2 := isAnd x) case Pair(FS,FS) =>
- conjunction(map(f,first f2), map(f,second f2))
- (f2 := isOr x) case Pair(FS,FS) =>
- disjunction(map(f,first f2), map(f,second f2))
- (f2 := isImplies x) case Pair(FS,FS) =>
- implies(map(f,first f2), map(f,second f2))
- (f2 := isEquiv x) case Pair(FS,FS) =>
- equiv(map(f,first f2), map(f,second f2))
- error "invalid propositional formula"
-
-@
-
\section{domain REF Reference}
<<domain REF Reference>>=
)abbrev domain REF Reference
@@ -429,32 +49,6 @@ Reference(S:Type): SetCategory with
@
-\section{category LOGIC Logic}
-
-<<category LOGIC Logic>>=
-)abbrev category LOGIC Logic
-++ Author:
-++ Date Created:
-++ Date Last Changed: May 27, 2009
-++ Basic Operations: ~, /\, \/
-++ Related Constructors:
-++ Keywords: boolean
-++ Description:
-++ `Logic' provides the basic operations for lattices,
-++ e.g., boolean algebra.
-
-
-Logic: Category == Type 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
@@ -605,81 +199,6 @@ Bits(): Exports == Implementation where
@
-
-\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: January 14, 2012
-++ Description:
-++ This domain implements Kleene's 3-valued propositional logic.
-KleeneTrivalentLogic(): Public == Private where
- Public == Join(PropositionalLogic,Finite) with
- unknown: % ++ the indefinite `unknown'
- 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 == Maybe Boolean add
- false == per just(false@Boolean)
- unknown == per nothing
- true == per just(true@Boolean)
- 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 ==
- case rep x is
- y@Boolean => y::OutputForm
- otherwise => outputForm 'unknown
-
- size() == 3
-
- index n ==
- n > 3 => error "index: argument out of bound"
- n = 1 => false
- n = 2 => unknown
- true
-
- lookup x ==
- x = false => 1
- x = unknown => 2
- 3
-@
-
\section{License}
<<license>>=