<div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, May 23, 2019 at 9:42 AM Philipp Hausmann <<a href="mailto:philipp.hausmann@314.ch">philipp.hausmann@314.ch</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
  
    
  
  <div bgcolor="#FFFFFF">
    Hi<br>
    <br>
    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?<br>
    <br></div></blockquote><div>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.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div bgcolor="#FFFFFF">
    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.<br>
    <br></div></blockquote><div><br></div><div>I agree that they are useful, maybe then find a way to be explicit about the method of their computation.</div><div>This touches a difficult subject that I haven't made my mind.</div></div><div class="gmail_quote"><br></div><div class="gmail_quote">There are two types of knowledge, knowledge that can be arrived through computation and knowledge that can be arrived through proofs.</div><div class="gmail_quote">Agda is a theorem proof assistant, but maybe we need to introduce computational methods during typechecking.</div><div class="gmail_quote"><br></div><div class="gmail_quote">examples : <br></div><div class="gmail_quote">1. Computation of Reals on the CPU instead of the mathematical notion of Real.</div><div class="gmail_quote">2. Tests , model checking.</div><div class="gmail_quote">3. All types of other computational methods , like numerical solutions to differential equations, image processing, neural networks, etc.<br></div><div class="gmail_quote"><div><br></div><div>One could use the result of computational methods into proofs to derive a result.</div><div><br></div><div>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</div><div>to the mathematical theorem that says that such a surface would be homeomorphic to S^2.</div><div><br></div><div>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?</div><div>And one should be interested in the reusability of the proofs by others.<br></div><div> </div><div>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.</div><div><br></div><div>(As you can see, my answer was actually a question , I do not have a solution.)<br></div><br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div bgcolor="#FFFFFF">
    I feel my comment from #3749 also applies here:<br>
    <p>
      </p><blockquote type="cite">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 <i>for now</i> because they are the most portable
        ones and let libraries experiment with packaging it up or adding
        different implementations? [2]<br>
      </blockquote>
    <p></p>
    <br>
    Cheers<br>
    Philipp<br>
    <br>
    [1] <a class="gmail-m_7417526232320060584moz-txt-link-freetext" href="https://github.com/agda/agda/issues/2194#issuecomment-251525747" target="_blank">https://github.com/agda/agda/issues/2194#issuecomment-251525747</a><br>
    [2] <a class="gmail-m_7417526232320060584moz-txt-link-freetext" href="https://github.com/agda/agda/issues/3749#issuecomment-489795629" target="_blank">https://github.com/agda/agda/issues/3749#issuecomment-489795629</a><br>
    <p><br>
    </p>
    <div class="gmail-m_7417526232320060584moz-cite-prefix">On 5/23/19 1:22 AM, Apostolis
      Xekoukoulotakis wrote:<br>
    </div>
    <blockquote type="cite">
      
      <div dir="ltr">
        <div>I was trying to support floats in agda-ocaml when I
          realized that this is a lost cause and a very dangerous one.</div>
        <div><br>
        </div>
        <div>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.</div>
        <div><br>
        </div>
        <div>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.</div>
        <div><br>
        </div>
        <div>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.</div>
        <div><br>
        </div>
        <div>Is it the job of agda to check whether two hardware or
          software versions have the same computational results? Of
          course not.</div>
        <div><br>
        </div>
        <div>In my opinion, all platform dependent computations should
          be inserted as postulates. This way, agda will do exactly what
          it was programmed to do.</div>
        <div><br>
        </div>
        <div>And we can still prove things for postulates.</div>
        <div><br>
        </div>
        <div>```</div>
        <div>open import Common.Integer<br>
          open import Agda.Builtin.Equality<br>
          <br>
          postulate<br>
            Float : Set<br>
            d : Float<br>
            round : Float → Integer<br>
          <br>
          f : round d ≡ round d<br>
          f = refl<br>
        </div>
        <div>```<br>
        </div>
      </div>
      <br>
      <fieldset class="gmail-m_7417526232320060584mimeAttachmentHeader"></fieldset>
      <pre class="gmail-m_7417526232320060584moz-quote-pre">_______________________________________________
Agda mailing list
<a class="gmail-m_7417526232320060584moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a class="gmail-m_7417526232320060584moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
  </div>

_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div></div>