[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Axiom Sane musings (SEL4)
From: |
Henri Tuhola |
Subject: |
Re: [Axiom-developer] Axiom Sane musings (SEL4) |
Date: |
Fri, 20 Sep 2019 20:31:46 +0300 |
I doubt it does cover that. And I think there would be at least two
approaches to implement GCD for polynomials in Idris.
Obvious approach would be to construct a type that represents
polynomials on some base number and variables. For example,
(Polynomial Nat [X]). You would then prove GCD for this structure.
Another approach I can think of would exploit the way how
type-propositions themselves can cause computer-algebra-system -like
behavior, reusing variables that the type system is already working
with. You can prove (a = b) -> (b = c) -> (a = c), then compose
equations together with that. Similarly you can rewrite x to y inside
a type if you have (x = y). There's already some support for changing
the behavior of Idris type checker, it could be that some sort of
equation simplifier could be implemented with features that Idris
already has.
-- Henri Tuhola
- [Axiom-developer] Axiom Sane musings (SEL4), Tim Daly, 2019/09/20
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Henri Tuhola, 2019/09/20
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Tim Daly, 2019/09/20
- Re: [Axiom-developer] Axiom Sane musings (SEL4),
Henri Tuhola <=
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Tim Daly, 2019/09/20
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Martin Baker, 2019/09/21
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Henri Tuhola, 2019/09/21
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Martin Baker, 2019/09/21
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Tim Daly, 2019/09/21
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Martin Baker, 2019/09/22
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Tim Daly, 2019/09/22
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Veer Singh, 2019/09/24
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Tim Daly, 2019/09/25