Re: [fricas-devel] Conditional exports in some types

2018-12-15 Thread Waldek Hebisch
Ralf Hemmecke wrote:
> 
> Hi Waldek,
> 
> Peter has updated his pull request
> 
> https://github.com/fricas/fricas/pull/5
> 
> some time ago. It is working for me and I would like to commit these 5
> patches to the fricas svn repository.
> 
> I was a bit concerned about him adding lowercase 'and, 'or, 'not into
> ax.boot.
> 
> https://github.com/fricas/fricas/commit/8c372df4dcfd1effbf66ba2780aea0d067b0bf10#diff-6b936c4207acbd850ff5bdb79c61e89fR378
> 
> But seemingly as described in my mail from Oct 2
> 
> see here
> https://groups.google.com/forum/#!msg/fricas-devel/vFWHujprxno/NEbM_1oUAAAJ
> 
> or here
> https://www.mail-archive.com/fricas-devel@googlegroups.com/msg12569.html
> 
> , these symbols are really generated by FriCAS.
> 
> It is not clear why FriCAS does this.
>
> Nevertheless, since I want to get rid of these pending patches, my
> question, can I commit them to the FriCAS repo?
> We can single out the issue with 'and vs AND later.
> 
> The patches are only connected to the aldor interface and don't
> otherwise interfere with anything else in FriCAS.
 
Yes, please go on and commit.

Concerning 'and' versus 'AND' problem I am affraid that
this is just part of bigger problem, that is general mess
in Spad compiler.  This is big problem in the sense that
"simple" thing with correct semantics is uncomputable
(the problem of staticaly deciding what will happen to conditions
at runtime is undecidable).  Simple computable appraches are
quite restrictive.  "Better" computable things quickly tend to
be quite complicated.  So Spad compiler gives ill-defined
handling which in cases used by Spad library gives resonable
results.  But the compiler code while relatively short is
messy.  'and' versus 'AND' is part of this mess.
More precisely, at Spad source level we have 'and'.
At runtime we need 'AND' because conditions are evaluated
by Lisp.  In clean design there would be sharp transition
between one representation (using 'and') and the other
(using 'AND').  But Spad compiler cleverly re-uses routines
for multiple purposes and extensively uses recursion.
So there are no clear separation of stages, logically the
same processing is done in several stages and data from
later stage may be feed back as input to earlier stage.

The intent of several my commits to compiler code was to
untangle this mess.  I would say that now most "accidental"
problems/inconsistencies are removed.  But deeper problem
remain, in particular problem of typechecking types: our
typechecking routines sometimes (in general case) need to
evaluate types.  But to safely evaluate we need to typecheck
first.  So there is stange recursion between evaluation
and typechecking.  Simple conditions that a priori
exclude possibility of infinite recursion seem to be
quite restrictive.  More useful approach could say that
compiler should do things as lazy as possible and
when even lazy way lead to infinite recursion than
program is incorrect.  OTOH even when lazy evaluation
leads to infinite recursion it may be possible to
compute fixpoint.  Let me say that giving sound
and useful theoretical formulation and implementing
it is still an open problem.  And that affects 'and'
problem: we need to find replacement for current
handling of conditions.

-- 
  Waldek Hebisch

-- 
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 fricas-devel+unsubscr...@googlegroups.com.
To post to this group, send email to fricas-devel@googlegroups.com.
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.


Re: [fricas-devel] Conditional exports in some types

2018-10-02 Thread Ralf Hemmecke
Hi Peter, hi Waldek,

Taking some content of a private mail from Peter that concerns the same
topic of this thread...

On 10/01/2018 09:51 PM, Peter Broadbery wrote:
> Taken a slightly closer look to remind myself - see for example the
> file index.KAF in build/src/algebra/PSCAT.NRLIB - the function '-'
> (ie. negate) has a condition
> consisting of both "|and|" and "AND".  There's no occurrences of
> '|not|' or '|or|', but it doesn't seem impossible that they could be
> generated. ")sh PSCAT" shows something similar - 'and' appears as both
> a function and a logical operation.

Interesting... index.KAF and )sh PSCAT show indeed quite some
complicated expression for unary "-". I wonder why my api.spad still is
able to simplify to true, i.e. no condition here

http://fricas.github.io/api/PowerSeriesCategory

for unary "-".

I must dig deeper, but my first impression is that api.spad collects all
signatures for a category recursively via

  GETDATABASE(x, 'CONSTRUCTORCATEGORY)

There seems to be only something of the form

  (IF  (has $ (VariablesCommuteWithCoefficients))
(IF (has t#1 (IntegralDomain))
(ATTRIBUTE (IntegralDomain))
noBranch)
noBranch)

returned from such a call. No AND or |and|.

Obviously FriCAS constructs the conditions for index.KAF or )sh PSCAT in
a different way and seemingly inconsistently.

Ralf

-- 
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 fricas-devel+unsubscr...@googlegroups.com.
To post to this group, send email to fricas-devel@googlegroups.com.
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.


[fricas-devel] Conditional exports in some types

2018-10-02 Thread Peter Broadbery
Hi,

I've been looking at the aldor interface (again), and found there's a
few categories in fricas with what appears to be an incorrect
condition on some exports

For example, conditionP in POLYCAT has the following condition:

conditionP : Matrix(%) -> Union(Vector(%),"failed") if
and(has($,CharacteristicNonZero),has(R,PolynomialFactorizationExplicit))

I'd expect 'AND' to be an infix operator as normal.

Obviously it's not causing much of a problem as the workaround is
trivial, but seems to imply that there's some simplification missing
(or 'and' is not being mapped to 'AND' in this case).  Two other
categories have similar exports, DIRPCAT and PSCAT.

Peter

-- 
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 fricas-devel+unsubscr...@googlegroups.com.
To post to this group, send email to fricas-devel@googlegroups.com.
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.