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
Received on Do Dez 16 2010 - 09:22:23 CET