[CakeML] Equality

[Ramana Kumar]

Yes, that is possible.

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.

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.

On Tue, May 20, 2014 at 5:27 PM, Konrad Slind <konrad.slind at gmail.com>wrote:

>  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/cce3b932/attachment.html>