[Agda] Platform Independent proofs.

[Apostolis Xekoukoulotakis]

On Thu, May 23, 2019 at 9:42 AM Philipp Hausmann <philipp.hausmann at 314.ch>
wrote:

> Hi
>
> You are right in so far as the floating point primitives implementation
> needs to exactly match the Haskell implementation used by Agda. Do you have
> a concrete example where this poses a problem?
>
> I will try again today to see if I can match haskell's implementation. But
this will solve the problem of inconsistency, not the problem that the
proofs depend on a specific implementation.


> There are people taking advantage of the fact that Floats can be reasoned
> about [1]. I do think that is a valid use case. This would no longer work
> if Floats were postulates. Note that Agda does not stop you from defining
> your own Float type with postulates. You are also not required to implement
> the float primitives if there is no reasonable way to support them.
>
>
I agree that they are useful, maybe then find a way to be explicit about
the method of their computation.
This touches a difficult subject that I haven't made my mind.

There are two types of knowledge, knowledge that can be arrived through
computation and knowledge that can be arrived through proofs.
Agda is a theorem proof assistant, but maybe we need to introduce
computational methods during typechecking.

examples :
1. Computation of Reals on the CPU instead of the mathematical notion of
Real.
2. Tests , model checking.
3. All types of other computational methods , like numerical solutions to
differential equations, image processing, neural networks, etc.

One could use the result of computational methods into proofs to derive a
result.

example : Given a surface , one could use computational methods to show
that the curvature of the surface is always positive. Then he could inject
that knowledge
to the mathematical theorem that says that such a surface would be
homeomorphic to S^2.

In my opinion, there are many practical benefits in doing that, the
question is how do we do it? How can we be explicit about the computational
techniques we used to derive that proof?
And one should be interested in the reusability of the proofs by others.

I am currently looking into the Wolfram language to find answers to those
questions, but I haven't used it myself. Maybe someone who has could
provide an opinion.

(As you can see, my answer was actually a question , I do not have a
solution.)

I feel my comment from #3749 also applies here:
>
> Is this actually an issue Agda itself needs to solve? Maybe this is a
> problem libraries should solve, as it already today is possible to package
> the Float implementation in a record and provide different implementations.
> Maybe Agda should just provide the single-nan primitives *for now*
> because they are the most portable ones and let libraries experiment with
> packaging it up or adding different implementations? [2]
>
>
> Cheers
> Philipp
>
> [1] https://github.com/agda/agda/issues/2194#issuecomment-251525747
> [2] https://github.com/agda/agda/issues/3749#issuecomment-489795629
>
>
> On 5/23/19 1:22 AM, Apostolis Xekoukoulotakis wrote:
>
> I was trying to support floats in agda-ocaml when I realized that this is
> a lost cause and a very dangerous one.
>
> If I didn't match the exact computational results of haskell, then I could
> get proofs that typechecked in agda that were completely wrong in OCaml.
>
> But there is also a theoretical error in all of this. Right now, we do not
> have universal proofs like in Mathematics. We have platform dependent
> proofs.
>
> In other words, we should write explicitly that this proof is correct for
> this specific version of the CPU, this specific version of haskell etc.
>
> Is it the job of agda to check whether two hardware or software versions
> have the same computational results? Of course not.
>
> In my opinion, all platform dependent computations should be inserted as
> postulates. This way, agda will do exactly what it was programmed to do.
>
> And we can still prove things for postulates.
>
> ```
> open import Common.Integer
> open import Agda.Builtin.Equality
>
> postulate
>   Float : Set
>   d : Float
>   round : Float → Integer
>
> f : round d ≡ round d
> f = refl
> ```
>
> _______________________________________________
> Agda mailing listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190524/b485b54c/attachment.html>