[CakeML] Equality

[Konrad Slind]

Thanks Ramana,

  I wasn't thinking about function comparison, which is indeed problematic.
My worry (currently) is about equivalence class reasoning where logical
steps can prove that non-identical elements are equal. Will try to think
of a decent example.

Konrad.



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

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