Re: Invertible nondeterminism?

From: Julio Mariņo <jmarino_at_fi.upm.es>
Date: Thu, 16 Dec 2010 15:42:10 +0100

On Thu, Dec 16, 2010 at 2:59 PM, Sebastian Fischer
<sebf_at_informatik.uni-kiel.de> wrote:
> On Thu, 2010-12-16 at 20:22 +0900, Sebastian Fischer wrote:
>> It is an equivalence class of pairs of (multi-)sets for the
>> equivalence relation
>>
>>     (A,X) ~ (B,Y)  :=  A \union Y  =  X \union B
>
> This was incorrect. The correct definition is (writing u for union)
>
>    (A,X) ~ (B,Y) := exists S : A u Y u S  =  X u B u S
>
> As a consequence, if we use sets and not multisets, then every element
> is equivalent to failure. Writing E for empty set:
>
>    (A,X) ~ (E,E) because for S = A u X : A u E u S = S = X u E u S
>
> So, for this construction to be useful, one should consider
> multiplicities of results such that (a ? a) is different from a.
>
> We can also show that every element equals failure if (?) is idempotent
> using the laws:
>
>    a = a ? failure
>      = a ? (a ? anti a)
>      = (a ? a) ? anti a
>      = a ? anti a
>      = failure

Hmmm, that looks different from the typical constructive negation
interpretation... negation would subtract a given amount of copies of
positive results...

7 ? 7 ? inv 7 = 7 = 7 ? inv 7 ? 7

IMHO this makes it more interesting mathematically, but less
attractive as a programming tool.

Julio

> Sebastian
>
> _______________________________________________
> curry mailing list
> curry_at_lists.RWTH-Aachen.DE
> http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
>

_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Thu Dec 16 2010 - 16:50:47 CET

This archive was generated by hypermail 2.3.0 : Mon Sep 16 2019 - 07:15:07 CEST