Waldek, Thanks for this, I will do my best to address these issues. I have just got back from a holiday (walking holiday in Austria) so it does not leave me much time to make changes by your deadline (If you think this might be a worthwhile addition to next release?).
Initial thoughts interspersed below: On Wednesday 08 Jun 2011 17:51:19 Waldek Hebisch wrote: > > I just thought I would mention (in case you are still interested in > > putting the code into FriCAS) that I have fixed the bugs that I know > > about in file computation.spad.pamphlet at: > > https://github.com/martinbaker/multivector/ > > > > In this pamphlet are implementations of various mathematical > > structures related to computation. such as: > > * lambda.spad > > * ski.spad > > * ILogic.spad > > Some remarks: > > - currently the code may fail to build due to use of non-ASCII > characters (this happens for example on my machine when I > use my normal setup). Basically speaking any non-ASCII character > (even in comments!) may cause build failure (unfortunatly, Lisp > treats unrecognised characters as errors). This is critical > problem as we have no control over setup of build machine. I can change this quickly (perhaps with a note that it will benefit from unicode when you are able to full commit to it). > - I see that you encode things using strings and integers. In > FriCAS better coding style is to use symbols. Basically, > use integers when you care that they are integers, that is > you perform arithmetic or use them as array indices. If you > just depend on having some distinct object and use only > comparisons (which seem to be the case), then symbols > are better. Similaray, use strings when you need to create > new ones, but if you have small number of "magic" strings, > then using symbols is better. > > If you really need a bunch of magic integers, then use macros > to give them names: > > my_magic_integer1 ==> 1::NNI > my_magic_integer2 ==> 2::NNI I can change this but it may take a bit longer (should be internal change - no effect on user interface?). > - 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. > - 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. 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? > 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. Martin -- 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.
