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

From: Wolfgang Lux <wlux_at_uni-muenster.de>

Date: Thu, 16 Dec 2010 11:25:53 +0100

Sebastian Fischer wrote:

*> Hi Sergio,
*

*>
*

*>>> inv a ? a = failure
*

*>>>
*

*>>> for all expressions `a`.
*

*>>
*

*>> Suppose, by way of an example, that a is True. There is no
*

*>> expression b such that b ? True is a failure.
*

*>
*

*> I propose to add a new language primitive `inv` (not to Curry, just in
*

*> imagination) such that `inv True` is such an expression.
*

Hmmm, to me it looks like you are mixing up disjunctions and

conjunctions (aka don't know and don't care nondeterminism). Regarding

the set of solutions of a program the *disjunction*

a ? b

computes the union of a's solutions and b's solutions. Obviously, this

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

*> This is in analogy to taking natural numbers and adding negative
*

*> numbers
*

*> (which where once much more controversial than they are today [1]).
*

*>
*

*>>> Such inversion would allow to restrict nondeterministic
*

*>>> computations not
*

*>>> only using predicates but also by defining another nondeterministic
*

*>>> operation and subtracting its results.
*

*>>
*

*>> I'd like to see an example.
*

*>
*

*> Suppose we define Peano naturals and two nondeterministic operations
*

*> that yield an arbitrary number and an even number respectively:
*

*>
*

*> data Nat = Z | S Nat
*

*> nat = Z ? S nat
*

*> evenNat = Z ? S (S evenNat)
*

*>
*

*> With `inv` we can define `oddNat` as
*

*>
*

*> oddNat = nat ? inv evenNat
*

What you are asking for here is set subtraction, not set union and

this confirms my prior suspicion. Considering the set of solutions

again you want NAT - EVEN, which could be expressed as NAT and (not

EVEN) - provided that we are able to invert the set even of numbers.

That would be something like

nat & inv evenNat

in Curry.

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.

Regards,

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Thu Dec 16 2010 - 11:42:05 CET

Date: Thu, 16 Dec 2010 11:25:53 +0100

Sebastian Fischer wrote:

Hmmm, to me it looks like you are mixing up disjunctions and

conjunctions (aka don't know and don't care nondeterminism). Regarding

the set of solutions of a program the *disjunction*

a ? b

computes the union of a's solutions and b's solutions. Obviously, this

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

What you are asking for here is set subtraction, not set union and

this confirms my prior suspicion. Considering the set of solutions

again you want NAT - EVEN, which could be expressed as NAT and (not

EVEN) - provided that we are able to invert the set even of numbers.

That would be something like

nat & inv evenNat

in Curry.

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.

Regards,

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Thu Dec 16 2010 - 11:42:05 CET

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