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.
Julio
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
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Do Dez 16 2010 - 13:41:29 CET