- 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, 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

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
: Mo Jan 27 2020 - 07:15:10 CET
*