- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

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 Thu Dec 16 2010 - 12:40:10 CET

Date: Thu, 16 Dec 2010 20:22:39 +0900

Hi Wolfgang,

On Thu, 2010-12-16 at 11:25 +0100, Wolfgang Lux wrote:

I don't think so.

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

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

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

example,

failure `butNot` True = anti True /= failure

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

Using the analogy of natural numbers with addition this is

NAT + (-EVEN)

which corresponds to

nat ? anti evenNat

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 Thu Dec 16 2010 - 12:40:10 CET

*
This archive was generated by hypermail 2.3.0
: Wed Sep 18 2019 - 07:15:08 CEST
*