diff options
Diffstat (limited to 'src/algebra/boolean.spad.pamphlet')
| -rw-r--r-- | src/algebra/boolean.spad.pamphlet | 153 |
1 files changed, 107 insertions, 46 deletions
diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet index ab33ba62..b9cb64cb 100644 --- a/src/algebra/boolean.spad.pamphlet +++ b/src/algebra/boolean.spad.pamphlet @@ -17,10 +17,10 @@ )abbrev category PROPLOG PropositionalLogic ++ Author: Gabriel Dos Reis ++ Date Created: Januray 14, 2008 -++ Date Last Modified: January 14, 2008 +++ Date Last Modified: September 20, 2008 ++ Description: This category declares the connectives of ++ Propositional Logic. -PropositionalLogic(): Category == with +PropositionalLogic(): Category == SetCategory with "not": % -> % ++ not p returns the logical negation of `p'. "and": (%, %) -> % @@ -43,7 +43,6 @@ PropositionalLogic(): Category == with ++ Description: This domain implements propositional formula build ++ over a term domain, that itself belongs to PropositionalLogic PropositionalFormula(T: PropositionalLogic): PropositionalLogic with - if T has CoercibleTo OutputForm then CoercibleTo OutputForm coerce: T -> % ++ coerce(t) turns the term `t' into a propositional formula coerce: Symbol -> % @@ -236,47 +235,46 @@ PropositionalFormula(T: PropositionalLogic): PropositionalLogic with -- Term -- implies(Formula, Formula) -- equiv(Formula, Formula) - if T has CoercibleTo OutputForm then - 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 + 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 @ @@ -501,9 +499,70 @@ Bits(): Exports == Implementation where 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: % + unknown: % + true: % + _case: (%,[| false |]) -> Boolean + _case: (%,[| unknown |]) -> Boolean + _case: (%,[| true |]) -> Boolean + 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. +--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 @@ -518,7 +577,7 @@ Bits(): Exports == Implementation where -- the documentation and/or other materials provided with the -- distribution. -- --- - Neither the name of The Numerical ALgorithms Group Ltd. nor the +-- - 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. -- @@ -544,6 +603,8 @@ Bits(): Exports == Implementation where <<domain BITS Bits>> <<category PROPLOG PropositionalLogic>> <<domain PROPFRML PropositionalFormula>> +<<domain KTVLOGIC KleeneTrivalentLogic>> + @ \eject \begin{thebibliography}{99} |