On 04.06.22 18:06, Waldek Hebisch wrote:
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.
At first, I would have agreed with what you say about the foundational
axiom, but that is actually not a problem.
What "Eltable" actually implements is the compose functionality.
Syntactivally written as x y or x(y) or x.y is it the operation of
juxtaposition or composition \circ that is an export of the domain % if
% is of type Eltable(%, %).
In that sense, "i is an index of u" clearly can only mean that i is an
element of the source and u(i) is function application of u (considered
as a function) to i. "u considered as a function" just means that there
exists a mapping from % to %->%, or in the general case of Eltable(S,T)
a mapping from % to S->T.
And I would actually interpret u(i) also in this sense, if i is a
segment of the form (a..b by c). The segment represents a "set of
integers" and the source for a List u is the set of integers from
minIndex(u) to maxIndex(u). So the result should be the list of the
respective values, i.e, [u,x for x in i]. Similar for Stream, only that
an error would occur only if one accesses a non-existing element.
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).
As I said above, "index" is to be interpreted as "an element of the
source of the function". Now, of course, in the case of
Eltable(UniversalSegment(INT),%) we would have to understand that an
element from % can also be considered as a (mathematical) function from
the set of all finite subsets of the natural numbers to List(X). An
"index" is then a "finite subset of 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".
Yep, exactly. We view u as a (partial) function and an error occurs if
i is not in the source of that function.
However what is applicable, that is domain of impled mapping depends
on specifics.
Yes, agreed. What "applicable" means is rather vague. And probably too
hard to document in a reasonably short specification that would be human
readable. At least I would aim for "guiding principles". In that sense I
fully agree with your statement that lazyness should overrule "early 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...
Not my view, see above.
We could add sometinig like
++ Elements of LazyStreamAggregate are computed only when strictly
++ needed. Lazy computation means that potential errors ar > ++ 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.
That would at least give a hint to "laziness overrules early error".
Yes, something like this should be added.
[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"?
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.
I agree. I think it is a dream that one can describe a generic function
and cover all cases.
What I was actually pointing at was that it could make sense to instead
of declaring Eltabe(UniversalSegment(INT), %) to export also
elt: (%, UniversalSegment(INT) -> % (*)
and give it an appropriate refined docstring.
It's a bit of a vague idea, but it could make sense to add in the
docstring for the specific case (*) the cases what happens for
list(a.. by c) where one would generically expect an error, but here we
deviate and declare what it means.
What should in the end appear at fricas.github.io/api should (of course)
be the documentation for the generic elt from Eltable PLUS the
additional docstring for (*).
Of course that creates the danger that people invent/document completely
contradicting properties to the generic case. However, we are working in
the open and should not let pass such problems via a review process. So
danger is low.
What do you think about such "additional clarifications via docstring"
in specific instantiations of a function? I do not currently know what
actually happens for the (*) case, i.e. if my api-extraction program
would actually be able to get the docstring for the elt of Eltable and
the specific elt (*). Oh... and there might be some more elt-docstrings
inbetween.
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/fricas-devel/43c99b5d-dee9-61c5-43d8-8572373a8f4c%40hemmecke.org.
