Drexel dragonThe Math ForumDonate to the Math Forum

Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.

Math Forum » Discussions » sci.math.* » sci.math.research

Topic: Internal Language of Categories with Strong Natural Number Object
Replies: 0  

Advanced Search

Back to Topic List Back to Topic List  
Rock Brentwood

Posts: 116
Registered: 6/18/10
Internal Language of Categories with Strong Natural Number Object
Posted: Oct 13, 2011 8:07 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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.

In Scott and Lambek ("Introduction to Higher Order Categorical Logic",
Cambridge Studies in Advanced Mathematics, 7, 1986) the comment

"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

It's the then-unsolved uncovering of this hidden structure that they
were alluding to.

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

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.

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

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
(a) a determination of when an arrow g: N -> A is differentiable
(b) the formulation for "rules of differentiation" for differentiable

The non-trivial element here is that a given arrow g: N -> A can be a
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

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,

Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.