- 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 21:13:48 +0900

Hi Juan,

*> These ideas are very interesting. I first though that you were refering
*

*> to computing the inverse of a function, but now I understand that you
*

*> are trying to compute the complement of a the set of values
*

*> corresponding to a non-deterministic expression, where the universe of
*

*> the set of values of the type of that expression.
*

Not quite (see my response to Wolfgang). I propose to extend the

universe to also include anti-results. The meaning of (?) in the new

universe is analogous to the meaning of addition on the integers (where,

for example, 4-7 is not 0 but -3).

*> oddNat -> nat `butNot` evenNat -> nat ? inv evenNat -> nat ->* Z
*

No, but using the laws from my response to Wolfgang one can reason like

this

oddNat = nat `butNot` evenNat

= nat ? anti evenNat

= Z ? S nat ? anti (Z ? S (S evenNat)))

= S nat ? Z ? anti Z ? anti (S (S evenNat))

= S nat ? failure ? anti (S (S evenNat))

= S nat ? anti (S (S evenNat))

= S (Z ? S nat) ? anti (S (S evenNat))

= S Z ? S (S nat) ? anti (S (S evenNat))

= S Z ? S (S nat) ? S (S (anti evenNat))

= S Z ? S (S (nat ? anti evenNat))

= S Z ? S (S (nat `butNot` evenNat))

= S Z ? S (S oddNat)

The last line does not use anti and could be used as an alternative

definition. In this case, this definition is as simple as the original

one. I'd like to see examples where this is not the case.

*> Switching to Toy, maybe we can do something in this line by using
*

*> disequality constraints. [...] And maybe we could use (\) to define 'anti' as
*

*>
*

*> anti :: A -> A
*

*> anti X = Y \ X
*

This definition does not make `anti a` an inverse of a so the laws would

be a little different. The main difference is that `butNot` is different

from set difference (no pun intended).

Using the predicate negation from my response to Wolfgang, one can

define a dis-equality constraint as

(=/=) :: a -> a -> Success

x =/= y = neg (x =:= y)

However, my implementation does not have logic variables, only

nondeterminism and anti, so (=/=) is not as efficient as it could be.

*> I do not understand this point
*

*> > Using the analogy of natural numbers with addition this is
*

*> >
*

*> > NAT + (-EVEN)
*

*> >
*

*> > which corresponds to
*

*> >
*

*> > nat ? anti evenNat
*

*>
*

*> But if we think about (?) and 'anti' like the set operators U (union)
*

*> and \ (difference), then 'nat ? anti evenNat' is like
*

*>
*

*> nat U (nat \ even) = nat
*

Thinking of (?) as set union and anti as set difference is misguided.

Think about representing natural numbers as multisets that can only

contain some value # but multiple times. For example 4 is {#,#,#,#}. In

this model addition on natural numbers is multi-set union. If you extend

this to negative numbers, the universe contains pairs like

({#,#},{#,#,#})

which is one representative of the equivalence class that denotes the

integer -1. Negation and addition are defined on these pairs as

-(A,X) = (X,A)

(A,X) + (B,Y) = (A \union B, X \union Y)

and lifted to equivalence classes by combining some representatives.

*> Does really (?) behave like some kind of addition, or like some
*

*> kind of set union operator?
*

The implementations of anti and (?) in the extended universe are similar

to the extended negation and addition above.

*> Which is the behaviour in concrete FLP systems?
*

I think the behaviour can be analyzed using the laws from my response to

Wolfgang (I have not proved this yet).

Sebastian

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

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

Date: Thu, 16 Dec 2010 21:13:48 +0900

Hi Juan,

Not quite (see my response to Wolfgang). I propose to extend the

universe to also include anti-results. The meaning of (?) in the new

universe is analogous to the meaning of addition on the integers (where,

for example, 4-7 is not 0 but -3).

No, but using the laws from my response to Wolfgang one can reason like

this

oddNat = nat `butNot` evenNat

= nat ? anti evenNat

= Z ? S nat ? anti (Z ? S (S evenNat)))

= S nat ? Z ? anti Z ? anti (S (S evenNat))

= S nat ? failure ? anti (S (S evenNat))

= S nat ? anti (S (S evenNat))

= S (Z ? S nat) ? anti (S (S evenNat))

= S Z ? S (S nat) ? anti (S (S evenNat))

= S Z ? S (S nat) ? S (S (anti evenNat))

= S Z ? S (S (nat ? anti evenNat))

= S Z ? S (S (nat `butNot` evenNat))

= S Z ? S (S oddNat)

The last line does not use anti and could be used as an alternative

definition. In this case, this definition is as simple as the original

one. I'd like to see examples where this is not the case.

This definition does not make `anti a` an inverse of a so the laws would

be a little different. The main difference is that `butNot` is different

from set difference (no pun intended).

Using the predicate negation from my response to Wolfgang, one can

define a dis-equality constraint as

(=/=) :: a -> a -> Success

x =/= y = neg (x =:= y)

However, my implementation does not have logic variables, only

nondeterminism and anti, so (=/=) is not as efficient as it could be.

Thinking of (?) as set union and anti as set difference is misguided.

Think about representing natural numbers as multisets that can only

contain some value # but multiple times. For example 4 is {#,#,#,#}. In

this model addition on natural numbers is multi-set union. If you extend

this to negative numbers, the universe contains pairs like

({#,#},{#,#,#})

which is one representative of the equivalence class that denotes the

integer -1. Negation and addition are defined on these pairs as

-(A,X) = (X,A)

(A,X) + (B,Y) = (A \union B, X \union Y)

and lifted to equivalence classes by combining some representatives.

The implementations of anti and (?) in the extended universe are similar

to the extended negation and addition above.

I think the behaviour can be analyzed using the laws from my response to

Wolfgang (I have not proved this yet).

Sebastian

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

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

*
This archive was generated by hypermail 2.3.0
: Mon Sep 23 2019 - 07:15:08 CEST
*