- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>

Date: Thu, 16 Dec 2010 16:34:39 +0900

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

Date: Thu, 16 Dec 2010 16:34:39 +0900

Hi Sergio,

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]).

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

*
This archive was generated by hypermail 2.3.0
: Mo Okt 26 2020 - 07:15:05 CET
*