Tim, please keep us apprised of your progress. Hill
On Thu, 7 Mar 2024, 4:47 am Tim Daly, <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/fricas-devel/38c58617-3dba-4c9d-93f9-5ab475113281n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAEnaMTF2TDNAk84jQXNiJepHrvGafsm7C8df6zs8Oe20qwTH9A%40mail.gmail.com.
