Inlägg

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 enou
Skicka en kommentar
Läs mer

Related work

It's curious when you start to explore some mathematic field, and when you finally find the appropriate categorical terms for expressing your ideas, and try to Google those ideas, you always find a two year old free online book describing almost exactly what you have found, but in a slightly different field. I guess that's the beauty of using CT as an interlingua for mathematics. I think there are still some holes for me to fill in, but it seems I won't have to do a lot of the math. Polynomial Functors: A General Theory of Interaction by David I. Spivak and Nelson Niu I have also found an early attempt to make a more formal definition of lambda calculus in categories that allows them (Cartesian Closed Categories have all finite exponential objects). https://golem.ph.utexas.edu/category/2006/08/cartesian_closed_categories_an_1.html
Skicka en kommentar
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
Skicka en kommentar
Läs mer

Lambda polymorphism as a natural transformation

In my last post I proposed seeing lambda polymorphism as a bifunctor, but this notion seems tio weak. Lambda polymorfism really needs three inputs, but one of them doesn't seem to involve any data in the set sense, only type data, connecting the types. I've tried making this into a category that defined every possible input as an arrow to the right output, but it didn't turn out nicely.  Instead I'm thinking of turning lambda polymorphism into a natural transformation. This seems promising, because as we all know, a parametrically polymorphic function is always a natural transformation. I will only scetch an example. The Church numeral 4 is applied to the Church numeral 3. Without polymorphism, this would not be possible, because 4 expects a signature * -> * in its first argument, but 3 has signature (* -> *) -> * -> *. We solve this by going by a * -> * functor before we apply the 3.  The * -> * functor is super simple. It takes every signature S to a
Skicka en kommentar
Läs mer

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 categor
Skicka en kommentar
Läs mer