4 ms·

Lean does have a tactics system (very similar to Coq). However, there is no general tactic that will do, e.g., "sin^2 + cos^2 = 1" for you. (Writing a tactic sp

Lean does have a tactics system (very similar to Coq). However, there is no general tactic that will do, e.g., "sin^2 + cos^2 = 1" for you. (Writing a tactic specifically for that simplification is easy, of course, but that's not what a CAS is). (I doubt there is one in Coq that will do this, although I'm not sure). A symbolic algebra system is expected to do this simplification (and much more advanced ones) automatically. All in all, proof assistants aren't computer algebra systems. You could make computer algebra systems in those frameworks but I'm not aware of any.

zozbot234 3y ago
Typically, there are 'group', 'ring' and 'field' tactics that will perform simplification in the relevant algebraic structures. Going from that to solving sin^2 x + cos^2 x is simply a matter of writing more such tactics, operating on e.g. real fields or whatever is applicable in any given case. This is a lot less ad-hoc than whatever CAS's do, but it's also less error prone.
- westurner 3y ago
  Do any existing CAS systems have configurable axioms? OTOH: Conway's surreal infinities, Do not early eliminate terms next to infinity, Each instance of infinity might should have a unique identity, configurable Order of operations, All of the axiomatic transformations applied by a CAS like SymPy should/must be in Lean Mathlib somewhere? If nothing else, a lookup_lean_mathlib_definition(expr, 'path/to/mathlib-v0.0.2') or find_similar(expr, AxiomDB) would be useful. How do CAS differ from Production Rule Systems? https://en.wikipedia.org/wiki/Production_system_(computer_science) https://en.wikipedia.org/wiki/Production_system_(computer_sc... CAS > Simplification: https://en.wikipedia.org/wiki/Computer_algebra#Simplification https://en.wikipedia.org/wiki/Computer_algebra#Simplificatio... Rewriting: https://en.wikipedia.org/wiki/Rewriting https://en.wikipedia.org/wiki/Rewriting Because the rulesets are expected to change, rules engines have functionality to compile rules into a tree or better for performance. eBPF is not a rules engine, but it does optimize filter sets IIRC?
  - staunton 3y ago
    Julia's Symbolics.jl allows users to easily add custom rewrite rules. However, it's not a state-of-the-art CAS. I don't have that much experience with others. Mathematica doesn't allow it, I think.
    - westurner 3y ago
      FWIU Wolfram's searching for a unified model with the Wolfram Physics Project, too; e.g. "The Physicalization of Metamathematics and Its Implications for the Foundations of Mathematics" (2022) https://www.wolframscience.com/metamathematics/ https://www.wolframscience.com/metamathematics/ https://www.wolframphysics.org/bulletins/ https://www.wolframphysics.org/bulletins/ Are fundamental constants other-valued in any Many Worlds interpretations, or are e, i, and Pi always e, i, and pi with the same relations? Countability and continuua (in a Hilbert space of degree n, where n is or is not inconstant like the many forms of [quantum discord] entropy and the energy that represents them) TIL the separable states problem is considered NP-hard, and many models specify independence of observation as necessary.
      - staunton 3y ago
        I don't see how that relates to the question of "does Mathematica allow users to define simplification rules?"
        westurner 3y ago
        https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g... : > In this game, you get own version of the natural numbers, called `mynat`, in an interactive theorem prover called Lean. Your version of the natural numbers satisfies something called the principle of mathematical induction, and a couple of other things too (Peano's axioms). Such axioms are hard-coded in SymPy, SageMath, and Mathematica but not in Lean Mathlib (which is not optimized for performance) If there are an infinite number of unitary transformations (as rotations on a Bloch sphere for example), I find it unlikely that we've yet discovered all of the requisite operators and axioms and coded them into any human CAS that exists in present day.

zozbot234 3y ago

Typically, there are 'group', 'ring' and 'field' tactics that will perform simplification in the relevant algebraic structures. Going from that to solving sin^2 x + cos^2 x is simply a matter of writing more such tactics, operating on e.g. real fields or whatever is applicable in any given case. This is a lot less ad-hoc than whatever CAS's do, but it's also less error prone.

westurner 3y ago
Do any existing CAS systems have configurable axioms? OTOH: Conway's surreal infinities, Do not early eliminate terms next to infinity, Each instance of infinity might should have a unique identity, configurable Order of operations, All of the axiomatic transformations applied by a CAS like SymPy should/must be in Lean Mathlib somewhere? If nothing else, a lookup_lean_mathlib_definition(expr, 'path/to/mathlib-v0.0.2') or find_similar(expr, AxiomDB) would be useful. How do CAS differ from Production Rule Systems? https://en.wikipedia.org/wiki/Production_system_(computer_science) https://en.wikipedia.org/wiki/Production_system_(computer_sc... CAS > Simplification: https://en.wikipedia.org/wiki/Computer_algebra#Simplification https://en.wikipedia.org/wiki/Computer_algebra#Simplificatio... Rewriting: https://en.wikipedia.org/wiki/Rewriting https://en.wikipedia.org/wiki/Rewriting Because the rulesets are expected to change, rules engines have functionality to compile rules into a tree or better for performance. eBPF is not a rules engine, but it does optimize filter sets IIRC?
- staunton 3y ago
  Julia's Symbolics.jl allows users to easily add custom rewrite rules. However, it's not a state-of-the-art CAS. I don't have that much experience with others. Mathematica doesn't allow it, I think.
  - westurner 3y ago
    FWIU Wolfram's searching for a unified model with the Wolfram Physics Project, too; e.g. "The Physicalization of Metamathematics and Its Implications for the Foundations of Mathematics" (2022) https://www.wolframscience.com/metamathematics/ https://www.wolframscience.com/metamathematics/ https://www.wolframphysics.org/bulletins/ https://www.wolframphysics.org/bulletins/ Are fundamental constants other-valued in any Many Worlds interpretations, or are e, i, and Pi always e, i, and pi with the same relations? Countability and continuua (in a Hilbert space of degree n, where n is or is not inconstant like the many forms of [quantum discord] entropy and the energy that represents them) TIL the separable states problem is considered NP-hard, and many models specify independence of observation as necessary.
    - staunton 3y ago
      I don't see how that relates to the question of "does Mathematica allow users to define simplification rules?"
      - westurner 3y ago
        https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g... : > In this game, you get own version of the natural numbers, called `mynat`, in an interactive theorem prover called Lean. Your version of the natural numbers satisfies something called the principle of mathematical induction, and a couple of other things too (Peano's axioms). Such axioms are hard-coded in SymPy, SageMath, and Mathematica but not in Lean Mathlib (which is not optimized for performance) If there are an infinite number of unitary transformations (as rotations on a Bloch sphere for example), I find it unlikely that we've yet discovered all of the requisite operators and axioms and coded them into any human CAS that exists in present day.