[CakeML] Equality

Konrad Slind konrad.slind at gmail.com
Tue May 20 16:27:16 UTC 2014


 OK. From the previous discussion it seems that cakeML provides
implementations for equality, when it can. My question arose in a
situation where I am working in HOL and using the HOL->cakeML
translator. This brings me to a related question: since logical equality
is much more powerful than computational equality could it be that
a program is proved correct but that the generated equality code
isn't enough to enforce the property?

Konrad.





On Tue, May 20, 2014 at 6:53 AM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>wrote:

> (This kind of question could go on the non-private currently very-quiet
> users at cakeml.org list :))
>
>
> On Mon, May 19, 2014 at 11:27 PM, Konrad Slind <konrad.slind at gmail.com>wrote:
>
>> Very good!   --Konrad.
>>
>>
>>
>> On Mon, May 19, 2014 at 5:11 PM, Scott Owens <S.A.Owens at kent.ac.uk>wrote:
>>
>>> 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).
>>>
>>> -Scott
>>>
>>> On 2014/05/19, at 22:54, Konrad Slind <konrad.slind at gmail.com> wrote:
>>>
>>> > Hi all,
>>> >
>>> >   In the regexp compiler I have a test to see whether something
>>> > on the worklist has already been seen. This has the form
>>> >
>>> >    if MEM r seen then ... else ...
>>> >
>>> > How do the translator and cakeML handle MEM? Should I instead write
>>> > a version of MEM parameterized by a regexp equality predicate?
>>> >
>>> > Thanks,
>>> > Konrad.
>>> >
>>>
>>>
>>
>> _______________________________________________
>> Dev mailing list
>> Dev at cakeml.org
>> https://lists.cakeml.org/listinfo/dev
>>
>>
>
> _______________________________________________
> Dev mailing list
> Dev at cakeml.org
> https://lists.cakeml.org/listinfo/dev
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20140520/40b95c94/attachment.html>


More information about the Users mailing list