diff options
| -rw-r--r-- | src/ChangeLog | 11 | ||||
| -rw-r--r-- | src/algebra/Makefile.am | 2 | ||||
| -rw-r--r-- | src/algebra/boolean.spad.pamphlet | 481 | ||||
| -rw-r--r-- | src/algebra/cycles.spad.pamphlet | 26 | ||||
| -rw-r--r-- | src/algebra/logic.spad.pamphlet | 546 |
5 files changed, 569 insertions, 497 deletions
diff --git a/src/ChangeLog b/src/ChangeLog index ee3f4f00..b1703f4c 100644 --- a/src/ChangeLog +++ b/src/ChangeLog @@ -1,5 +1,16 @@ 2013-05-25 Gabriel Dos Reis <gdr@integrable-solutions.net> + * algebra/logic.spad.pamphlet: New file. + * algebra/boolean.spad.pamphlet (Logic): Move there. + (BooleanLogic): Likewise. + (PropositionalLogic): Likewise. + (PropositionalFormula): Likewise. + (PropositionalFormulaFunctions1): Likewise. + (PropositionalFormulaFunctions2): Likewise. + (KleeneTrivalentLogic): Likewise. + +2013-05-25 Gabriel Dos Reis <gdr@integrable-solutions.net> + * algebra/cycles.spad.pamphlet (CycleIndicators) [spol]: Rename from nniBump. Fix thinko. diff --git a/src/algebra/Makefile.am b/src/algebra/Makefile.am index 536cbed8..ae00743b 100644 --- a/src/algebra/Makefile.am +++ b/src/algebra/Makefile.am @@ -1091,7 +1091,7 @@ SPADFILES= \ $(OUTSRC)/lie.spad $(OUTSRC)/limitps.spad $(OUTSRC)/lindep.spad \ $(OUTSRC)/lingrob.spad $(OUTSRC)/liouv.spad $(OUTSRC)/listgcd.spad \ $(OUTSRC)/list.spad $(OUTSRC)/lmdict.spad $(OUTSRC)/lodof.spad \ - $(OUTSRC)/lodop.spad $(OUTSRC)/lodo.spad \ + $(OUTSRC)/lodop.spad $(OUTSRC)/lodo.spad $(OUTSRC)/logic.spad \ $(OUTSRC)/manip.spad $(OUTSRC)/mappkg.spad $(OUTSRC)/matcat.spad \ $(OUTSRC)/matfuns.spad $(OUTSRC)/mathml.spad \ $(OUTSRC)/matrix.spad $(OUTSRC)/matstor.spad \ 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>>= diff --git a/src/algebra/cycles.spad.pamphlet b/src/algebra/cycles.spad.pamphlet index 7b1b7c0d..0a92b83a 100644 --- a/src/algebra/cycles.spad.pamphlet +++ b/src/algebra/cycles.spad.pamphlet @@ -54,15 +54,15 @@ CycleIndicators: Exports == Implementation where ++\spad{alternating n} is the cycle index of the ++ alternating group of degree n. - cyclic: PI -> SPOL RN --cyclic group + cyclic: NNI -> SPOL RN --cyclic group ++\spad{cyclic n} is the cycle index of the ++ cyclic group of degree n. - dihedral: PI -> SPOL RN --dihedral group + dihedral: NNI -> SPOL RN --dihedral group ++\spad{dihedral n} is the cycle index of the ++ dihedral group of degree n. - graphs: PI -> SPOL RN + graphs: NNI -> SPOL RN ++\spad{graphs n} is the cycle index of the group induced on ++ the edges of a graph by applying the symmetric function to the ++ n nodes. @@ -100,24 +100,20 @@ CycleIndicators: Exports == Implementation where trm: PTN -> SPOL RN trm pt == monomial(inv(pdct(pt) :: RN),pt) - list: Stream PTN -> L PTN - list st == entries complete st - complete i == i=0 => 1 - +/[trm pt for pt in list partitions i] - - - even?: PTN -> B - even? p == even?( #([i for i in parts p | even? i])) + +/[trm pt for pt in entries partitions i] + + even?: L I -> B + even? li == even?( #([i for i in li | even? i])) alternating i == - 2 * _+/[trm p for p in list partitions i | even? p] + 2 * _+/[trm p for p in entries partitions i | even? p] elementary i == i=0 => 1 - +/[(spol := trm pt; even? pt => spol; -spol) - for pt in list partitions i] + +/[(spol := trm partition pt; even? pt => spol; -spol) + for pt in entries partitions i] divisors: I -> L I divisors n == @@ -161,7 +157,7 @@ CycleIndicators: Exports == Implementation where prod := c * prod2 * prod xx * prod - graphs n == +/[trm2 p for p in list(partitions n)] + graphs n == +/[trm2 p for p in entries partitions n] cupp: (PTN,SPOL RN) -> SPOL RN cupp(pt,spol) == diff --git a/src/algebra/logic.spad.pamphlet b/src/algebra/logic.spad.pamphlet new file mode 100644 index 00000000..895051f2 --- /dev/null +++ b/src/algebra/logic.spad.pamphlet @@ -0,0 +1,546 @@ +\documentclass{article} +\usepackage{open-axiom} + +\title{src/algebra logic.spad} +\author{Gabriel Dos~Reis} + +\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 + ~: % -> % + ++ \spad{~x} returns the logical complement of \spad{x}. + /\: (%, %) -> % + ++ \spad {x/\y} returns the logical `meet', e.g. conjunction, of + ++ \spad{x} and \spad{y}. + \/: (%, %) -> % + ++ \spad{x\/y} returns the logical `join', e.g. disjunction, or + ++ \spad{x} and \spad{y}. + add + x \/ y == ~(~x /\ ~y) + +@ + +\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: % + ++ \spad{true} is a logical constant. + false: % + ++ \spad{false} is a logical constant. + implies: (%,%) -> % + ++ \spad{implies(p,q)} returns the logical implication of `q' by `p'. + equiv: (%,%) -> % + ++ \spad{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{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>>= +--Copyright (C) 1991-2002, The Numerical Algorithms Group Ltd. +--All rights reserved. +--Copyright (C) 2007-2013, 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>> + +<<category LOGIC Logic>> +<<category BOOLE BooleanLogic>> + +<<category PROPLOG PropositionalLogic>> +<<domain PROPFRML PropositionalFormula>> +<<package PROPFUN1 PropositionalFormulaFunctions1>> +<<package PROPFUN2 PropositionalFormulaFunctions2>> + +<<domain KTVLOGIC KleeneTrivalentLogic>> + +@ + + +\eject +\begin{thebibliography}{99} +\bibitem{1} nothing +\end{thebibliography} +\end{document} + |