<div dir="ltr"><div>Thanks Ramana,<br><br>  I wasn't thinking about function comparison, which is indeed problematic.<br></div><div>My worry (currently) is about equivalence class reasoning where logical <br>steps can prove that non-identical elements are equal. Will try to think<br>
of a decent example.<br><br></div><div>Konrad.<br><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, May 20, 2014 at 11:33 AM, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">Yes, that is possible.<br><br>You could define a function f in HOL that makes use of logical equality to compare functions extensionally. You could also prove some property P holds of f.<br>


<br>However, when you try to translate f into CakeML, the translator will either fail or will generate a certificate theorem with (unprovable) side-conditions. The translator propagates something like an Equality type-class for all uses of equality and requires them to be at appropriate types so as to be implementable in the CakeML semantics.<br>


</div><div><div class="h5"><div class="gmail_quote"><br>On Tue, May 20, 2014 at 5:27 PM, Konrad Slind <span dir="ltr"><<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

<div dir="ltr"><div><div> OK. From the previous discussion it seems that cakeML provides <br>implementations for equality, when it can. My question arose in a <br>situation where I am working in HOL and using the HOL->cakeML<br>



translator. This brings me to a related question: since logical equality<br></div>is much more powerful than computational equality could it be that<br>a program is proved correct but that the generated equality code<br>


</div>
<div>isn't enough to enforce the property?<span><font color="#888888"><br><br></font></span></div><span><font color="#888888"><div>Konrad.<br><br></div></font></span><div><div>

<div><div><div><br>   <br><div><div><div><div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, May 20, 2014 at 6:53 AM, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br>



<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">(This kind of question could go on the non-private currently very-quiet <a href="mailto:users@cakeml.org" target="_blank">users@cakeml.org</a> list :))<br>



</div><div class="gmail_extra"><br><br><div class="gmail_quote"><div><div>On Mon, May 19, 2014 at 11:27 PM, Konrad Slind <span dir="ltr"><<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>></span> wrote:<br>





</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div><div dir="ltr">Very good!   --Konrad.<br><br></div><div><div><div class="gmail_extra">
<br><br>

<div class="gmail_quote">On Mon, May 19, 2014 at 5:11 PM, Scott Owens <span dir="ltr"><<a href="mailto:S.A.Owens@kent.ac.uk" target="_blank">S.A.Owens@kent.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">This should be fine. The underlying CakeML polymorphic equality will be used, which can be problematic for some types (e.g., those that can contain functions, or that represent sets as various non-canonical tree structures), but should be fine for the regexp type (now that char sets are bitvectors).<br>







<span><font color="#888888"><br>
-Scott<br>
</font></span><div><div><br>
On 2014/05/19, at 22:54, Konrad Slind <<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>> wrote:<br>
<br>
> Hi all,<br>
><br>
>   In the regexp compiler I have a test to see whether something<br>
> on the worklist has already been seen. This has the form<br>
><br>
>    if MEM r seen then ... else ...<br>
><br>
> How do the translator and cakeML handle MEM? Should I instead write<br>
> a version of MEM parameterized by a regexp equality predicate?<br>
><br>
> Thanks,<br>
> Konrad.<br>
><br>
<br>
</div></div></blockquote></div><br></div>
</div></div><br></div></div>_______________________________________________<br>
Dev mailing list<br>
<a href="mailto:Dev@cakeml.org" target="_blank">Dev@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/dev" target="_blank">https://lists.cakeml.org/listinfo/dev</a><br>
<br></blockquote></div><br></div>
<br>_______________________________________________<br>
Dev mailing list<br>
<a href="mailto:Dev@cakeml.org" target="_blank">Dev@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/dev" target="_blank">https://lists.cakeml.org/listinfo/dev</a><br>
<br></blockquote></div><br></div></div></div></div></div></div></div></div></div></div></div>
</blockquote></div><br></div></div></div></div>
</blockquote></div><br></div>