Hi,
a while ago Sebastian Fischer posted (among other things) this
interesting program:
inv :: (a -> b) -> (b -> a)
inv f b | f(a) =:= b = a where a free
Let's try to give it a precise semantics when applied to total functions
with a discrete codomain.
We first observe that when a pure function (f :: a -> b) isn't *onto*
then ((inv f) :: b -> a) is a partial function defined only on a subset
of the set of all elements of type b.
And second when (f :: a -> b) isn't *one-to-one* then
((inv f) :: b -> a) is non-deterministic, returning subsets of the set
of all elements of type a.
Making this explicit with an /inverse image/ operation couldn't be
easier.
type Sub a = a -> Success
(*) :: (a -> b) -> (Sub b -> Sub a)
(f* v) a = v(f(a))
But since Curry supports existential quantification via free variables
we can also do this in the other direction with a /direct image/
operation.
(#) :: (a -> b) -> (Sub a -> Sub b)
(f# u) b = let a free in u(a) & f(a) =:= b
The relation between those two operations is that of an adjunction, i.e.
for any (f :: a -> b), (u :: Sub a) and (v :: Sub b) it holds that the
direct image of u under f is contained in v exactly when u is contained
in the inverse image of v under f.
(f# u) \subset v iff u \subset (f* v)
(If /failed/ is observable in Curry than we must add the condition that
the predicates u,v and the function f don't mention each other, I
think.)
We can now characterise inv with laws like
(f# u) \subset v iff u \subset ((inv f)# v)
What other - probably more interesting - laws are there? I've only just
begun to explore this.
Cheers,
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Mär 07 2008 - 11:45:28 CET