Hi Juan,
> These ideas are very interesting. I first though that you were refering
> to computing the inverse of a function, but now I understand that you
> are trying to compute the complement of a the set of values
> corresponding to a non-deterministic expression, where the universe of
> the set of values of the type of that expression.
Not quite (see my response to Wolfgang). I propose to extend the
universe to also include anti-results. The meaning of (?) in the new
universe is analogous to the meaning of addition on the integers (where,
for example, 4-7 is not 0 but -3).
> oddNat -> nat `butNot` evenNat -> nat ? inv evenNat -> nat ->* Z
No, but using the laws from my response to Wolfgang one can reason like
this
oddNat = nat `butNot` evenNat
= nat ? anti evenNat
= Z ? S nat ? anti (Z ? S (S evenNat)))
= S nat ? Z ? anti Z ? anti (S (S evenNat))
= S nat ? failure ? anti (S (S evenNat))
= S nat ? anti (S (S evenNat))
= S (Z ? S nat) ? anti (S (S evenNat))
= S Z ? S (S nat) ? anti (S (S evenNat))
= S Z ? S (S nat) ? S (S (anti evenNat))
= S Z ? S (S (nat ? anti evenNat))
= S Z ? S (S (nat `butNot` evenNat))
= S Z ? S (S oddNat)
The last line does not use anti and could be used as an alternative
definition. In this case, this definition is as simple as the original
one. I'd like to see examples where this is not the case.
> Switching to Toy, maybe we can do something in this line by using
> disequality constraints. [...] And maybe we could use (\) to define 'anti' as
>
> anti :: A -> A
> anti X = Y \ X
This definition does not make `anti a` an inverse of a so the laws would
be a little different. The main difference is that `butNot` is different
from set difference (no pun intended).
Using the predicate negation from my response to Wolfgang, one can
define a dis-equality constraint as
(=/=) :: a -> a -> Success
x =/= y = neg (x =:= y)
However, my implementation does not have logic variables, only
nondeterminism and anti, so (=/=) is not as efficient as it could be.
> I do not understand this point
> > Using the analogy of natural numbers with addition this is
> >
> > NAT + (-EVEN)
> >
> > which corresponds to
> >
> > nat ? anti evenNat
>
> But if we think about (?) and 'anti' like the set operators U (union)
> and \ (difference), then 'nat ? anti evenNat' is like
>
> nat U (nat \ even) = nat
Thinking of (?) as set union and anti as set difference is misguided.
Think about representing natural numbers as multisets that can only
contain some value # but multiple times. For example 4 is {#,#,#,#}. In
this model addition on natural numbers is multi-set union. If you extend
this to negative numbers, the universe contains pairs like
({#,#},{#,#,#})
which is one representative of the equivalence class that denotes the
integer -1. Negation and addition are defined on these pairs as
-(A,X) = (X,A)
(A,X) + (B,Y) = (A \union B, X \union Y)
and lifted to equivalence classes by combining some representatives.
> Does really (?) behave like some kind of addition, or like some
> kind of set union operator?
The implementations of anti and (?) in the extended universe are similar
to the extended negation and addition above.
> Which is the behaviour in concrete FLP systems?
I think the behaviour can be analyzed using the laws from my response to
Wolfgang (I have not proved this yet).
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Do Dez 16 2010 - 13:41:29 CET