Martin Baker wrote:
>
> Gaby,
>
> Its not clear to me how best to use your (undocumented) PropositionalFormula
> domain. Should I use it over Symbol so that the propositions are represented
> by symbols as below?
By definition propositional formula is build from atomic formulas
using logical connectives. Which kind of atomic formulas you
use depends on your needs. Symbols are good to represent variables,
but you may wish to use something more fancy like your typed
variables. But you may also represent formulas form differnet
theories, for example you may use comparisons between variables
as atomic formulas to handle orders. Or you may use equality
and inequality between polynomials to represent quantifier-free
part of ring theory. The point is that PropositionalFormula
domains imposes no interpretation on atomic formulas, it
only performs logical operations for which it needs to know
if two atomic formulas are equal or not. Of course, to take
advantage of more interesting atomic formulas you need to
add extra code, but the point is that it should be possible
reusing PropositionalFormula for what it can do. To get
the spirit Google for "SMT solvers" or Nelson-Oppen
(PropositionalFormula is a toy compared to serious SMT
solvers, but SMT solvers show that one can sucessfully
decuple propositional resoning for resonings specific
to given theory).
> Also its written using Kernel, what is the advantage of this?
Kernel-s are cached, so there is only one kernel with given
arguments. That makes testing equality faster. It
is easier to detect if formula changed (some simplifications
are applied as long as formula changes). Also, some
transformations if done naively would duplicate subformulas.
Due to recursion this can easily lead to exponential growth
of formula size. Caching of kernels means that some
subformulas are automatically shared, limiting possibility
of running out of memory and saving processing time.
> Martin
> ------------------------------------------------
> (ran in FriCAS using Waldeks translation)
>
> Type: PropositionalFormula(Symbol)
> (5) -> pq := p /\ q
> Internal Error
> The function /\ with signature hashcode is missing from domain
> PropositionalFormula(Symbol)
>
...
> (8) -> dual(pq)
> Function: ?=? : (%,%) -> Boolean is missing from domain:
> PropositionalFormula(Polynomial(Integer))
> Internal Error
> The function = with signature (Boolean)$$ is missing from domain
> PropositionalFormula(Polynomial (Integer))
...
> (8) -> simplify(conjunction(b := true()$PROP,pq))
> Function: ?=? : (%,%) -> Boolean is missing from domain:
> PropositionalFormula(Symbol)
> Internal Error
> The function = with signature (Boolean)$$ is missing from domain
> PropositionalFormula(Symbol)
>
Below is new version with this problem fixed. It uses changed
Product, so you need FriCAS from svn to compile it.
)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
lnot: % -> %
++ \spad{lnot x} returns the complement or negation of \spad{x}.
-- land: (%,%) -> %
-- ++ \spad{x land y} returns the conjunction of \spad{x} and \spad{y}.
-- lor: (%,%) -> %
-- ++ \spad{x lor y} returns the disjunction of \spad{x} and \spad{y}.
)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'.
)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) with
isAtom : % -> Union(T, "failed")
++ \spad{isAtom f} returns a value \spad{v} such that
++ \spad{v case T} holds if the formula \spad{f} is a term.
isNot : % -> Union(%, "failed")
++ \spad{isNot f} returns a value \spad{v} such that
++ \spad{v case %} holds if the formula \spad{f} is a negation.
isAnd : % -> Union(Product(%,%), "failed")
++ \spad{isAnd f} returns a value \spad{v} such that
++ \spad{v case Product(%,%)} holds if the formula \spad{f}
++ is a conjunction formula.
isOr : % -> Union(Product(%,%), "failed")
++ \spad{isOr f} returns a value \spad{v} such that
++ \spad{v case Product(%,%)} holds if the formula \spad{f}
++ is a disjunction formula.
isImplies : % -> Union(Product(%,%), "failed")
++ \spad{isImplies f} returns a value \spad{v} such that
++ \spad{v case Product(%,%)} holds if the formula \spad{f}
++ is an implication formula.
isEquiv : % -> Union(Product(%,%), "failed")
++ \spad{isEquiv f} returns a value \spad{v} such that
++ \spad{v case Product(%,%)} 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}.
coerce: T -> %
Private == add
Rep == Union(T, Kernel %)
import Kernel %
import BasicOperator
import KernelFunctions2(Identifier,%)
import List %
rep(x:%):Rep == x pretend Rep
per(x:Rep):% == x pretend %
-- 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
opnot := operator(NOT, 1)
opand := operator(AND, 2)
opor := operator(OR, 2)
opimp := operator(IMP, 2)
opeqv := operator(EQV, 2)
opfalse := operator(FALSE, 0)
optrue := operator(TRUE, 0)
false() == per kernel(opfalse, [], 1)
true() == per kernel(optrue, [], 1)
lnot p ==
per kernel(opnot, [p], 1 + level p)
conjunction(p,q) ==
per kernel(opand, [p, q], 1 + max(level p, level q))
_/_\(p, q) == conjunction(p,q)
disjunction(p,q) ==
per kernel(opor, [p, q], 1 + max(level p, level q))
_\_/(p, q) == disjunction(p,q)
implies(p,q) ==
per kernel(opimp, [p, q], 1 + max(level p, level q))
equiv(p,q) ==
per kernel(opeqv, [p, q], 1 + max(level p, level q))
isAtom f ==
f' := rep f
f' case T => f'::T
"failed"
isNot f ==
f' := rep f
f' case Kernel(%) and is?(f', NOT) => first argument f'
"failed"
p = q ==
p' := rep p
q' := rep q
p' case T =>
q' case T => p'::T = q'::T
false
q' case T => false
p'::Kernel(%) = q'::Kernel(%)
isBinaryOperator(f: Kernel %, op: Symbol): Union(Product(%, %), "failed") ==
not is?(f, op) => "failed"
args := argument f
[first args, second args]
isAnd f ==
f' := rep f
f' case Kernel % => isBinaryOperator(f', AND)
"failed"
isOr f ==
f' := rep f
f' case Kernel % => isBinaryOperator(f', OR)
"failed"
isImplies f ==
f' := rep f
f' case Kernel % => isBinaryOperator(f', IMP)
"failed"
isEquiv f ==
f' := rep f
f' case Kernel % => isBinaryOperator(f', EQV)
"failed"
-- 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
is?(p', TRUE) or is?(p', FALSE) => operator(p')::OutputForm
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 ==
(p1 := isNot p) case % =>
elt(outputForm '_not, [notFormula (p1::%)])$OutputForm
primaryFormula p
andFormula(f: %): OutputForm ==
(f1 := isAnd f) case Product(%,%) =>
p := f1::Product(%,%)
-- ??? 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
notFormula f
orFormula(f: %): OutputForm ==
(f1 := isOr f) case Product(%,%) =>
p := f1::Product(%,%)
-- ??? 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
andFormula f
formula f ==
-- Note: this should be equivFormula, but see the explanation above.
orFormula f
)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
PF ==> PropositionalFormula T
import Product(PF, PF)
dual f ==
f = true()$PF => false()$PF
f = false()$PF => true()$PF
isAtom f case T => f
(f1 := isNot f) case PF => lnot(dual f1)
(f2 := isAnd f) case Product(PF, PF) =>
disjunction(dual first f2, dual second f2)
(f2 := isOr f) case Product(PF, PF) =>
conjunction(dual first f2, dual second f2)
error "formula contains `equiv' or `implies'"
atoms f ==
(t := isAtom f) case T => set([t])
(f1 := isNot f) case PF => atoms f1
(f2 := isAnd f) case Product(PF, PF) =>
union(atoms first f2, atoms second f2)
(f2 := isOr f) case Product(PF, PF) =>
union(atoms first f2, atoms second f2)
empty()$Set(T)
-- one-step simplification helper function
simplifyOneStep(f: PF): PF ==
(f1 := isNot f) case PF =>
f1 = true$PF => false$PF
f1 = false$PF => true$PF
(f1' := isNot f1) case PF => f1' -- assume classical logic
f
(f2 := isAnd f) case Product(PF,PF) =>
first f2 = false$PF or second f2 = false$PF => false$PF
first f2 = true$PF => second f2
second f2 = true$PF => first f2
f
(f2 := isOr f) case Product(PF,PF) =>
first f2 = false$PF => second f2
second f2 = false$PF => first f2
first f2 = true$PF or second f2 = true$PF => true$PF
f
(f2 := isImplies f) case Product(PF,PF) =>
first f2 = false$PF or second f2 = true$PF => true$PF
first f2 = true$PF => second f2
second f2 = false$PF => lnot first f2
f
(f2 := isEquiv f) case Product(PF,PF) =>
first f2 = true$PF => second f2
second f2 = true$PF => first f2
first f2 = false$PF => lnot second f2
second f2 = false$PF => lnot first f2
f
f
simplify f ==
(f1 := isNot f) case PF => simplifyOneStep(lnot simplify f1)
(f2 := isAnd f) case Product(PF,PF) =>
simplifyOneStep(conjunction(simplify first f2,
simplify second f2))
(f2 := isOr f) case Product(PF,PF) =>
simplifyOneStep(disjunction(simplify first f2,
simplify second f2))
(f2 := isImplies f) case Product(PF,PF) =>
simplifyOneStep(implies(simplify first f2,
simplify second f2))
(f2 := isEquiv f) case Product(PF,PF) =>
simplifyOneStep(equiv(simplify first f2,
simplify second f2))
f
)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 => lnot map(f,f1)
(f2 := isAnd x) case Product(FS,FS) =>
conjunction(map(f, first f2), map(f, second f2))
(f2 := isOr x) case Product(FS,FS) =>
disjunction(map(f, first f2), map(f, second f2))
(f2 := isImplies x) case Product(FS,FS) =>
implies(map(f, first f2), map(f, second f2))
(f2 := isEquiv x) case Product(FS,FS) =>
equiv(map(f, first f2), map(f, second f2))
error "invalid propositional formula"
--
Waldek Hebisch
[email protected]
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en.
