Re: [Axiom-developer] Axiom Sane musings (SEL4)

[Tim Daly]

Axiom has type information everywhere. It is strongly
dependently typed. So give a Polynomial type, which
Axiom has, over a Ring or Field, such as
Polynomial(Integer) or Polynomial(Fraction(Integer))
we can use theorems from the Ring while proving
properties of Polynomials.

Axiom has a deep type hierarchy, all of which can be
inherited by types like Polynomial. The type hierarchy
uses Group Theory as its scaffold.

I'm "decorating" the inherited type hierarchy with axioms.
These will be available by inheritance for Polynomial
proofs. Proving GCD in non-negative integers can assume
that all of the arguments are non-negative integers (i.e. NATs).

There are quite a few GCD algorithms in Axiom.

I'm trying to prove the implemented algorithms for GCD
correct rather than rewrite them.

I've seen a couple of the Idris videos. It looks quite interesting.

Given an Idris proof, is there a "verifier" function?

Tim


On 9/20/19, Henri Tuhola <address@hidden> wrote:
> 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
>