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. On Tuesday, March 5, 2024 at 11:58:16 AM UTC-5 [email protected] wrote: > 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 > > On Tue, Mar 5, 2024 at 4:39 PM Hill Strong <[email protected]> wrote: > >> 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/38c58617-3dba-4c9d-93f9-5ab475113281n%40googlegroups.com.
