The Lambda Polymorphism (bi?) functor

So, I’m trying to think about how to define a category for lambda calculus. I’m thinking of a category that has as objects all the lambda function signatures and as arrows “the set of all lambda functions” somehow related by the domain and codomain signature. I am not sure exactly how to define the arrows, but currently it is much like Set, so all objects (except * and possibly some initial and terminal objects) are exponential objects. To create the exponentials, products are needed, but they are merely cartesian products, and exponentials are defined using the curry-uncurry isomorphism, as in Set.

Let S be a non product signature with n inputs of signatures 

s1, s2, … , sn, 

so that 

S = s1 -> s2 -> … - > sn -> *. 

and T another non-product signature. Then the homset Hom(T, S) is the set of all lambda functions of signature T -> s1 -> s2 -> … - > sn -> *. If S is a product UxV, the arrows are pairs of arrows  from Hom(T, U) and Hom(T, V), defining a categorical product with the obvious homset isomorphisms. If T is a product UxV, Hom(UxV, S) is the set of all lambda functions of signature U -> V -> s1 -> s2 -> … - > sn -> *.

While it might be possible to implement the same lambda function in many ways, I believe there is a way to define the set of all “(fairly) unique” lambda functions of a certain signature as the set of strings that can be produced by some context free grammar related to the signature. I will get back to that.

Lambda functions do not have to be applied to the exact signatures of their input parameters. They can also be applied to lambda functions defined by signatures where every * is replaced with some fixed other signature and returns a function of that signature. As an example a Church numeral has the signature (* -> *) -> * -> *. If every * is replaced with * -> *, the signature becomes ((* -> *) -> (* -> *)) -> (* -> *) -> (* -> *). Since the -> bifunctor is right associative, it can also be written ((* -> *) -> * -> *) -> (* -> *) -> * -> *. A Church numeral can behave as both those signatures, but they will, in a sense, do the same thing but to different things. 

In this case, we replaced * with * -> *, but we could just as well have replaced it with any other signature. This can be nicely translated into category theory by associating every object O with an endofunctor going to the signature where every * is replaced with the signature of the endofunctor, and just lifting arrows to “the same” lambda function. This association can, in turn, be defined using a functor 

P : Lam -> (Lam ^ Lam), 

That is a functor from the category to the category of endofunctors of the category. Or is it just a bifunctor? I can’t wait to see what I’ll find next!


Kommentarer

Skicka en kommentar

Populära inlägg i den här bloggen

The category of lambda calculus with products and coproducts

Normal Forms and Cut-Free Proofs as Natural Transformations by Girard, Scedrov and Scott seems to have what I have been looking for. My interpretation: (simply typed) Lambda calculus with products can be expressed as natural deductions (with parcels and products) via the Curry-Howard isomorphism. Natural deductions can in turn be expressed by left sequent logic (with products). Sequent logic can always be rewritten in a way that is cut free. The main result of the paper is that all rules in left sequent logic (with products), except the cut rule, can be interpreted in any Cartesian closed category. Further, these interpretations can be inductively proven to be dinatural.  I think cut free left sequent logic corresponds to simply typed lambda calculus in normal form where all free variables in all subexpressions have been bound and uncurried, so the passive context of the sequent represents a tuple with the needed unbound variables in the subexpression. Notably, they have been kind ...
Läs mer

The universal arrow of the exponential object for combining function and input

I have no idea how this should be done, but I am pretty certain (right now) that it is the way forward. As described in my first post, (almost) all objects in the lambda category are exponential objects of each other. The (possibly Cartesian product) contravariant part denotes the input, and the covariant part denotes the (probably curried) output. In Set, the universal arrow of the exponential object denotes how a pair of function and input is related to the output. The trick is to do the same thing in the lambda category. Next we have to consider that the function object is lifted by a (possibly identity) natural transformation before it is applied to the input, as described in the previous post. I don't know how yet. It will probably make sense to define a category were objects are exponentials, points of the objects denote the current function of the application chain and arrows are a pairs of a natural transformation and an input object of the right signature fed to the evalua...
Läs mer