Martin Baker 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 representaion.
>
> I can't claim to have checked all existing domains (especially the
> more sparsely documented ones). I've just had a quick glance at Kernel
> domain which seems to require a fixed list of arguments at
> construction? SExpression seems to involve base (Lisp) types? It looks
> like these domains may not be compatible because the arguments of the
> 'computation' domains are functions and combinators and the operation
> is function composition and these functions don't need to defined at
> construction time. For combinators the number of arguments is variable
> and so function composition is non-associative hence it is represented
> by binary tree structure. For Lambda calculus we have bound and
> unbound variables so again non-associative and represented by binary
> tree structure. So we could extend some non-associative or binary tree
> structure class but I can't see a great benefit in doing so?
>
> Eventually, if I could find a way to do it, it would be good to have a
> function composition (hom-set) domain and to implement these as a
> special (non-associative) version of that.
>
> I'll have a better look at Kernel domain and see if I can find some
> documentation about it to see if my initial thoughts about this not
> being compatible are correct.
>
1) 'kernel' takes _list_ of arguments, so effectively you can have
arbitrarily many arguments. Most of existing operators take
fixed number of arguments, but this does not prevent you from
using new operators with variable number of arguments. The
main feature of Kernel is that is contains a cache, there is
exactly one kernel of given value. If you try to create new
kernel equal to an old one the creation function gives you back
the old one from the cache. This has several advantages (essentially
this gives you "common subexpression elimination" for free), but
also some costs.
2) SExpression can encode arbitary tree-like structures. If you
are encoding things SExpression should be more convenient than
using for example integers.
> > - Meaning of your '=' for intuitionistic logic is not clear. My impression
> > is that for quantifier-free intuitionistic formulas equivalence is
> > decidable, so that may be more natural choice.
>
> The intuitionistic logic domain has both symbolic and literal elements
> so its not possible to to reduce to purely literal elements to
> compare.
Sure. I mean formulas with symbolic elements. By definition two
formulas are equvalent if each is conseqence of the other. For
example variable x is not equivalent to variable y, while AFAICS
expression x /\ x is equivalent to x. As I wrote, my impression is
that there is an algorithm to decide if two (quantifier-free)
intuitionistic formulas are equivalent.
> We could do some limited simplification before comparison,
> for example x /\ T to x, but I don't know how useful that would be
> until I use it and develop it a bit more.
>
> For literal values I assume that:
>
> T = T
> _|_ = _|_
> undefined = undefined
>
> would all be true and all other combinations would be false?
>
That is problematic: intutionistic logic can not be faithfully
represented by three values, you need infinitely many. Your
table look correct if you treat 'undefined' as another variable,
but if you want "values" for formulas with more then one
variable, then finite number of values will not do.
> > Releated to this I think
> > that there are more generally valid simplifications for intuitionistic
> > logic and the one you use seem fairly incomplete.
>
> This might also take a bit longer, again I need to get a set of rules
> that work for both symbolic and literal elements.
>
> This reply is a bit hurried (and I'm still in holiday mode) but I
> thought I would check to see if you would want this in the next
> release and what the minimum changes would be required.
>
The critical thing is elimination of non-ASCII letters. The other
are suggestions for improvement.
--
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.
