further examples:
4. (a b c => d) U (a =>b -> c -> d) = _|_
5. (a -> b -> c -> d) U (a => b -> c -> d) = (a => b -> c => d)
6. (a => b -> c -> d) U (a => b -> c -> d) = (a => b ->c => d)
7. (a => b => c -> d) U (a => b -> c -> d) = (a => b => c => d)
8. (a => b => c => d) U (a => b -> c -> d) = (a => b => c => d)
9. (a => b c => d) U (a => b -> c -> d) = (a => b c => d)
The unification rules (to be applied recursively
1. a U (b -> c) = {a = b -> c} (b -> c)
2. a U (b => c) = {a = b => c} (b => c)
3. (a -> b) U (c -> d) | either b or d are not a function = {a U c, b U d}
(a => b)
| otherwise {a U c, b U d} (a -> b)
4. (a -> b) U (c => d) = {a U c, b U d} (a => b)
5. (a => b) U (c => d) = {a U c, b U d} (a => b)
I'm still thinking about it, so would be interested if I have overlooked
something.
Keean.
On 31 March 2015 at 17:13, Keean Schupke <[email protected]> wrote:
> You are right, but I would state it more like, the arrows cannot be plain
> HM arrows if the equations are all true.
>
> Lets assume I was mistaken when I said they are HM arrows, and focus on
> the implications of the equations.
>
> K.
>
>
> On 31 March 2015 at 17:05, Matt Oliveri <[email protected]> wrote:
>
>> On Tue, Mar 31, 2015 at 11:44 AM, Keean Schupke <[email protected]> wrote:
>> > Clarification, so:
>> >
>> > 1. (a -> b -> c -> d) U (a b c => d) = (a b c => d)
>> >
>> > 2. (a -> b) U (a b c => d) = _|_
>> >
>> > 3. (a -> b) U (a -> b -> c -> d) = (a =>b -> c -> d)
>>
>> (x U y) is notation for "unify x with y"? If so, then sorry, but I
>> think you're mistaken. Those equations cannot all be true if the
>> arrows are HM arrows. See my previous email.
>> _______________________________________________
>> bitc-dev mailing list
>> [email protected]
>> http://www.coyotos.org/mailman/listinfo/bitc-dev
>>
>
>
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
