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 On Fri, 23 Feb 2024, 1:38 am Ralf Hemmecke, <[email protected]> wrote: > 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 > > -- > 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/44817e6f-f23f-49f5-b7e9-e43368b3fbe9%40hemmecke.org > . > -- 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/CAEnaMTEX_WMbk3o5_-AekpCVSo2zQ%3D8C2L1o4B3q6g66cbRPtA%40mail.gmail.com.
