# the semantics of inv :: (a -> b) -> (b -> a)

From: Sebastian Hanowski <sebastian.hanowski_at_web.de>
Date: Fri, 07 Mar 2008 11:23:17 +0100

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

This archive was generated by hypermail 2.3.0 : Di Sep 29 2020 - 07:15:03 CEST