Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.
|
|
|
|
Internal Language of Categories with Strong Natural Number Object
Posted:
Oct 13, 2011 8:07 AM
|
|
Buried in the theory of Closed Cartesian Categories (CCC) with strong
natural number objects is an analogue of the differential and integral
calculus, complete with its own analogue of the "rules for
differentiation" as well as an analogue of the "Fundamental Theorem of
Calculus". Some of this structure will be unfolded here.
1. THE ISSUE
In Scott and Lambek ("Introduction to Higher Order Categorical Logic",
Cambridge Studies in Advanced Mathematics, 7, 1986) the comment
appears:
"We would have preferred to state Theorem 11.3 for strong natural
numbers objects in Lawvere's sense. Unfortunately, we do not yet know
how to handle the corresponding notion in typed lambda-calculus
equationally."
It's the then-unsolved uncovering of this hidden structure that they
were alluding to.
2. THE BACKGROUND
First, the context of the remark...
It is in a discussion of the evolution and history of the Curry-
Howard(-DeBruijn) correspondence. Lawvere's name came up in the
remark, since he was mentioned as one of those who (like Gentzen) had
early on reinstated the standing of the logical connectives as first-
class citizens, revoking the tendency in the earlier mathematics and
logic literature to reduce everything to the conditional and negation.
This eventually tied in with the appearance of CCC's into the mix by
way of the Rosetta stone:
true <-> Terminal Object 1
A and B <-> Product A x B
if A then B <-> Exponential B^A
The introduction by Church of the "Church numerals", over time,
evolved into the notion of the "weak natural number object" N, whose
defining features were the admission the following:
* Arrows O: 1 -> N, S: N -> N
* Existence of iterators g: N -> A for each p: 1 -> A, h: A -> A
such that g.S = h.g and g.O = p where I'm using ().() to denote
composition.
A strong natural number object has each p and h associated with a
unique solution g.
As Scott and Lambek mentioned, Goedel's "functionals of finite type"
foreshadowed this notion of what eventually came to be called
"prerecursive categories" (by Marie-France Thibault).
The "internal language" of such a category, C, is obtained by way of
the natural functor {C}: C -> Set, given for any small category C with
terminal object 1 by:
* {C}: A |-> C(1, A) = morphism class of 1->A arrows in C
* {C}f: p in C(1, A) |-> f.p in C(1, B) if f: A -> B.
The authors' Theorem 11.3 is the construction of the equivalent
representation of the CCC with weak natural number object via its
internal language. They constructed a typed lambda calculus with a
product type, "surjective pairing" and an "iterator" and the
equivalence result.
(Surjective pairing is the property that any element c of type A x B
is expressible as c = (Lc, Rc) where L: A x B -> A and R: A x B -> B
are the projections associated with the product).
So, that's the context of the above remark and the open problem it
alludes to.
3. THE INTEGRAL OPERATOR
A little thought reveals the minimum that is required to resolve the
problem alluded to by Scott and Lambek.
First, each h: A -> A and p: 1 -> A must be associated with a unique
g: N -> A such that
g.O = p
g.S = h.g.
To clarify further discussion, I will use the following notion to
denote the "elements" of the "type" {C}A, where {C}: C -> Set is the
natural functor for the category C:
*p: A where p: 1 -> A
&a: 1 -> A where a: A
such that
&*p = p, and *&a = a.
Define 0 = *O, and define function application by
f: A -> B, a: A ==> fa = *(f.&a): B
Then the conditions on g can be stated equivalently by:
g0 = a, g(Sn) = h(gn), where n: N.
These conditions are analogous to those which characterize the
definite integral. Therefore, denote the solution by:
g = integral_a h.
Thus, a CCC with strong natural number object has an "integral"
operation --
* if h: A -> A and a: A then integral_a h: N -> A
* (integral_a h) 0 = a
* for all n: N, (integral_a h)(Sn) = h(integral_a h (n))
4. DIFFERENTIABILITY AND THE DIFFERENTIAL OPERATOR
Let g = integral_a h. To get uniqueness requires that both a and h can
be extracted from g. Part of this is already given to us:
a = g0
The remainder requires that we be able to solve the equation
g.S = (_).g.
Let the solution, if it exists, be denoted dg. Not all arrows g: A ->
A need have such solutions. Therefore, let those arrows which do have
a solution be called "differentiable".
Thus, a CC with strong natural number object also has a "differential"
operation --
* if g: N -> A is differentiable, then dg: A -> A
* for all n: N, g(Sn) = dg(gn).
Thus, from g can be reconstructed a = g0 and h = dg. This leads to the
following result.
The Fundamental Theorem:
if g: N -> A is differentiable, then g = integral_{g0} dg.
So, in order to arrive at a resolution to Scott and Lambek's problem
requires
(a) a determination of when an arrow g: N -> A is differentiable
(b) the formulation for "rules of differentiation" for differentiable
arrows
5. RULES OF DIFFERENTIATION
The non-trivial element here is that a given arrow g: N -> A can be a
composition
g = k.l, where k: B -> A, l: N -> B,
and suppose that g = integral_a h.
If l is differentiable, with dl = m, and if l0 = b, we can write:
a = g0 = k(l0) = kb
h(k(ln)) = h(gn) = g(Sn) = k(l(Sn)) = k(m(ln))
In particular, for n = 0,
h(kb) = k(mb).
So now, this shows we need to be able to obtain h = d_m k: A -> A as
the (unique) solution to k.m = (_).k, where k: B -> A and m: B -> B.
Thus, the need to "differentiate" has to generlize beyond the
successor arrow S: N -> N to arbitrary arrows m: B -> B:
if k: B -> A, m: B -> B and k is m-differentiable, then d_m k: A -> A
Then, one has the
CHAIN RULE:
if l: N -> B is differentiable with m = dl: B -> B
if k: B -> A is m-differentiable
then d(k.l) = d_m k.
I won't carry out this unfolding all the way (much less prove any
equivalence result), but this line of arguments takes the matter far
enough to make it clear that the structure hidden in the internal
language of the CCC with strong number object is nothing less than a
categorical analogue of the the differential and integral calculus,
itself.
|
|
|
|
