On Sat, Jun 04, 2022 at 11:48:56AM +0200, Ralf Hemmecke wrote:
> On 04.06.22 04:26, Waldek Hebisch wrote:
> >On Thu, Jun 02, 2022 at 11:07:06PM +0200, Ralf Hemmecke wrote:
> >>I've just updated my branch
> >>
> >>https://github.com/hemmecke/fricas/commits/elt-universalsegment
> >>
> >>to be in line with the "intersection of indices" see testcases for
> >>detail.
> >
> >I do not think that in eager case returning empty (or shorter aggregate)
> >is good idea. Namely for streams normal if we have empty
> >stream and need an element, then we get error. OTOH in eager case we
> >depend on correct length and shortened aggregate will lead to
> >propagating wrong value.
> >
> >To put it differenly, for vectors there are two consistent views,
> >namely curremnt one and alternative view that vectors are in fact
> >infinite but have only finite number of nonzero components. The
> >second view would give 0 for out of bound references. While
> >logically consistent, the second view pragmatically seem to be
> >inferior to current one. OTOH when we have stream of coefficients of
> >series, then empty stream mean that further coefficients are zero.
> >So at pragmatic level stream case and eager case (lists and vectors)
> >are different.
> >
> >Our current code in eager case signals error early and this does not
> >cause trouble. As I wrote, signaling errors early for stream could
> >lead to trouble (for example, testing for empty before need would
> >break stream usage if done for all operations).
>
> Your view may be sensible, but I am a bit worried about the actual
> specification and whether user find that simple enough to actually use
> that functionality. If the result is not predictable then nobody will
> use list(u) or stream(u).
>
> What you say above is basically that
>
> list(u))::Stream(S)
>
> and
>
> (list::Stream(S))(u)
>
> may give different results. Personally, I would find this a bit
> confusing, but never mind, if the specification tells that this is the
> case then that should be implemented.
That is example of frequent and quite fundamental confusion.
Evaluating at point (called "specialization" in algebraic
context) is only partial homomorfizm. It works as expected
in "generic" cased but in general may fail (signal errors or
produce unexpected result). This is fundamental limitation,
we try to make it work but only as good faith effort (because
we can not promise that this will "always" work).
> So what actually is the specification?
>
> We have...
>
> LinearAggregate(S : Type) : Category ==
> Join(IndexedAggregate(Integer, S), Collection(S),
> Eltable(UniversalSegment Integer, %)) with
> ...
>
> FiniteLinearAggregate(S : Type) : Category == Join(LinearAggregate S,
> finiteAggregate)
>
> and
>
> StreamAggregate(S : Type) : Category ==
> Join(UnaryRecursiveAggregate S, LinearAggregate S) with
> ...
>
> and
>
> ListAggregate(S : Type) : Category == Join(StreamAggregate S,
> FiniteLinearAggregate S, ExtensibleLinearAggregate S) with
>
> and
>
> OneDimensionalArrayAggregate(S : Type) : Category ==
> Join(FiniteLinearAggregate S, shallowlyMutable)
>
> In other words, in all places where elt: (%, UniversalSegment) -> %
> is implemented, it inherits the specification from
> Eltable(UniversalSegment(Integer),%) with the documentation:
>
> ++ An eltable over domains D and I is a structure which can be viewed
> ++ as a function from D to I.
> ++ Examples of eltable structures range from data structures, e.g. those
> ++ of type \spadtype{List}, to algebraic structures, e.g.
> ++ \spadtype{Polynomial}.
> Eltable(D : Type, I : Type) : Category == with
> elt : (%, D) -> I
> ++ elt(u, i) (also written: u.i) returns the element of
> ++ u indexed by i.
> ++ Error: if i is not an index of u. (*)
>
> It's a bit difficult to interpret "i is not an index of u" if i is a
> segment, open or closed, with or without the "by step" part.
Actually wording above is problematic. For example in many
places we have Eltable(%, %) which if interpreted literaly
as "element of u indexed by i" leads to trouble with axiom
of foundation.
Actually, with literal interpretation as indices we should
not have 'Eltable(UniversalSegment(Integer), %)' because
segments are not elements of index set (that is segments
are not integers).
There is looser interpretation above given by the phrase
"can be viewed as a function". So probably we should
have "Error: if u is not applicable to i". However
what is applicable, that is domain of impled mapping
depends on specifics.
Also, original Axiom sources had separate 'elt : (%, U) -> %'
in linear aggregate with docstring having no mention of
error (but default implementation signalled error ...).
> Let me appreviate U==>UniversalSegment(Integer).
> What we should implement is a function (%, U)->%
>
> Let's look at ListAggregate of OneDimensionalArrayAggregate. Their elements
> are functions from a finite index set I into a set S.
> Clearly, the error condition (*) tells me that an implementation
> would have to give an error whenever u contains an integer that is
> not in I.
Literaly it should signal error because segment is not an integer,
so can not be an index...
> That clearly agrees with what you say about "error early in eager
> structures".
>
> Now Stream.
>
> ++ A stream is an implementation of a possibly infinite sequence using
> ++ a list of terms that have been computed and a function closure
> ++ to compute additional terms when needed.
>
> That tells me that a stream is either a (lazy) list (= finite stream), i.e.
> a function from a finite set I to S, or an infinite structure, i.e. a
> function from N (natural numbers starting from 1) to S.
Well, more fundamental is description from LazyStreamAggregate:
++ LazyStreamAggregate is the category of streams with lazy
++ evaluation. It is understood that the function 'empty?' will
++ cause lazy evaluation if necessary to determine if there are
++ entries. Functions which call 'empty?', e.g. 'first' and 'rest',
++ will also cause lazy evaluation if necessary.
We could add sometinig like
++ Elements of LazyStreamAggregate are computed only when strictly
++ needed. Lazy computation means that potential errors are
++ delayed, so errors are detected later than in case of normal
++ (eager) evaluation used by other aggregates. In some cases
++ computation that would signal error when using eager evaluation
++ can succeed when using lazy evaluation.
> For finite streams, I would say that it should behave exactly as in the list
> case. The only exception would be that the error occurs according to the
> laziness, i.e. early in the list case and when a non-existing index is
> accessed in the stream case.
It seems that we agree.
> For ininite streams there will be only an error if the lower index is
> less then minIndex(x).
>
> If x is a finite structure (eager of lazy) then I would interpret the
> specification of elt in such a way that x(a.. by c) must always give
> an error (in eager or lazy way).
Well, lazy way means that we get error only on actual access to
out of bound element. So code that test for presence of elements
can avoid error by not accessing unavailable elements.
> Actually, that is not what I would want or what would be similar to pythons
> slice semantics for lists of the semantics of Mathematica's span semantics.
> https://reference.wolfram.com/language/ref/Span.html
> No it is not necessary that we must have the same semantics, but as a
> convenience for the user I think that
>
> [1,2,3,4](3..) (or [1,2,3,4](3.. by -1))
>
> should give [3,4] (or [3,2,1]) instead of an error even though
> the actual set of indices represented by the segment clearly contains an
> index that falls out of the allowed range of the list.
>
> So what do we want in this last case and how do we specify it in the
> ++-docstring of "elt"?
Well, that touch much bigger subject. I mentioned some time ago
conceptual integrity. We want behaviours of various functions to
fit common pattern. Original Axiom did that quite well. Of
course, we want to go forward, but we also need to look how
our design decisions affect the whole. AFAICS one part of
orignal design was desire to catch errors early. This includes
cases which are meaningful but do not fit well to formal rules
(especialy type rules). As an example 'sqrt' of negative
float signals errors, while some other systems return
complex value. Or (ufortunate) case with 'recip' where
'recip' in the ring fails, while 'recip' in the fraction
field would work. So there is cost to this approach.
But there are also benefits. Bugs are easier to fix
when errors are detected early. And following type
rules means that code is _much_ more understandable.
However, treating FriCAS code just as formal system
IMO would be too rigid. In some cases instead for
of mathematical argument we need more "lawyer like"
argument. Even if formal argument says a there
may be overriding principle that says differently.
I think this is the case with lazy evaluation, it
overrides our desire to detect errors early.
Concering documentation, there is somewhat debatable
what we should write. IMO trying to do formal
description is (at least now) futile: it is easy
to get formal description wrong, correct formal
descriptions tend to be rather long, so it would
be large task. And it is hard to correctly read
formal description, so its usfulness for most
users is limited. Hence, I think that currently
it is better to stay at informal level. Here
tricky question is how much background knowledge
is required and what should be left unstated.
There are some math books which try to be as explict
as possible. This may be good for beginners,
but in effect such books are long and frequently
miss advanced issues. There are other which
assume a lot of background. In case of FriCAS
I think that we should take math and programming
concepts as granted (necessary background) in
reference part. It makes sense to provide tutorials
to various concepts, but with understanding that
they are not exhaustive (both in depth and in
coverage of concepts).
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/fricas-devel/20220604160629.GA25158%40fricas.math.uni.wroc.pl.
