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 enough to leave the low hanging(?) fruit of coproduct types. I will try to find or make a solution for this hole.

I believe that, once coproducts have been added, the resulting category will be optimal for describing all computable functions, and replace Set as the preferred category to define the semantics of computer science, in general. 

It seems we must allow lambda expressions of infinite length. I don't know how nontermination will be handled. The fixed point operator can then be defined by the infinite lambda expression f . f•f•f•… It might turn out that all arrows of Set will be preserved, due to coproducts, but I believe this new category will be small; the collection of all its objects will form a Set.

Kommentarer

Skicka en kommentar

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

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