transporting predicates along maps

From: Sebastian Hanowski <>
Date: Fri, 13 Jun 2008 13:42:52 +0200


this is about the three canonical ways to transform predicates with

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

 We have predicates. What are quantifiers then? Predicates on

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

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

curry mailing list
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