Uday's question

Uday's question

[Reinhold Heckmann]

When reading the last message of Uday Reddy,
I got three ideas.

1) Several people have pointed out that naturality is impossible.
Yet a weaker form of naturality may be appropriate.
Consider existential quantification on sets.
If f: A -> B is a function and p: B -> M (= Bool) a predicate,
then  exists x in A: p(fx)  iff  exists x in f(A): p x
This suggests to require naturality  E_A (p o f) = E_B p
for *epis*  f: A -> B  only.

2)  Uday Reddy asked about the significance of the third equation:
    E_A(\x. E_B(\y.hxy))  =  E_B(\y. E_A(\x.hxy))
This equation looks a bit like the Foubini theorem
in integration theory.
The difference is that in Foubini's theorem,
there is a third mediating term, whose analogue would be
    E_(A x B) (\(x,y). hxy) .
[Distinguish the product symbol x in A x B from the variable x.]

3) The analogy with integration also shows that
something may be missing from the present setting:
The integral depends on the function to be integrated
and also on a measure.  It is in fact an operator
    I_A: [A->M] x M(A) -> M
where M are the (non-negative?) reals
with the multiplicative monoid structure,
and M(A) is the set of measures on A.
[Distinguish the operator M from the monoid M.
 Yet there is some connection: M(1) = M
 if M is taken to consist of the non-negative reals.]

Now, we get
         I_A(\x. a * gx, m)  =  a * I_A(g, m)
         I_A(\x. gx * a, m)  =  I_A(g, m) * a
by linearity of integration, and
         I_A(\x.1, m) = m(A)
(= 1, if only normalised measures are considered, but then M = M(1) is lost)
Of course, integration has many more properties, e.g.
additivity in the function, and linearity in m.

The last equation becomes
  I_A (\x. I_B (\y. hxy, mb), ma) = I_B (\y. I_A (\x. hxy, ma), mb)
  =  I_(A x B) (\(x,y). hxy, ma x mb)   with the product measure ma x mb.

There is also kind of naturality, namely the law of substitution:
For  f: A -> B,  I_A (p o f, ma) = I_B (p, ma o f^-1)
	(for  p: B -> M  and  ma in M(A) ).
This becomes a bit more categorical
by noting that  M(-)  is a functor  with  M(f) (ma) = ma o f^-1
and so   I_A ( [f->] p, ma) = I_B (p, M(f) ma) .

Much of this can be formulated abstractly with a functor M.
For the mediating term of the Foubini theorem,
a natural transformation  x_AB: M(A) x M(B) -> M(AxB)  is needed
to form the product measure.

It may be useful to introduce a natural transformation
eta_A: A -> M(A), giving point measures.
    I_A (p, eta_A(x)) = p(x)  holds for p: A -> M  and  x in A.

The transformation x_AB induces a binary operation on  M(1) = M(1 x 1),
and for  1 = {()},  eta_1 ()  is an element of  M(1).
This gives a monoid structure on M(1),
giving back the original monoid M.

Back to existential quantification:
===================================
Take  M(A) = P(A), the powerset of A,  and M = P(1) = Bool
and define  E_A (p, S) = exists x in S: p(x)
for  p: A -> M  and  S in P(A).
Then all the equations for integration hold
(with  x_AB : P(A) x P(B) -> P(A x B)  being cartesian product
 and  eta_A(x) = {x} )

Instead of considering  E_A: [A->M] x P(A) -> M,
one may, using CC, also consider  E'_A: P(A) -> [[A->M]->M] .
This is even a monad homomorphism from the power set monad
to the monad  [[- -> M] -> M]  (known as continuation monad
with "final answers" M).

A similar thing is possible in the category of domains,
with P being some power domain construction
(see my paper  "Power Domains and Second Order Predicates",
 TCS 111, 59 - 88 (1993) ).

Maybe, this is the essence of Uday's work:
defining a monad homomorphism from some monad used
in the semantic description of a language to the continuation monad.

Regards,
Reinhold Heckmann
Universitaet des Saarlandes