What would you call Join(SemiRng, AbelianMonoid) as a category

[Hill Strong]

I have quite a few places in the FriCAS source code the following

Join(SemiRng, AbelianMonoid)

What would you call this particular algebraic structure?

[Ralf Hemmecke]

The name is actually irrelevant. Since it is a Join, it is actually an
unnamed category in FriCAS that is only there for the purpose of listing
the exports (probably you have found it places like this:
https://github.com/fricas/fricas/blob/master/src/algebra/polycat.spad#L21
or this
https://github.com/fricas/fricas/blob/master/src/algebra/matcat.spad#L723
).

It says nothing more than for functionality that is provided by (for
example) RectangularMatrixCategory, it is enough, if the coefficient
domain is a (possibly non-commutative wrt. multiplication) Ring
(possibly without 1).

It looks as if SemiRng would be enough, but seemingly the existence of
the additive neutral element 0 is required.

Of course, FriCAS could introduce a name for this, and perhaps some day
it will, but it seems not necessary now.

I guess, if you are not satisfied with this answer, Waldek will comment
more on this.

Ralf

[Hill Strong]

My count is that there are 24 occurrences of this particular combination. There are other combinations that exist for which a named category is available - one example is Join(LinearAggregate(S),   finiteAggregate) which can be replaced with FiniteLinearAggregate(S). One place applicable would be FiniteLinearAggregateFunctions2.

When I see this in code bases, it is an indicator that this should be looked at and fixed appropriately.

Hill

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/1c623d73-91b9-4b1b-837d-22e063190571%40hemmecke.org.

[Ralf Hemmecke]

On 2/21/24 18:04, Hill Strong wrote:
> My count is that there are 24 occurrences of this particular combination.
> There are other combinations that exist for which a named category is
> available - one example is Join(LinearAggregate(S), finiteAggregate)
> which can be replaced with FiniteLinearAggregate(S). One place applicable
> would be FiniteLinearAggregateFunctions2.

> When I see this in code bases, it is an indicator that this should be
> looked at and fixed appropriately.

Suppose there are two categories CatA and CatB and we define

CatAB: Category == Join(CatA, CatB)

You know that there is a little difference between

FooJ(D): Export == Implementation where
D: Join(CatA, CatB)
Export ==> ...
Implementation ==> ...

and

FooC(D): Export == Implementation where
D: CatAB
Export ==> ...
Implementation ==> ...

.

If we have

Dom: Join(CatA, CatB) == ...

then

FooJ(Dom) is OK, while FooC(Dom) is not.

In that sense the definition of FooJ is more general.

Yes, it may make sense to introduce specific categories, like CatAB,
but you then have to go through the whole FriCAS sources and figure out
in which cases you might have to add something like CatAB to the exports
of a certain domain (or category, and maybe even conditionally, i.e.
depending on a domain parameter). That is doable, but sounds a bit
error-prone. I don't even know whether it is easy to check that such a
code modification did not introduce unwanted behaviour, because we might
not yet have a test included for such circumstance.

Ralf

[Hill Strong]

Good morning Ralf,

On Thu, Feb 22, 2024 at 4:49 AM Ralf Hemmecke <ra...@hemmecke.org> wrote:

[Remove ...]

Suppose there are two categories CatA and CatB and we define

CatAB: Category == Join(CatA, CatB)

You know that there is a little difference between

FooJ(D): Export == Implementation where
   D: Join(CatA, CatB)
   Export ==> ...
   Implementation ==> ...

and

FooC(D): Export == Implementation where
   D: CatAB
   Export ==> ...
   Implementation ==> ...

You say that there is [little] difference. Why is there any difference? In one case you have created a name for the Join, in the other it is anonymous. Yet, the [value] that is the category in both cases should be identical and hence NO difference between either specification. If there is then the system has a major problem that is not explained anywhere. The semantics should be identical.

 

.

If we have

Dom: Join(CatA, CatB) == ...

then

FooJ(Dom) is OK, while FooC(Dom) is not.

Again, what difference is there between either case? The underlying category [value] should be the same and defining a domain as you have done  and used in either definition should result in an identical code production.  If it does not then again there is a serious problem with the semantics and the compiler is going to bite the user and the code developers in strange and very awkward ways.

In that sense the definition of FooJ is more general.

This should not be the case.

Yes, it may make sense to introduce specific categories, like CatAB,
but you then have to go through the whole FriCAS sources and figure out
in which cases you might have to add something like CatAB to the exports
of a certain domain (or category, and maybe even conditionally, i.e.
depending on a domain parameter). That is doable, but sounds a bit
error-prone. I don't even know whether it is easy to check that such a
code modification did not introduce unwanted behaviour, because we might

There should be very very few cases (zero or close to it) where such changes would be different  semantically. If there does arise differences then the underlying compiler (boot) is the problem and needs seriously to be fixed.

FriCAS has a high enough learning curve as it is, without strange little semantic anomalies coming out and biting  you like some yapping little ankle-biting dog at unexpected times. I fully understand that any code base, especially one as old as this, will build up a lot of cruft over its lifetime. But it does need to be dealt with or the code base will become unmaintainable in many ways. Making little ad hoc changes here and there does not garner well for the system's future where you want more people to be interested in and actively use the system. Axiom and FriCAS both deserve better as does all the hard work that has been put into each by all the people who have been involved over the decades.

not yet have a test included for such circumstance.

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...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/a37b415c-7eb1-4cb6-8b37-f84f87f9bf5a%40hemmecke.org.

[Ralf Hemmecke]

On 2/21/24 21:23, Hill Strong wrote:
> Good morning Ralf,
>
> On Thu, Feb 22, 2024 at 4:49 AM Ralf Hemmecke <ra...@hemmecke.org> wrote:
>
>> [Remove ...]
>> Suppose there are two categories CatA and CatB and we define
>>
>> CatAB: Category == Join(CatA, CatB)
>>
>> You know that there is a little difference between
>>
>> FooJ(D): Export == Implementation where
>> D: Join(CatA, CatB)
>> Export ==> ...
>> Implementation ==> ...
>>
>> and
>>
>> FooC(D): Export == Implementation where
>> D: CatAB
>> Export ==> ...
>> Implementation ==> ...
>>
>>
> You say that there is [little] difference. Why is there any difference? In
> one case you have created a name for the Join, in the other it is
> anonymous. Yet, the [value] that is the category in both cases should be
> identical and hence NO difference between either specification. If there is
> then the system has a major problem that is not explained anywhere. The
> semantics should be identical.

See https://fricas.github.io/book.pdf page 15: "Domains Belong to
Categories by Assertion",

You may wish for something else, but that's the way it is in FriCAS (and
Aldor).

>> If we have
>>
>> Dom: Join(CatA, CatB) == ...
>>
>> then
>>
>> FooJ(Dom) is OK, while FooC(Dom) is not.
>>
>
> Again, what difference is there between either case?

Dom is of CatA and of CatB but not of CatAB. FooC requires its argument
to be of CatAB, but Dom is not of that type, so FooC(Dom) cannot be
compiled.

> The underlying
> category [value] should be the same and defining a domain as you have done
> and used in either definition should result in an identical code
> production. If it does not then again there is a serious problem with the
> semantics and the compiler is going to bite the user and the code
> developers in strange and very awkward ways.

You wish something else. That's fine. But the SPAD language implements
"a domain only belongs to a (named) category if that category is
explicitly included when the domain is defined".

There are ideas of "post facto extensions" in Aldor
http://www.aldor.org/docs/HTML/chap10.html or look into the Aldor User
Guide (http://www.aldor.org/docs/aldorug.pdf) that would make life a bit
easier. Unfortunately, SPAD does not (yet) implement this idea.
And it would still be the same. Domains belong to categories by assertion.

>> Yes, it may make sense to introduce specific categories, like CatAB,
>> but you then have to go through the whole FriCAS sources and figure out
>> in which cases you might have to add something like CatAB to the exports
>> of a certain domain (or category, and maybe even conditionally, i.e.
>> depending on a domain parameter). That is doable, but sounds a bit
>> error-prone. I don't even know whether it is easy to check that such a
>> code modification did not introduce unwanted behaviour, because we might
>>
>
> There should be very very few cases (zero or close to it) where such
> changes would be different semantically. If there does arise differences
> then the underlying compiler (boot) is the problem and needs seriously to
> be fixed.

You can see it that way. However, the current behaviour *is* documented
and the compiler behaves accordingly.

> FriCAS has a high enough learning curve as it is, without strange little
> semantic anomalies coming out and biting you like some yapping little
> ankle-biting dog at unexpected times. I fully understand that any code
> base, especially one as old as this, will build up a lot of cruft over its
> lifetime. But it does need to be dealt with or the code base will become
> unmaintainable in many ways. Making little ad hoc changes here and there
> does not garner well for the system's future where you want more people to
> be interested in and actively use the system. Axiom and FriCAS both deserve
> better as does all the hard work that has been put into each by all the
> people who have been involved over the decades.

If you can help to make FriCAS better, you are welcome.

As for the learing curve... I usually point someone who wants to learn
SPAD to reading the Aldor user guide (AUG). Yes, Aldor is a bit
different from SPAD (I once listed a number of them here
http://wiki.fricas.org/LanguageDifferences), but the AUG much better
defines the language than the FriCAS-book does.

Ralf

[Hill Strong]

Good morning Ralf,

I have no issue with this. However, whether a particular assertion is named or not, it should not matter once you have made the assertion. Unless, each assertion generates something new.

If you were to say 

Join(CatA, CatB) in one place and then do so again in another place and each of these assertions is different from each other then I would not have a problem with it also being different from a named assertion CatAB.

BUt, as far as I can tell, using the former in multiple places means the same semantically. Hence the question as to why if would be different from the named variety?

>> If we have
>>
>> Dom: Join(CatA, CatB) == ...
>>
>> then
>>
>> FooJ(Dom) is OK, while FooC(Dom) is not.
>>
>
> Again, what difference is there between either case?

Dom is of CatA and of CatB but not of CatAB. FooC requires its argument
to be of CatAB, but Dom is not of that type, so FooC(Dom) cannot be
compiled.

But why is the distinction being made as they are the same thing? The only difference is the that one uses a name and the other doesn't.

> The underlying
> category [value] should be the same and defining a domain as you have done
> and used in either definition should result in an identical code
> production.  If it does not then again there is a serious problem with the
> semantics and the compiler is going to bite the user and the code
> developers in strange and very awkward ways.

You wish something else. That's fine. But the SPAD language implements
"a domain only belongs to a (named) category if that category is
explicitly included when the domain is defined".

From my perspective then this is wrong on the part of the SPAD implementation unless every anonymous  usage is to be considered different even though they have identical forms. The point is subtle but highly important for consistency.

There are ideas of "post facto extensions" in Aldor
http://www.aldor.org/docs/HTML/chap10.html or look into the Aldor User
Guide (http://www.aldor.org/docs/aldorug.pdf) that would make life a bit
easier. Unfortunately, SPAD does not (yet) implement this idea.
And it would still be the same. Domains belong to categories by assertion.

As I said above, there is no issue here. The problem from my perspective is that the assertion is identical irrespective of whether the assertion is named or anonymous.

 

>> Yes, it may make sense to introduce specific categories, like CatAB,
>> but you then have to go through the whole FriCAS sources and figure out
>> in which cases you might have to add something like CatAB to the exports
>> of a certain domain (or category, and maybe even conditionally, i.e.
>> depending on a domain parameter). That is doable, but sounds a bit
>> error-prone. I don't even know whether it is easy to check that such a
>> code modification did not introduce unwanted behaviour, because we might
>>
>
> There should be very very few cases (zero or close to it) where such
> changes would be different  semantically. If there does arise differences
> then the underlying compiler (boot) is the problem and needs seriously to
> be fixed.

You can see it that way. However, the current behaviour *is* documented
and the compiler behaves accordingly.

From your perspective, it may appear to be true. But from my perspective as someone who has and does design languages, it is not. We can back and forth this all day and not come to any form of agreement. So be it. At least, I am getting some very useful information from these discussions, so thank you.

> FriCAS has a high enough learning curve as it is, without strange little
> semantic anomalies coming out and biting  you like some yapping little
> ankle-biting dog at unexpected times. I fully understand that any code
> base, especially one as old as this, will build up a lot of cruft over its
> lifetime. But it does need to be dealt with or the code base will become
> unmaintainable in many ways. Making little ad hoc changes here and there
> does not garner well for the system's future where you want more people to
> be interested in and actively use the system. Axiom and FriCAS both deserve
> better as does all the hard work that has been put into each by all the
> people who have been involved over the decades.

If you can help to make FriCAS better, you are welcome.

My goal at the moment is to redesign the language to be more consistent and more shall we say [modern] bringing it up to the mid-70's to mid-80's. The reason I am asking these questions is that in making the language more consistent, these things are being found in the FriCAS code base.

SPAD itself will be essentially dispensed with. There are certain aspects of the language that are amenable to using LR parsers and other aspects where the current Pratt parser is better suited. I have in the past incorporated dynamic changes of Lexers into LR parsers and now I am working on incorporating Pratt parsing into LR parsing, which is an interesting project in and of itself. It hasn't been done in this particular way before (at least not in the literature that I have been reading) but it shouldn't be too problematic as it is a variation on how error handling is at times incorporated into LR parsers.

As for the learing curve... I usually point someone who wants to learn
SPAD to reading the Aldor user guide (AUG). Yes, Aldor is a bit
different from SPAD (I once listed a number of them here
http://wiki.fricas.org/LanguageDifferences), but the AUG much better
defines the language than the FriCAS-book does.

Ralf

Have a blessed day ahead 

Hill

 

--
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...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/702b534b-dab0-4ccb-a16a-c9c4923976a2%40hemmecke.org.

[Waldek Hebisch]

Well, for use by people reasonable name name is "semiring". In FriCAS
we need to do more: in common mathematical practice various details
are dismissed using phrase "it will cause no confusion to the reader"
(and frequently this phrase is used in situations which do cause
confusion). In this case important distincion is presence or absence
of neutral elements. In FriCAS Rng means a ring possibly without
a multiplicative unit while Ring means ring with multiplicative unit.
In case of semiring there are two units in question: additive one
and multiplicative one. Most general case is semiring possibly without
both additive and multiplicative unit, that is SemiRng. SemiRing
means semiring with both additive and multiplicative unit.
Join(SemiRng, AbelianMonoid) means semiring with additive unit but
possibly without multiplicative unit. Once we need to make such
fine distinctions it makes sense to have a systematic way to
create names. From this point of view Join(SemiRng, AbelianMonoid)
is quite a good name, once you grasp consepts it is clear what it
means and it is IMHO easy to remember. Alternative of having
names like SemiRngWithAdditiveUnit or

SemiRingButPossiblyWithoutMultiplicativeUnit

are clumsy and harder to remember (ypu need to remember something
which is essentially arbitreary choice).

There are also technical issues. As Ralf wrote Join is different
from named category. You seem to think that this is wrong, but in
fact this goes to very old and fundamental question about types,
namely: "When two types are equal". There are two popular answers
to this question. One answer is that each declaration creates new
type, distinct from all other types, this is typically called "name
equivalence". The second anwer is that each type is build is some
way and types build in the same way are equal. This second answer
is called "structural equivalence". Each of answers has it advanteges
and drawbacks. Arguably, name equivalence gives better support to
data abstraction: mere fact that types are build in the same way
(say both are integers at implementation level) does not mean that
the types are intended to be exchangable in any context. OTOH
in some situations we do want structural equivalence. In Modula 3
designers decided to give users both possiblities, by default
Modula 3 uses structural equivalence, but user can add a keyword
(IIRC "branded") to the definition to indicate that the type should
use name equivalence. In FriCAS types have parameters and
"type name" logically includes paramenters. So natural choice is
that types are equal when they have the same constructor and the
same parameters, where equality of parameters is recursive for
parameters being types and should use domain equality for non-type
parameters. Now, under name equivalence:

SemiRngWithAdditiveUnit : Category == Join(SemiRng, AbelianMonoid)

has different name than Join(SemiRng, AbelianMonoid), so is a different
type. Name equvalence is problematic for anonymous types. Namely
under strict interpretation each occurence of the same expression
would create a new type distinct from other types. This is of limited,
so it is natural to use structural equvalence for anonymous types. In
FriCAS trurly anonymous type are rare, but when they appear they
use structural equvalence.

Coming back to your question/problem: FriCAS algebra tries to promote
and use generic coding, that is code is supposed to run with rich
variety of types. Applicability of various methods/algorithms depends
on "features" of data, that is logical assertions and available
functions (interfaces). In FriCAS this is expressed via categories.
In order to type check Spad compiler needs to make inferences.
For Join needed inference is a general rule: Join has all properties
of its arguments. For named categories rule is a bit different:
category has properties explicitely mentioned in its definition,
which for named categories means that such category has more
properties, namely SemiRngWithAdditiveUnit above has one property more
than Join(SemiRng, AbelianMonoid), namely SemiRngWithAdditiveUnit.
So, for proper inference in Spad compiler we need in algebre code which
informs compiler about propagation for named categories. So
with named categores we need more code because we need to add various
propagation rules. For Join propagation is automatic. OTOH rules
written in code are more flexible than rule used by Join.

Anyway, using Join is natural in situations that can be handled by
it. Named categories are for for more complicated situations and
when we want to be closer to clasical mathematical nomenclature which
heavily depends on names.

--
Waldek Hebisch

[Ralf Hemmecke]

I also want to add this bit.

https://github.com/fricas/fricas/blob/master/src/algebra/catdef.spad#L214

CharacteristicZero() : Category == Ring

===============

Suppose

Foo1(R: CharacteristicZero) : ... == ...
Foo2(R: Ring) : ... == ...

FriCAS uses the named category CharacteristicZero to transport the
message that a corresponding domain should implement a ring with
characteristic 0. That is a bit of information that can be exploited in
the implementation of Foo1, but not Foo2.

Admittedly, it would be nicer that instead of just using well-chosen
names we had a mechanism (syntax) to specify the mathematical axioms for
that property.

Similarly, it is done for CommutativeRing. Commutativity of * of the
ring in FriCAS is nowhere else specified than by the special category
CommutativeStar which (more or less) comes with an empty definition as
most other categories in the file attribs.spad.

https://github.com/fricas/fricas/blob/master/src/algebra/attribs.spad#L88

Hill, if you find a better (more mathematical) way to implement
properties/axioms that would be great. It probably was a challenge back
then when Scratchpad started, but maybe it is not anymore. Do you know?

Ralf

[Hill Strong]

Ralf,

After reading and digesting both Waldek's and your responses, my view is that the FriCAS language is conflating a number of ideas into a single syntactic structure.

Looking through the source code available, there are various [properties] that are being defined automatically under some circumstances and having to be defined manually in others. 

This is the first inconsistency since it is not obvious to those coming from alternative fields.

It may now be far too late to fix this.

The other problem is the use of category definitions to specify some particular property or axiom. The example being the Characteristic 0. 

In this case, additional syntax/semantic support is required as pointed out by yourself. Since there are different kinds of axioms and/or associated properties that are applicable and there appears to be various ways that these axioms can be specified, one would have to find  common ground here.

That common ground could be in the form of incorporating systems like Lean 4 or Metamath. The problem would then require the ability contained in the system t be able to restructure code entered under user control. Certainly, FriCAS already incorporates some of the required functionality by its type system, but whether this additional restructuring (by application of the axioms) is feasible, I don't know.

A different approach may be required by looking at alternative systems and using them as a base (such as Lean 4).

An interesting question and problem.

Hill

--
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...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/44817e6f-f23f-49f5-b7e9-e43368b3fbe9%40hemmecke.org.

[Hill Strong]

Further to my previous comment and opening an opportunity for discussion.

Properties should not be automatic in that it is up to the programmer to decide if he/she wants a category or domain to have some specific property. This is already done in various areas. It would mean that the default functionality of a category definition would be removed.

Now in terms of axioms, I think that a new facility of defining axioms within the category/domain definitions would be better suited for clarity and understanding.

Possibly something like

Axiom name : syntactic structure

Axiom LeftDistributive : Operator(*,+) Variables(a,b,c) == a*(b+c) <-> a*b + a*c

Axiom CharacteristicZero : Characteristic(0)

I do not have sufficient knowledge to really suggest what should be appropriate here. But we can at least open the discussion to what might be suitable.

Hill

[Tim Daly]

LEAN4 and mathlib provide a solid foundation for a future upgrade.

I am currently looking at parallel hierarchical structures which would

mirror the category structure now in place. A Group, for example, would

have a corresponding "proof" structure which asserts various axioms, theorems,

and definitions. The proof structure would inherit LEAN4 information and

make it available to domains that implement Group functions. These

functions could then be proven using the Group-Proof information.

This has the additional benefit that, once proven, a function can be used

in other domains as part of proofs of their functions.

[Hill Strong]

Tim, please keep us apprised of your progress.

Hill 

To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/38c58617-3dba-4c9d-93f9-5ab475113281n%40googlegroups.com.