Re: Invertible nondeterminism?

From: Wolfgang Lux <>
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.


curry mailing list
Received on Do Dez 16 2010 - 11:42:05 CET

This archive was generated by hypermail 2.3.0 : Di Sep 29 2020 - 07:15:03 CEST