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