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