Fwd: Invertible nondeterminism?

From: Julio Mariño <jmarino_at_fi.upm.es>
Date: Thu, 16 Dec 2010 13:33:40 +0100

The idea seems mathematically reasonable and reminds me to
constructive negation in constraint logic programming.

The domain-theory needed for anti-answers would be similar,
apparently, to constructive computed answers in CLP(Herbrand) with
equalities and disequalities, but I am being highly speculative here.


On Thu, Dec 16, 2010 at 8:34 AM, Sebastian Fischer
<sebf_at_informatik.uni-kiel.de> 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.
> 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
> We could define a general combinator for subtraction:
>    butNot :: a -> a -> a
>    butNot x y = x ? inv y
> And define `oddNat` more intuitively as
>    oddNat = nat `butNot` evenNat
> I notice that this example may be misleading because `inv` does not
> construct negative numbers like in my analogy. Instead, `inv` constructs
> anti-results (something that is to results like anti-matter is to
> matter). Incidentally, I happened to demonstrate this using a data type
> for natural numbers.
> I wonder whether anti-results have been proposed before and am
> interested in other examples of using it. (Inspiration could be drawn
> from formal languages that are difficult to define without using
> complement but that have a complement which is easy to define.)
> Sebastian
> P.S. maybe `inv` should be called `anti` instead..
> [1]: Some quotes from
> http://en.wikipedia.org/wiki/Negative_and_non-negative_numbers#History
> For a long time, negative solutions to problems were considered "false".
> In Hellenistic Egypt, Diophantus in the third century A.D. referred to
> an equation that was equivalent to 4x + 20 = 0 (which has a negative
> solution) in Arithmetica, saying that the equation was absurd.
> "A debt cut off from nothingness becomes a credit; a credit cut off from
> nothingness becomes a debt."
> In the 12th century AD in India, Bhāskara II also gave negative roots
> for quadratic equations but rejected them because they were
> inappropriate in the context of the problem. He stated that a negative
> value is "in this case not to be taken, for it is inadequate; people do
> not approve of negative roots."
> In the 15th century, Nicolas Chuquet, a Frenchman, used negative numbers
> as exponents and referred to them as “absurd numbers.” [citation needed]
> In A.D. 1759, Francis Maseres, an English mathematician, wrote that
> negative numbers "darken the very whole doctrines of the equations and
> make dark of the things which are in their nature excessively obvious
> and simple". He came to the conclusion that negative numbers were
> nonsensical.
> In the 18th century it was common practice to ignore any negative
> results derived from equations, on the assumption that they were
> meaningless.
> _______________________________________________
> curry mailing list
> curry_at_lists.RWTH-Aachen.DE
> http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

curry mailing list
Received on Thu Dec 16 2010 - 13:41:29 CET

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