Martin Baker wrote:
>
> So since operator is defined like this:
>
> TermAlgebraOperator(S: SetCategory): Public == Private where
> Public == OperatorCategory S with
> operator: (S,Arity) -> %
>
> then we need a SetCategory, the nearest that I can find in src/interp/lisp-
> backend.boot is this:
As Gaby wrote, you are trying to translate too much. Below is quick
translation of what I believe is relevant (compiles in FriCAS 1.1.4).
Note1: AFAICS OpenAxiom original in coercion to OutputForm is
missing cases for false and true, which leads to infinite recursion.
I added them to translation.
Note2: I have no idea if/how the construct:
false == per constantKernel FALSE
true == per constantKernel TRUE
works in OpenAxiom. Instead I represent true and false as 0 argument
operators.
Note3: FriCAS instead of Pair has Product domain, I did relevant
renamings.
Note4: Because FriCAS parser performs transformations of 'not',
'and' and 'or' they are not usable as functions names. I replaced
them by 'lnot', 'land' and 'lor'.
)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))
land(p, q) == conjunction(p,q)
disjunction(p,q) ==
per kernel(opand, [p, q], 1 + max(level p, level q))
lor(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"
isBinaryOperator(f: Kernel %, op: Symbol): Union(Product(%, %), "failed") ==
not is?(f, op) => "failed"
args := argument f
makeprod(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 selectfirst p,
andFormula selectsecond 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 selectfirst p,
orFormula selectsecond 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 selectfirst f2, dual selectsecond f2)
(f2 := isOr f) case Product(PF, PF) =>
conjunction(dual selectfirst f2, dual selectsecond 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 selectfirst f2, atoms selectsecond f2)
(f2 := isOr f) case Product(PF, PF) =>
union(atoms selectfirst f2, atoms selectsecond 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) =>
selectfirst f2 = false$PF or selectsecond f2 = false$PF => false$PF
selectfirst f2 = true$PF => selectsecond f2
selectsecond f2 = true$PF => selectfirst f2
f
(f2 := isOr f) case Product(PF,PF) =>
selectfirst f2 = false$PF => selectsecond f2
selectsecond f2 = false$PF => selectfirst f2
selectfirst f2 = true$PF or selectsecond f2 = true$PF => true$PF
f
(f2 := isImplies f) case Product(PF,PF) =>
selectfirst f2 = false$PF or selectsecond f2 = true$PF => true$PF
selectfirst f2 = true$PF => selectsecond f2
selectsecond f2 = false$PF => lnot selectfirst f2
f
(f2 := isEquiv f) case Product(PF,PF) =>
selectfirst f2 = true$PF => selectsecond f2
selectsecond f2 = true$PF => selectfirst f2
selectfirst f2 = false$PF => lnot selectsecond f2
selectsecond f2 = false$PF => lnot selectfirst f2
f
f
simplify f ==
(f1 := isNot f) case PF => simplifyOneStep(lnot simplify f1)
(f2 := isAnd f) case Product(PF,PF) =>
simplifyOneStep(conjunction(simplify selectfirst f2,
simplify selectsecond f2))
(f2 := isOr f) case Product(PF,PF) =>
simplifyOneStep(disjunction(simplify selectfirst f2,
simplify selectsecond f2))
(f2 := isImplies f) case Product(PF,PF) =>
simplifyOneStep(implies(simplify selectfirst f2,
simplify selectsecond f2))
(f2 := isEquiv f) case Product(PF,PF) =>
simplifyOneStep(equiv(simplify selectfirst f2,
simplify selectsecond 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, selectfirst f2), map(f, selectsecond f2))
(f2 := isOr x) case Product(FS,FS) =>
disjunction(map(f, selectfirst f2), map(f, selectsecond f2))
(f2 := isImplies x) case Product(FS,FS) =>
implies(map(f, selectfirst f2), map(f, selectsecond f2))
(f2 := isEquiv x) case Product(FS,FS) =>
equiv(map(f, selectfirst f2), map(f, selectsecond f2))
error "invalid propositional formula"
--
Waldek Hebisch
hebi...@math.uni.wroc.pl
------------------------------------------------------------------------------
All the data continuously generated in your IT infrastructure contains a
definitive record of customers, application performance, security
threats, fraudulent activity and more. Splunk takes this data and makes
sense of it. Business sense. IT sense. Common sense.
http://p.sf.net/sfu/splunk-d2d-oct
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
