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

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.

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

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.

Julio

On Thu, Dec 16, 2010 at 8:34 AM, Sebastian Fischer

<sebf_at_informatik.uni-kiel.de> wrote:

_______________________________________________

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

*
This archive was generated by hypermail 2.3.0
: So Jan 26 2020 - 07:15:11 CET
*