>
> I don't know if this is relevant to your discussion about kernels (most
> of it goes over my head) but I thought I might mention something I would
> like to implement, at some time in the future, in case there is some
> requirement that is relevant?
>
> Some time ago I implemented intuitionistic logic with a rep like this:
>
> ILogic() : Exports == Implementation where
> ....
> Rep := Union(_
> const : Record(val : Symbol), _
> var : Record(str : String), _
> binaryOp : Record(typ : Symbol, c1 : %, c2 : %), _
> unaryOp : Record(typ : Symbol, c1 : %)_
> )
>
> I would like to make this more general and allow many types of
> propositional logic and associated algebras such as boolean, (co)Heyting
> algebra and so on.
>
> In OpenAxiom Gaby implemented PropositionalFormula using Kernel like this:
>
> PropositionalFormula(T: SetCategory): Public == Private where
> ....
> Rep == Union(T, Kernel %)
>
> Would it be better if I used Kernel like this?
Yes, this representation looks fine.
> I get the impression most
> of the issues you are discussing are around casheing. I suspect there
> would not be the same performance issues for discrete algebra like this?
> I might even question if FriCAS/pan-axiom is the way to go for discrete
> algebra? I suspect you are optimising for more numerical based algebra?
The discussion is more about equality and builtin simplifications.
We could use representation like above for Expression(Integer).
But then we would have to provide special code to implement
simplifications due to associative law, distributive law, etc.
For Expression(Integer) user expectation is that say 'x*(y + z)'
is equal to 'y*x + x*z' and we implement equality so that this
is true. For logic formula user do not expect such simplifications,
so it is enough to provide equality essentialy as trees. I other
words for your purpose you can just use equality from representation.
Of course, you could get more ambitious and say that two formulas
are equal in your domain if and only if they are logically equivalent.
For pure Boolean propositional logic there are representations with
such property, namely disjuntive (or conjunctive) normal forms
or binary decision diagrams. But if you enrich your logic
a bit then you would have similar (probably worse) problems
to the ones appearing in Expression(Integer).
Conserning preformance issues: AFAIK fast theorem provers use
specialized representation based on normal forms or binary decision
diagrams. And they spent a lot of attention on low level details.
In general purpose system like FriCAS efficiency in normally
lower than in specialized systems. We could try to provide
an optimized domain which internally uses representation like
fast provers. But providing something slower but
working already would be a progress compared to current
situation (that is no domain for logical formulas).
--
Waldek Hebisch
[email protected]
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
