# Re: Invertible nondeterminism?

From: Juan Rodriguez Hortala <juanrh_at_fdi.ucm.es>
Date: Thu, 16 Dec 2010 12:32:44 +0100

Hi Sebastian,

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. But then I do not
understand why do you characterize anti (I also prefer that name) by
'anti a ? a = failure'. Because to me the operator (?) corresponds to
set union, not set interesection, which seems to be more appropiate in
this context. Maybe another characterization could be that the
intersection between the total parts of the denotations of 'a' and 'anti
a' would be the empty set, for any expression a.

Regarding your definition of oddNat, again I do not understand the use
of the operator (?). With your definition you can do

oddNat -> nat `butNot` evenNat -> nat ? inv evenNat -> nat ->* Z

Switching to Toy, maybe we can do something in this line by using
disequality constraints. We can define a function to filter some values
in the denotation of an expression

filterV :: (A -> bool) -> A -> A
filterV F X = if F X then X

We can use this function to try to define the set difference operator
for expressions, which makes the set difference of the denotation of
those expression
(\) :: A -> A -> A
S1 \ S2 = filterV (/= S2) S1

Note the use of the disequality constraint operator (/=). With this we
can define

oddNat = nat \ (anti nat)

for which

oddNat -> nat \ (anti nat) -> filterV (/= (anti nat)) nat -> let X = nat
in if X /= anti nat then X

Probably this definition is not complete, but I think it is an
approximation. And maybe we could use (\) to define 'anti' as

anti :: A -> A
anti X = Y \ X

Note the use of the free variable Y

Greetings,

Juan

```--
------------------------------------------------------------------------
Juan Rodríguez Hortalá
Grupo de Programación Declarativa / Declarative Programming Group
E-Mail : juanrh_at_fdi.ucm.es
Tel: + 34 913947646
Despacho / Office: 220 (2ª planta / 2nd floor)
Dept. Sistemas Informáticos y Computación / Department of Computer Systems and Computing