diff options
Diffstat (limited to 'src/algebra/boolean.spad.pamphlet')
| -rw-r--r-- | src/algebra/boolean.spad.pamphlet | 481 |
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>>= |