On Sun, Jun 05, 2022 at 02:13:00PM +0200, Ralf Hemmecke wrote:
> 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(%, %).
Sure, but it means that "index" in the docstring is really not an
index...
> >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.
I do not think it is good idea, at least with current Spad compiler
and documentation machinery.
Namely, if function have separate declaration (not based on category)
conditions based on category no longer work. So we would get
more complicated and less adequate conditions in the code.
OTOH if function is inherited from category, then code can depend
only on general properties. Also, depending on what is asked
in browse one will get different dosctrings for the same function.
I think that idea of extra docstring could work if we were able
to create a "combined docstring", and show various views:
- full, with conditions applying to various part
- filtered, showing only parts with conditions satisfied
in given context
- "general", that only from original category
But that would require changes to documentation machinery. In
particular, how to mark such extra info in the code? And
different representation of docstrings in databases.
BTW: Something like above should also solve problem mentioned
by Johannes Grabmeier, that should give ability to explain
that some operations (like those from differential fields
when applied to say rationals) are trivial and possibly
hide them from view.
--
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/20220605192411.GA13687%40fricas.math.uni.wroc.pl.
