Re: Invertible nondeterminism?

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>
Date: Thu, 16 Dec 2010 20:22:39 +0900

Hi Wolfgang,

On Thu, 2010-12-16 at 11:25 +0100, Wolfgang Lux wrote:
> Hmmm, to me it looks like you are mixing up disjunctions and
> conjunctions (aka don't know and don't care nondeterminism).

I don't think so.

> Regarding
> the set of solutions of a program the *disjunction*
> a ? b
> computes the union of a's solutions and b's solutions.

After including `inv`, which I will from now on call `anti`, the
denotation of an expression is no longer a (multi-)set of results.

It is an equivalence class of pairs of (multi-)sets for the equivalence
relation

    (A,X) ~ (B,Y) := A \union Y = X \union B

> Obviously, this
> set cannot be empty (i.e., a failure) if b has at least one solution.

This is like saying "obviously 'n+m' cannot be 0 if n is positive". In
analogy to the above equivalence classes, the set of integers is
isomorphic to the set of equivalence classes of pairs of natural numbers
for the equivalence relation

    (a,x) ~ (b,y) := a+y = x+b

> What you are asking for here is set subtraction, not set union and
> this confirms my prior suspicion.

The meaning of `butNot` is not set subtraction (or set difference). For
example,

    failure `butNot` True = anti True /= failure

> Considering the set of solutions again you want NAT - EVEN,

In this case, yes, because there is no "debt part" in the result.

> which could be expressed as NAT and (not
> EVEN) - provided that we are able to invert the set even of numbers.

Using the analogy of natural numbers with addition this is

    NAT + (-EVEN)

which corresponds to

    nat ? anti evenNat

> An approximation of inv, namely negation by failure, can be
> implemented with encapsulated search (a fairly trivial exercise), but
> I see no way for general negation of arbitrary predicates.

I have implemented anti-results by constructing the Grothendiek-group of
a nondeterminism monad.

A first useful application of this is, as you point out, negation of
predicates. The following function takes a predicate p and yields a
predicate that succeeds on its argument if p fails on it and vice versa:

    neg :: (a -> Success) -> a -> Success
    neg p x = success `butNot` p x

Thank you, I have not thought of this before!

Rather than thinking in terms of the Grothendiek-construction, one can
reason about programs that involve anti-results using equational laws. I
think one can extend the let-calculus with the following laws:

             a ? anti a = failure (Anti)
           anti (a ? b) = anti a ? anti b (DistrAnti)
             s (anti a) = anti (s a) (AppAnti)
    let x = anti a in b = anti (let x = a in b) (LetAnti)
           anti failure = failure (AntiFail)
          anti (anti a) = a (AntiAnti)

The last two laws follow from the others together with the usual laws.
Another consequence is:

       s (a `butNot` b) = s a `butNot` s b (DistrButNot)

All these laws (except LetAnti) are inspired by corresponding laws for
natural numbers:

     a+(-a) = 0
     -(a+b) = -a + -b
     x*(-a) = -(x*a)
         -0 = 0
      -(-a) = a
    x*(a-b) = x*a - x*b

Do you think the laws are consistent when transferred to
nondeterministic computations as above?

Sebastian

_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Do Dez 16 2010 - 12:40:10 CET

This archive was generated by hypermail 2.3.0 : Do Jun 20 2024 - 07:15:11 CEST