expressions and computation
Martin Baker
> - You implement a bunch of "expression like" domains. Have you checked
> if existing domains have needed functionality? One obvious alternative
> is to base you implementation on Kernel. Another is to use
> SEexpression as representaion.
I've been thinking about this and I agree that the computation domains
are
"expression like" .... sort of .... but ....
it seems that an expression would be in some algebra, for instance
perhaps there could be an expression where the symbols are elements of
a group, or a boolean algebra, or even a mixture of algebras?
So if lambda-calculus, combinators and intuitionistic logic are like
expressions then, what is the algebra that they are expressions in?
For instance imagine I had an algebra (don't take this very loose
pseudo-code laterally):
myAlgebra(baseAlgebra)....
.... with
e:Record(baseAlgeba,baseAlgeba) -> % -- constructor
m:(%,%) -> % -- binary op
.... ==>
Rep:=Record(A,B)
Then I could have some expression manipulator for that algebra:
myExpression()....
.... with
e:% -> Symbol -- code to read out a given expression
m:% -> Record(%,%)
eval:% -> myAlgebra -- apply myAlgebra recursively to get single
term
... ==>
Rep:=Union(e:Symbol,m:Record(%,%))
But I can't see a way to define lambda-calculus, combinators or
intuitionistic logic in this sort of way? Somehow they seem to need to
be defined in terms of a inductively defined co-datatype like this:
Rep:=Union(e:base,m:Record(%,%))
rather than a datatype like this:
Rep:=Record(A,B)
I am coming at this in abstract terms here, but in practical terms I
haven't yet seen a practical reason to use the domains you mention,
for instance I haven't yet noticed a need for caching of terms, but
that may change?
However I do like the idea that when the compiler compiles an algebra
like myAlgebra then why not allow it to generate expression
manipulator code for the algebra at the same time?
Martin
Bill Page
On Fri, Sep 16, 2011 at 11:22 AM, Martin Baker wrote:
> On Wednesday 08 Jun 2011 17:51:19 Waldek Hebisch wrote:
>> - You implement a bunch of "expression like" domains. Have you
>> checked if existing domains have needed functionality? One
>> obvious alternative is to base you implementation on Kernel.
>> Another is to use SEexpression as representation.
>
> I've been thinking about this and I agree that the computation
> domains are "expression like" .... sort of .... but ....
> it seems that an expression would be in some algebra, for instance
> perhaps there could be an expression where the symbols are
> elements of a group, or a boolean algebra, or even a mixture of
> algebras?
>
One reason I did not reply earlier to this is because I did not
understand what you meant by "algebra" in this context. What is the
essential characteristic of an "algebra" that is essential for your
application?
> So if lambda-calculus, combinators and intuitionistic logic are like
> expressions then, what is the algebra that they are expressions in?
>
Without completely understanding what you mean by "algebra" It seems
rather obvious that each of lambda calculus, combinators and
intuitionist logic are themselves selves "like" an algebras - or at
least, they are formal languages, each with its own syntax and
semantics. The expressions in lambda calculus are all syntactically
valid statements in that particular language, etc.
> For instance imagine I had an algebra (don't take this very loose
> pseudo-code laterally):
>
> myAlgebra(baseAlgebra)....
> .... with
> e:Record(baseAlgeba,baseAlgeba) -> % -- constructor
> m:(%,%) -> % -- binary op
> .... ==>
> Rep:=Record(A,B)
>
What is A and B? Maybe you meant Record(A:%,B:%) ? This looks just
PAIR from OpenAxiom.
> Then I could have some expression manipulator for that algebra:
>
> myExpression()....
> .... with
> e:% -> Symbol -- code to read out a given expression
> m:% -> Record(%,%)
> eval:% -> myAlgebra -- apply myAlgebra recursively to get single
> term
> ... ==>
> Rep:=Union(e:Symbol,m:Record(%,%))
>
Record(A:%,B:%)
In general this looks OK.
> But I can't see a way to define lambda-calculus, combinators or
> intuitionistic logic in this sort of way? Somehow they seem to need to
> be defined in terms of a inductively defined co-datatype like this:
>
> Rep:=Union(e:base,m:Record(%,%))
>
> rather than a datatype like this:
>
> Rep:=Record(A,B)
>
I don't understand what you are trying to say here. In each case you
will have a different set of operators (like 'm' above).
> I am coming at this in abstract terms here, but in practical terms I
> haven't yet seen a practical reason to use the domains you mention,
> for instance I haven't yet noticed a need for caching of terms, but
> that may change?
>
Representations can be chosen for reasons of efficiency or convenience
and in the best case both. In Axiom is ofter makes sense to try to
choose the "highest level" representation available which already
represents many of the essential aspects of the target domain, at
least by way of some obvious analogy (mapping).
> However I do like the idea that when the compiler compiles an
> algebra like myAlgebra then why not allow it to generate
> expression manipulator code for the algebra at the same time?
>
Could you give an example of what you mean by "expression manipulator code"?
Regards,
Bill Page
Martin Baker
I apologise for not being very precise and thanks for replying anyway.
> One reason I did not reply earlier to this is because I did not
> understand what you meant by "algebra" in this context.
I keep coming across terms like \Omega-Algebras, F-Algebras and T-
Algebras, I haven't found a precise definition of these and I think
different sources use these terms differently but my interpretation of
these terms would be:
\Omega-Algebra A set of operator symbols, each operator has an 'arity'
and
all operators act only on the elements of the algebra.
F-Algebras and F-Coalgebras are the same as \Omega-(co)algebras
except we denote all the operator signatures by a single functor.
A T-Algebra is an F-Algebra, as defined above, together with a set
of equations (axioms) built from the F-Algebra operations.
In each of these cases an 'algebra' would have a signature like this:
(%) -> %
(%,%) -> %
(%,%,%) -> %
...
and a 'co-algebra' would have a signature like this:
% -> (%)
% -> (%,%)
% -> (%,%,%)
...
So what I was trying to say is, if we are building an instance of an
'algebra' signature in FriCAS we would tend to have a representation
like:
Rep:=Record(....
But if we are building an instance of an 'co-algebra' signature in
FriCAS we would tend to have a representation like:
Rep:=Union(....
That is: the first is a datatype and the second is a co-datatype.
In the computation framework the domains appear to be of the second
type (co-datatypes) but I was thinking of Kernel (and I've probably
completely misunderstood here) as something that takes an 'algebra'
signature and allows us to solve equations in that algebra.
So I was just trying to understand whether the domains in the
computation framework are best thought of as 'algebras' or 'co-
algebras' in these terms.
If this still does not make sense, its probably best to leave it until
I/(we) attempt to translate the propositional logic code after which I
may understand Kernel better.
Martin
Bill Page
I prefer to use the email lists - one list or the other is fine.
'rep' is equivalent to the function:
rep(x:%):Rep == x pretend Rep
similarly
per(x:Rep):% == x pretend %
These functions implement type-safe casts from a domain to it's
underlying representation and back. In FriCAS these casts are (mostly)
implicit. In Aldor these where made explicit. In OpenAxiom they are
built-in. I use them all the time in my FriCAS coding.
> zero? a == zero? rep a
means that the 'zero?' function of this domain is the same as the
'zero?' function of it's representation.
Regards,
Bill Page.
On Wed, Oct 12, 2011 at 4:19 AM, Martin Baker <ax8...@martinb.com> wrote:
> Bill,
>
> Do you know what rep (lower case) does in OpenAxiom and how I could implement
> it in FriCAS? as in:
>
> zero? a == zero? rep a
>
> which comes from the code below.
>
> Martin
>
> PS: is it alright to ask you this directly or is it best to use the FriCAS or
> OpenAxiom forums?
> ---------------------------------------
> )abbrev domain ARITY Arity
> ++ Author: Gabriel Dos Reis
> ++ Date Created: December 04, 2008
> ++ Date Last Updated: May 09, 2009
> ++ Description:
> ++ This domain implements the arity of a function or an operator,
> ++ e.g. the number of arguments that an operator can take. An
> ++ arity is either a definition nonnegative integer, and the special
> ++ value `arbitrary', signifying that an operation can take any
> ++ number of arguments.
> Arity(): Public == Private where
> Public == Join(SetCategory, RetractableTo NonNegativeInteger) with
> arbitrary: %
> ++ aribitrary is the arity of a function that accepts any
> ++ number of arguments.
> zero?: % -> Boolean
> ++ \spad{zero? a} holds if \spad{a} is the arity of niladic function.
> one?: % -> Boolean
> ++ \spad{one? a} holds if \spad{a} is the arity of nullary function.
> Private == add
> Rep == SingleInteger
> arbitrary == per(-1)
> zero? a == zero? rep a
> one? a == one? rep a
> hash x == hash rep x
> x = y == rep x = rep y
> coerce(x: %): OutputForm ==
> x = arbitrary => 'arbitrary::OutputForm
> rep(x)::OutputForm
> coerce(n: NonNegativeInteger): % ==
> max()$SingleInteger < n =>
> error "arity is too large for OpenAxiom"
> per(n::SingleInteger)
> retractIfCan x ==
> negative?(n := rep x) => "failed"
> n@Integer::NonNegativeInteger
>
> @
>
Martin Baker
>
> 'rep' is equivalent to the function:
>
> rep(x:%):Rep == x pretend Rep
>
> similarly
>
> per(x:Rep):% == x pretend %
Strangely enough (just for the record) although per is not a known
function in FriCAS the following line does not produce a compile
error:
arbitrary == per(-1)
but it did not return the expected type, so I had to do:
per(x:Rep):% == x pretend %
to get the right type.
I only mention this to illustrate how messy it seems to be to to
translate from one version of Axiom to another, the compiler error
messages are not much help with this sort of thing (if only you guys
could have a reconciliation and merge the forks back together again!)
> I prefer to use the email lists - one list or the other is fine.
'fork x is better than fork y' discussion but I guess people here are
grown up enough not to do that).
Martin
Gabriel Dos Reis
| On Wednesday 12 Oct 2011 14:56:34 you wrote:
| >
| > 'rep' is equivalent to the function:
| >
| > rep(x:%):Rep == x pretend Rep
| >
| > similarly
| >
| > per(x:Rep):% == x pretend %
|
| Thanks Bill, thats very helpful.
|
| Strangely enough (just for the record) although per is not a known
| function in FriCAS the following line does not produce a compile
| error:
|
| arbitrary == per(-1)
|
| but it did not return the expected type, so I had to do:
|
| per(x:Rep):% == x pretend %
| arbitrary == per(-1)
I think the latter was part of what Bill said.
| to get the right type.
| I only mention this to illustrate how messy it seems to be to to
| translate from one version of Axiom to another, the compiler error
| messages are not much help with this sort of thing (if only you guys
| could have a reconciliation and merge the forks back together again!)
That is a valid criticism and one that I heard frequently.
However, I believe it is also plainly clear that OpenAxiom and FriCAS are
not at war (at least, the two leading developers are not) so I am not
sure "reconcicialtion" is the right word -- maybe you meant something else.
OpenAxiom and FriCAS are pursing different lines of visions -- and it is
clear that the differences are not just mere differences in how users
invokve configure. The differences in philosophy are slowly emerging
and I suspect it is going to be like that for a while.
| > I prefer to use the email lists - one list or the other is fine.
|
| No problem. (I was just trying to be tactful and avoid triggering a
| 'fork x is better than fork y' discussion but I guess people here are
| grown up enough not to do that).
I cannot speak for everybody, but I can tell you this: You would not hear
that from OpenAxiom developers; and I am sure Waldek would not engage in
that.
Martin Baker
> Martin Baker <ax8...@martinb.com> writes:
> | Strangely enough (just for the record) although per is not a known
> | function in FriCAS the following line does not produce a compile
> | error:
> |
> | arbitrary == per(-1)
> |
> | but it did not return the expected type, so I had to do:
> |
> | per(x:Rep):% == x pretend %
> | arbitrary == per(-1)
>
> I think the latter was part of what Bill said.
What I'm saying is, in FriCAS, if rep is called but not defined, then I get a
compiler error:
>> Apparent user error:
cannot compile (rep a)
but if per is called but not defined then there is no compiler error (except
for possible type mismatch in other parts of the program).
Is that what Bill said?
> That is a valid criticism and one that I heard frequently.
> However, I believe it is also plainly clear that OpenAxiom and FriCAS are
> not at war (at least, the two leading developers are not) so I am not
> sure "reconcicialtion" is the right word -- maybe you meant something else.
Yes, I did not mean to imply you are at war, just pointing out the
difficulties for end users.
Martin
Gabriel Dos Reis
| On Wednesday 12 Oct 2011 17:09:44 Gabriel Dos Reis wrote:
| > Martin Baker <ax8...@martinb.com> writes:
| > | Strangely enough (just for the record) although per is not a known
| > | function in FriCAS the following line does not produce a compile
| > | error:
| > |
| > | arbitrary == per(-1)
| > |
| > | but it did not return the expected type, so I had to do:
| > |
| > | per(x:Rep):% == x pretend %
| > | arbitrary == per(-1)
| >
| > I think the latter was part of what Bill said.
|
| What I'm saying is, in FriCAS, if rep is called but not defined, then I get a
| compiler error:
| >> Apparent user error:
| cannot compile (rep a)
|
| but if per is called but not defined then there is no compiler error (except
| for possible type mismatch in other parts of the program).
|
| Is that what Bill said?
No. :-)
The first part of your elaboration makes things clearer now and brings a
different understanding. Thanks.
-- Gaby
leh...@bayou.uni-linz.ac.at
> > zero? a == zero? rep a
zero? a == zero?(rep a)$Rep
otherwise I observe what appears to be an infinite loop at runtime.
regards,
Franz
Gabriel Dos Reis
Yes, that is needed in old AXIOM systems and any other AXIOM-descendant
that uses implicit conversion from $ to Rep and vice-versa. OpenAxiom's
choice (that Bill Page described early) prevents that surprising
behaviour, for everybody's sanity. Therefore, the $Rep is never needed
in OpenAxiom code that uses per and rep (the whole point of the exercise!)
See also
http://sourceforge.net/mailarchive/message.php?msg_id=18430416
if you are interested in having that in your favorite AXIOM flavour.
-- Gaby
Waldek Hebisch
>
> What I'm saying is, in FriCAS, if rep is called but not defined, then I get a
> compiler error:
> >> Apparent user error:
> cannot compile (rep a)
>
> but if per is called but not defined then there is no compiler error (except
> for possible type mismatch in other parts of the program).
>
In FriCAS 1.1.4 I get the same error for per. However, sometimes
one gets error about type mismatch which are really caused by
use of undefined functions.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Martin Baker
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?
Also its written using Kernel, what is the advantage of this?
Martin
------------------------------------------------
(ran in FriCAS using Waldeks translation)
(1) -> PROP := PropositionalFormula Symbol
(1) PropositionalFormula(Symbol)
Type: Type
(2) -> p := "p"::Symbol::PROP
(2) p
Type: PropositionalFormula(Symbol)
(3) -> q := "q"::Symbol::PROP
(3) q
Type: PropositionalFormula(Symbol)
(4) -> r := "r"::Symbol::PROP
(4) r
Type: PropositionalFormula(Symbol)
(5) -> pq := p /\ q
Internal Error
The function /\ with signature hashcode is missing from domain
PropositionalFormula(Symbol)
(5) -> conjunction(p,q)
(5) p and q
Type: PropositionalFormula(Symbol)
(6) -> conjunction(b := true()$PROP,p)
(6) %true and p
Type: PropositionalFormula(Symbol)
(7) -> atoms(pq)
(7) {pq}
Type: Set(Polynomial(Integer))
(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)
Gabriel Dos Reis
| 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?
|
| Also its written using Kernel, what is the advantage of this?
Kernel is the canonical datastructure for symbolic expressions in AXIOM.
The Logic (or lattice) operators ~.\/, and /\ were indeed missing
implementations. They are morally not, or, and. Fixed. I ran your
tests, and below is the output.
-- Gaby
PROP := PropositionalFormula Symbol
(1) PropositionalFormula Symbol
Type: Domain
p: PROP := 'p
(2) p
Type: PropositionalFormula Symbol
q: PROP := 'q
(3) q
Type: PropositionalFormula Symbol
r: PROP := 'r
(4) r
Type: PropositionalFormula Symbol
pq := p /\ q
(5) p and q
Type: PropositionalFormula Symbol
conjunction(p,q)
(6) p and q
Type: PropositionalFormula Symbol
b := true$PROP
(7) %true
Type: PropositionalFormula Symbol
conjunction(b,p)
(8) %true and p
Type: PropositionalFormula Symbol
atoms pq
(9) {p,q}
Type: Set Symbol
dual pq
(10) p or q
Type: PropositionalFormula Symbol
simplify conjunction(b,pq)
(11) p and q
Type: PropositionalFormula Symbol
(12) -> )quit
Waldek Hebisch
>
> 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
heb...@math.uni.wroc.pl
Martin Baker
Thanks, do you intend putting this into FriCAS? I looked in SVN trunk and
boolean.spad.pamphlet has not changed recently, or have you put it somewhere
else?
The comments below are very useful. I suspect it may also be useful to others
who may work on the code so, if you do put this into FriCAS, it would be
helpful if you could cut&paste these notes into the pamphlet file.
Thanks again,
Martin
Waldek Hebisch
>
> Waldek,
>
> Thanks, do you intend putting this into FriCAS? I looked in SVN trunk and
> boolean.spad.pamphlet has not changed recently, or have you put it somewhere
> else?
I think I will put it into FriCAS. But not yet -- it is likely
that code will change and I do all developement outside of
pamphlets. For included code basically developement cycle is
unwrap-modify-wrap and not putting code into pamphlets
saves a lot of work.
--
Waldek Hebisch
heb...@math.uni.wroc.pl