|
From: | Martin Baker |
Subject: | Re: [Axiom-developer] Axiom Sane musings (SEL4) |
Date: | Sat, 21 Sep 2019 16:38:01 +0100 |
User-agent: | Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.8.0 |
On 21/09/2019 13:40, Henri Tuhola wrote:
The elaborator reflection also allows accessing the term rewriting. I suppose that's all you need in order to write a program that simplifies equations inside the type context?
I am trying to understand if these equations could be solved in this way?I think Axiom equation solving tends to work in terms of reals and complex numbers. I suspect that a type that depends on a floating point literal would be problematic in that the equality could fail due to a rounding error.
Also, although I never understood it, I get the impression that Axiom equation solving is extremely complicated. First representing it as functions within polynomials within functions an so on, then expressing the multivariate polynomials in terms of a single variable. I've probably got this all wrong but the point is: could elaborator reflection handle this level of complexity?
If these kinds of thing can't be done in the type system then I guess they would have to be handled differently from equations in proofs.
Martin
[Prev in Thread] | Current Thread | [Next in Thread] |