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

From: Sebastian Hanowski <sebastian.hanowski_at_web.de>

Date: Fri, 13 Jun 2008 13:42:52 +0200

Hi,

this is about the three canonical ways to transform predicates with

functions.

Allow an abbreviation for the type of predicates:

type P a = a -> Success

(You can read 'P' as powerset)

Now, given a /pure/ (deterministic, total) function (f :: a -> b) you

can always move a predicate (v :: P b) *backwards* along f

(*) :: (a -> b) -> (P b -> P a)

(f* v) a = v(f(a))

giving a predicate holding for all those elements of a which get mapped

to elements of b such that v holds. This computes the /inverse image/ of

v.

We have predicates. What are quantifiers then? Predicates on

predicates!

type Q a = (a -> Success) -> Success

And in Curry the /existential quantifier/ comes for free:

exists :: Q a

exists(p) = let a free in p(a)

Settheoretically this allows to move a subset *along* with a map:

f? u = { b | there exists an a with u(a) and f(a) = b }

And this has a straightforward encoding in Curry,

(?) :: (a -> b) -> (P a -> P b)

(f? u) b = exists(\a -> u(a) & f(a) =:= b)

giving the /direct image/ of all those elements for which u holds.

We cannot hope to define a 'generic' /universal quantifier/ as well,

because this is only possible for /compact/ spaces of data.

forAll :: Q a

forAll = unknown

However, in set theory a subset also gets moved /covariantly/ with the

help of the /universal quantifier/:

f! u = { b | for all a, if f(a) = b, then u(a) }

And this just says that (f! u) consists of all those elements whose

complete preimage under f is covered by u.

So, under the condition that f must map only finitely many elements of a

to every element of b, I was wondering whether one can have the above as

this:

(!) :: (a -> b) -> (P a -> P b)

(f! u) b = foldr ((&) . u) success (findall(\a -> f(a) =:= b))

Cheers,

Sebastian

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on Fr Jun 13 2008 - 15:46:04 CEST

Date: Fri, 13 Jun 2008 13:42:52 +0200

Hi,

this is about the three canonical ways to transform predicates with

functions.

Allow an abbreviation for the type of predicates:

type P a = a -> Success

(You can read 'P' as powerset)

Now, given a /pure/ (deterministic, total) function (f :: a -> b) you

can always move a predicate (v :: P b) *backwards* along f

(*) :: (a -> b) -> (P b -> P a)

(f* v) a = v(f(a))

giving a predicate holding for all those elements of a which get mapped

to elements of b such that v holds. This computes the /inverse image/ of

v.

We have predicates. What are quantifiers then? Predicates on

predicates!

type Q a = (a -> Success) -> Success

And in Curry the /existential quantifier/ comes for free:

exists :: Q a

exists(p) = let a free in p(a)

Settheoretically this allows to move a subset *along* with a map:

f? u = { b | there exists an a with u(a) and f(a) = b }

And this has a straightforward encoding in Curry,

(?) :: (a -> b) -> (P a -> P b)

(f? u) b = exists(\a -> u(a) & f(a) =:= b)

giving the /direct image/ of all those elements for which u holds.

We cannot hope to define a 'generic' /universal quantifier/ as well,

because this is only possible for /compact/ spaces of data.

forAll :: Q a

forAll = unknown

However, in set theory a subset also gets moved /covariantly/ with the

help of the /universal quantifier/:

f! u = { b | for all a, if f(a) = b, then u(a) }

And this just says that (f! u) consists of all those elements whose

complete preimage under f is covered by u.

So, under the condition that f must map only finitely many elements of a

to every element of b, I was wondering whether one can have the above as

this:

(!) :: (a -> b) -> (P a -> P b)

(f! u) b = foldr ((&) . u) success (findall(\a -> f(a) =:= b))

Cheers,

Sebastian

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on Fr Jun 13 2008 - 15:46:04 CEST

*
This archive was generated by hypermail 2.3.0
: Fr Jul 10 2020 - 07:15:03 CEST
*