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 Do Dez 16 2010 - 11:42:05 CET