NIST Workshop on Computational Category Theory: Day 1 and Day 2

This is the continuation of a previous post. The schedule for the workshop can be found here. In addition, the slides can be found here. This post is broken up into the repsective days of the workshop. I will give some take aways that I thought were interesting.

Day 1

Upon arriving at the NIST campus for the first time we had to first visit the visitors center to obtain passes for the workshop. There we would just stand in line and wait. There I noticed a few people hanging around and realized that they were attending the workshop. I offered them a ride from there to the main building. So we all piled in my small rental car and made our way over.

The workshop had a really good turn out. I think there were around twenty people. The group was a nice mix of both academics and people from industry. I found it very interesting to here what kind of problems the industry folks thought that category theory (CT) could help solve. An even more interesting aspect of talking with everyone was the people like me who already love CT do not need much convincing, but getting engineers and other practioners to see that CT is a worthy theory to learn for their job.

CT can be very intimidating, and there is an initial startup cost of learning it. There were a number of proposals for trying to fix this problem. For example, using different language. That is, do not call it CT, but something else, because it seems that some words are scary to people, for example, monad, pull back, functor, Kan extension, etc. I do not think this is good idea personally. A better idea, that was also mentioned at the workshop, is to get better at teaching CT, especially in the U.S. There are many universities that do not even teach it at the graduate level, but we really need it at the undergraduate level. This would be a huge gain if we could introduce people to CT earlier. Then they learn the proper way to think earlier on as opposed to having to unlearn some things. Any teaching researchers out there, you are up!

The first talk was by Spencer Breiner and it was called “Structural Mathematics for Complex Systems”. This talk was a “why are we here?” talk. It tried to explain just what Computational Category Theory (CCT) is. CCT is to be a another tool in the tool box for applied problem solving. For example, calculus came out of Newton studying the world around him, and by wanting to explain his world using the language of mathematics. The same is hoped for CCT. This new tool is to be very computational which means we want to actually implement categorical phenomenon. We would like to be able to compute with them, for example, we might want to compute a pull back as opposed to just knowing that one exists.

Some interests pointed out by Spencer that CCT could potentially contribute to are Software Security and Specification, Cyberphysical systems, Data Integration, and interfacing several databases — think

He went on to really do a good job outlining why CT, and even why not CT, but I will not be able to do his talk justice here. David Spivak did recommend that he record the talk and put it on YouTube, and so if he does I will add a link here.

David Spivak gave the second talk of the day filling in for Jacques Carette who could not make the workshop. David talked about his work using operads to model modular thinking. The idea is that a concept is an operad, and more advanced concepts can be constructed using various operators on operads. Check out his proposal for more information.

The forth talk of the day is another I liked a lot. It was on the “Functorial Query Language (FQL)” which is a new database description and query language. The presenter was Ryan Wisnesky a colleague of David Spivak’s. FQL is an implementation of the notion that any database can be given a semantics in CT.

A database scheme is a category where the objects are tables and the morphisms are columns. Suppose \(T\) is an object, then the morphism \(c : T \to T’\) is a column of \(T\) valued in \(T’\). Now an instance of a database schema (category) is a set-valued functor \(F : D \to \mathsf{Set}\) where \(D\) is the schema. An interesting point about this semantics is that data migration from one DB, \(D\), to another, \(D’\), is simply a functor \(M : D \to D’\). This idea goes back to Bob Rosebrugh and Michael Johnson’s work in 1996, but was expanded on by David Spivak. See the paper Functorial Data Migration by David Spivak for more on how DB’s can be designed using categories.

Ryan presented his work on implementing FQL, and hence, implementing categories and operations on categories such as pull backs. He ran into some issues, because he wants to be able to implement categories and then fully automatically prove properties about these categories. For example, any constraints that must be satisifed to get the pull back needs to be automatically discharged. A more simple issue is, any particluar category might have a morphism \(m : A \to A\) which provides a means to create an infinite number of morphisms, \(m\), \(m;m\), \(m;m\), \(\ldots\), through composition. So how do we concreately implement this? He is using Java, which I think is a bad idea, because just as he notes he runs into problems implementing these. I however would have used a lazy language with corecursion to implement the infinte stream of compositions. Then we only compute what we need when we need it.

Someone posed the question of why they did not use a functional programming lanugage like Haskell for implementing FQL. Ryan’s response was that Haskell corresponds to the Hask category, and hence, is only usebable for working within one category and not suitable for implementing general categories. I think this is a narrow view. First, this is only one view of the semantics of a functional language, but it happens to be very useful one. I could could argue that Java has a semantics in coalgebras using the work of Bart Jacobs, and hence, by Ryan’s argument Java is only good for working in a coalgebra.

Check out more about FQL here.

Day 2

The second day was much shorter due to it being the last day. Bob Rosebrugh gave the opening talk on his and Mike Johnson’s work on a functorial semantics of DBs. He also demoed a tool his students and he implemented to construct databases in a categorial way called Entity Attribute Sketch (EAS). He also has a few other categorical goodies such as a graphical database for category theory GDCT which has a number of things one could use to study category theory. Lastly, he also started a project to implement a database of categories DBC. It was really cool to meet him and Mike they are both really nice people.

There were a few other talks as well, but this post is getting long enough.

The day ended with a discussion session led by David Spivak on where the project should go next. One of the milestones decided on was the creation of a new website for collecting information on the project. Go and check it out!

I found the workshop to be a lot of fun, and I am glad I went. I got a number of useful research ideas from it.

Posted in category theory, computer science, Conferences/Workshops, Haskell, Semantics | Tagged , , , , , , | Leave a comment

NIST Workshop on Computational Category Theory: Day 0

Yesterday, I departed from Augusta, GA to attend a two day workshop at the National Institute of Standards and Technology (NIST). The workshop is called “Computational Category Theory” and is somewhat of a kickoff on the discussion of how category theory can be used in the more practical aspects of computer science. I caught wind of the project through Dusko Pavlovic when I visited him this past summer. He asked that I be added to the NIST mailing list for the project and through the mailing list I was invited to the workshop; everyone on the list was invited.

I am particularly excited to be attending this workshop, because, as my readers know, I think category theory (CT) has a lot more to offer computer science than it has already. This attendees of this workshop know, by the fact that some of them are from the industry, that the power CT is spreading. Throughout the next three days I will be blogging — and tweeting (@heades) — about the workshop. I am hopping to have some pictures as well.

The workshop is being held on the NIST campus in Gaithersburg, Maryland. I flew from Augusta to Atlanta, and then to Washington, DC. My flights were through Delta, and I am actually quite surprised that my flights were very comfortable and timely. After I arrived in DC I decided to rent a car, because there was just to much public transportation I would have had to navigate everyday. No problems with the car rental either, in fact, Enterprise was quite quick and inexpensive.

The only problem I ran into was driving the interstate from Washington to Gaithersburg. I was heading down the interstate at around sixty-five miles per hour when the eight cars in front of me had to slam on their breaks. At that moment I was looking at the family van directly in front of me, filled to capacity, apply their breaks, and I literally saw people in the back of the van fly forward into the front. At that point I followed suit and applied my breaks, but I began to slide forward at an alarming rate, in fact, if some evasive maneuver was not used I was going to hit the van, and hit it hard, and so I looked left, and saw that there was room, and forced the car to slide into the adjacent lane. I was okay, and the van full of children were okay as well. I would have rather crashed somewhere other than that van. I think I was shaking the rest of the afternoon.

The workshop is scheduled to consist of both talks and discussion sessions. The following are the list of talks and abstractions:

Horn Clause logic of subatomics by Radhakrishnan Balu

Turing-computable Horn clause based logical programming is a very successful technique in expressing classical algorithms. Here, we extend this formalism to the quantum context and discuss algorithms and communication protocols that are commonly found in the literature. The rigorous framework of quantized Horn clauses is established using the machinery of quantum probability. The lattices underlying the quantum logic of Horn clauses characterized and several examples discussed in the proposed language. Finally, open issues in the design of a possible theorem prover to interpret the quantized Horn clauses are discussed.

Structural Mathematics for Complex Systems by Spencer Breiner

Part of NIST’s mission is to promote industrial innovation. Looking forward, tomorrow’s industry requires a more sophisticated set of tools to address the complexity and dynamism of new mechanisms such as cybe-physical systems and the Internet of Things. Category theory, which has demonstrated its ability to simplify and organize complex problems in mathematics and the sciences, may offer just such a toolbox. A new generation of accessible textbooks makes industrial application of these techniques more realistic, but we still lack the coherent collection of software tools necessary to realize this promise. The development of this software will benefit not only modern industry, but also category theory itself.

(Module signature/type class/trait/theory presentation) combinatorsData Landscaping to Support Coordination at Scale by Peter Gates

Pharmaceutical research and development is an endeavor requiring coordination at scale. The high risk together with the inherent scope of product research and development requires that many bets be made and managed across a complex data landscape. The reality of the present day data landscape is more akin to a wild and untamed frontier than to a well-tended garden where information is systematically created, stability and adaptability are in harmony and risks are understood and managed. With this metaphor in mind we will consider what a data landscape is and how we can go about surveying, standardizing, integrating and evolving that landscape. We coin the phrase data landscaping as a concept that takes an integrated global view of all of the various activities required to provide support for coordination at scale.

Axiomatic Category Theory For Knowledge Representation by Henson Graves

Axiomatic category theory provides a computationally friendly replacement for set theory as a foundation for engineering and science. This claim is based on the use of category theory axiom sets as descriptive models in science and engineering. The language primitives of an engineering modelling language such as SysML can be identified with maps and types (objects). Conversely, the modelling languages can be used to provide a graphical syntax for the topos based languages. Models in these languages can be embedded as axiom sets within constructive topos theory. Constructive axioms can be given that generate a topos with canonical subobjects. The axioms are expressed in a computational logic which is suitable for automated reasoning. This work extends the work of Joachim Lambek on axiomatics for Cartesian closed categories and dogmas. The constructive topos formalism can be used to integrate reasoning with product development in the context of engineering modelling. Automated reasoning from these axiom sets has the potential to solve practical problems. Many problems reduce to whether the theory of the axioms is consistent. Computational toposes can be represented as sections of a sheaf constructed from the Heyting object. The sheaf representation provides a semantics which can be used for simulations of the descriptive models. Meta level characterizations of axiom sets for which all of the valid interpretations are isomorphic are given. These results enable model analysis to be reduced to syntactic properties of axiom sets.

Set-valued functors preserving structure: Presentations, Computations and Implications. by Michael Johnson

Cateno: an approach to computational category theory by Jason Morton

I will discuss the design of an interactive computer algebra system, Cateno, for computational category theory. The emphasis in Cateno is on modeling; it is intended as a ”Matlab of category theory” and is targeted at people doing applied work rather than as a proof assistant for category theorists. There is a corresponding design emphasis on performance, accessibility, and working with data. The first models amenable to representation in Cateno are uncertainty models which admit descriptions as monoidal categories. Cateno is implemented in Julia.

Implementing database design categorically by Bob Rosebrugh

Designing models for the syntactic structure of databases is best done using categories. In particular, finite-limit, finite-sum (EA) ”sketches” are just right for expressing the both the types and constraints of a database model, especially for the relational paradigm.
The EASIK Java application provides a user-friendly graphical design environment for EA sketches which means that it provides a visualization for such categories. The sketch specifications are XML documents and this is probably EASIK’s main interest for Computational CT. The main function of EASIK is exporting a design to a database schema in SQL (the standard relational database language). The application also supports data entry and manipulation. Its most recent version also facilitates definition and export of database views.

FQL: A Functorial Query Language by Ryan Wisnesky

We study the data transformation capabilities associated with schemas that are presented by directed multi-graphs and path equations. Unlike most approaches which treat graph-based schemas as abbreviations for relational schemas, we treat graph-based schemas as categories. A schema S is a finitely-presented category, and the collection of all S-instances forms a category, S-Inst. A functor F between schemas S and T, which can be generated from a visual mapping between graphs, induces three adjoint data migration functors,
ΣF :S-Inst→T-Inst, ΠF :S-Inst→T-Inst, ∆F :T-Inst→S-Inst.

We present an algebraic query language FQL based on these functors, prove that FQL is closed under composition, prove that FQL can be implemented with the select-project-product-union relational algebra (SPCU) extended with a key-generation operation, and prove that SPCU can be implemented with FQL.

A Categorial Approach to Knowledge Management by Ralph Wojtowicz

Categorical logic provides a promising framework for developing knowledge management technologies that complement relational databases. semantic web and logic-based infrastructure. I will discuss joint work with S. Bringsjord and J. Hummel in which we explored applications of sketch theory to knowledge management including representation of context, analogy, inference (via Q-trees of Freyd and Scedrov), and alignment (via the theory of a sketch and Morita equivalence). I will discuss joint work with N. Yanofsky in which we researched quantum algorithms for computing Kan extensions. We found that, quantum computers will not provide a speedup for exact calculation of right Kan extensions in general or for coproducts. The left Kan extension case depends on whether or not a superior quantum algorithm for computing coequalizers can be found. Finally, I will discuss a project aimed at using category theory to explore transformations between uncertainty models (such as probability and Dempster-Shafer belief states).

Posted in category theory, Conferences/Workshops | 1 Comment

TTT: Exercise 1.1.\(\text{IIT}^\diamond\)


Describe the isomorphisms, initial objects, and terminal objects (if they exist) in each of the categories in exercise \(1.1.\text{CCON}^\diamond\). I think this exercise should have come before the exercise \(1.1.\text{ISO}^\diamond\) in the book, because it requires the definition of isomorphism for slice categories.

  • Arrow Category.
    • Isomorphisms. An isomorphism in the category \(Ar(\cat{C})\) is a pair of morphisms (described by the following diagrams):

      These two morphisms must satisfy the following equations:

      Thus, an isomorphism in \(Ar(\cat{C})\) corresponds to a pair of ismorphisms in \(\cat{C}\).
    • Initial Objects. Recall that an initial object in a category is an object such that there exists an unique arrow from the initial object to any other object. Thus, for every object, an arrow of \(\cat{C}\), we must be able to construct an unique arrow from the initial object to any other object (arrow of \(\cat{C}\)). Suppose \(g : C \to D\) is an arrow of \(\cat{C}\). The following diagram defines a unique arrow to \(g\):

    • Terminal Objects. Terminal objects are similar to the construction given for initial objects. The unique diagram is as follows:

  • Twisted Arrow Category.
    • Isomorphisms. An isomorphism in the category \(Ar(\cat{C})\) is a pair of morphisms (described by the following diagrams):

      These two morphisms must satisfy the following equations:

      Thus, an isomorphism in \(Tar(\cat{C})\) corresponds to a pair of ismorphisms in \(\cat{C}\) and \(\cat{C}^{\mathsf{op}}\)
    • Initial Objects. We cannot use the trick with identities to get an initial object in the twisted arrow category, but if \(\cat{C}\) has an intital object, then \(Tar(\cat{C})\) has one. The morphisms of \(Tar(\cat{C})\) are pairs of morphisms from \(\cat{C}\) and \(\cat{C}^{\mathsf{op}}\) respectively. Thus, if \(\cat{C}\) has an initial object, then \(\cat{C}^{\mathsf{op}}\) has a terminal object. This implies that we can define the initial object of \(Tar(\cat{C})\) as the identity out of the initial object of \(\cat{C}\). The following diagram defines the unique arrow out of the initial object:

    • Terminal Objects. We can use our identity trick to get terminal objects in any twisted category. The following defines the terminal arrow:

  • Slice Category.
    • Isomorphisms. Isomorphisms in slice categories were defined in the post \(1.1.\text{ISO}^\diamond\).
    • Initial Objects. Simiarly to the twisted category intitial objects do not exist in any aribtrary slice category, but if \(\cat{C}\) has an initial object, then \(\cat{C}/A\) does as well. The unique arrow is defined as follows:

      This diagram commutes, because of the uniqueness of \(\diamond_A\).
    • Terminal Objects. Terminal objects do exist, and correspond to the identity arrow. The unique arrow is defined as follows:

Posted in category theory | Tagged , | Leave a comment

TTT: Exercise 1.1.\(\text{ISO}^\diamond\)


The category of objects of \(\cat{C}\) over \(A\) (slice category \(C/A\)) has as objects the arrows of \(\cat{C}\), and an arrow from \(f : B \to A\) to \(g : C \to A\) is an arrow \(h : B \to C\) making the following diagram commute:

  • a. Show that if \(h : f \to g\) over A of \(\cat{C}/A\) is an isomorphism then \(h\) is an isomorphism in \(\cat{C}\). Note that this question is an iff in the book, but in the light of part b I changed it to an only an if, because the only-if direction would mean that any time we have an isomorphism in \(\cat{C}\), then all morphisms forming a slice would be isomorphic, but this is not the case.

    Suppose \(h : f \to g\) is an isomorphism. Then there exists another morphism \(h^{-1} : g \to f\) such that all of the following are true:

    Both of the previous diagrams imply that \(h\) and \(h^{-1}\) are mutual inverses in \(\cat{C}\), and hence, define an isomorphism.
  • b. Give an example of objects \(A\), \(B\), and \(C\) of some category \(\cat{C}\) and arrows \(f : B \to A\) and \(g : C \to A\)such that \(B \cong C\) in \(\cat{C}\), but \(f\) and \(g\) are not isomorphic in \(\cat{C}/A\).

    Set \(A = \mathbb{N}\), \(B = \mathbb{N} \times \top\), and \(C = \mathbb{N}\), then \(f = \pi_1 : A \times \perp \to A\) and \(g(x) = x*2 : A \to A\). In this case \(B \cong C\), but \(f\) and \(g\) are not isomorphic, because it is not possible to form a morphism \(h : f \to g\) or \(h’ : g \to f\).

Posted in category theory | Tagged | Leave a comment

TTT: Exercise 1.1.\(\text{CCON}^\diamond\)

Starting now I am going to be doing nearly every exercise in Barr and Wells’ book “Toposes, Triples, and Theories.” I might skip some here and there. I am doing this to start closing the gaps in my category theory knowledge. It should be fun. Future posts will not have much commentary, but will state the problem and my solution. Perhaps I will use these again in the future, or someone out there in the cloud might find them helpful. It gives me an excuse to do them, and write them up completely.

Verify the following constructions are categories.

  • a. For any category, \(\cat{C}\), the arrow category denoted, \(Ar(\cat{C})\), has as objects the arrows of \(\cat{C}\) and an arrow from \(f : A \to C\) to \(g : B \to D\) is a pair of arrows \(h : A \to B\) and \(k : C \to D\) making the following diagram commute:

    Identities. Suppose \(f : A \to A\) is an arrow of \(\cat{C}\). We must define two arrows \(h : A \to A\) and \(k : A \to A\) making the following diagram commute:

    Choose \(h = k = \id_A\). Clearly, the previous diagram commutes.

    Composition. Suppose we have the diagrams:

    It is easy to show that the previous two diagrams imply that the following diagram will commute:

    We prove this diagram commutes by the following equational reasoning:

    The previous diagram corresponds to the composition of the two arrows \((h_1,k_1) : f \to g\) and \((h_2,k_2) : g \to h\). We can see that this turns out to be \((h_1;h_2,k_1;k_2)\). Thus composition of \(Ar(\cat{C})\) is inherited from composition in \(\cat{C}\). This then implies that composition in \(Ar(\cat{C})\) will respect identities as well as associativity.
  • b. For any category, \(\cat{C}\), the twisted arrow category denoted, \(Tar(\cat{C})\), has as objects the arrows of \(\cat{C}\) and an arrow from \(f : A \to C\) to \(g : B \to D\) is a pair of arrows \(h : A \to B\) and \(k : D \to C\) making the following diagram commute:

    Identities. Defined as they were for \(Ar(\cat{C})\).

    Composition. Suppose we have the diagrams:

    We must show that the previous diagrams imply the following diagram commutes:

    We prove this diagram commutes by the following equational reasoning:

    Again, associativity of arrows will come from associativity from \(\cat{C}\) and composition will respect identities because \(\cat{C}\) respects identities.
Posted in category theory | Tagged | Leave a comment

The Collapse: When Matter Meets Antimatter

One characteristic which sets category theory apart from other theories is that for any concept there exists a dual. This makes category theory an obvious choice when setting out on an investigation of a dual concept. In this post we take a look at the less well-known dual of implication which we call coimplication, but is also known as subtraction or exclusion.

Implication corresponds to the right adjoint of the cartesian product. That is, a cartesian category \(\cat{C}\) models implication if the functor \(A \times (-) : \cat{C} \to \cat{C}\) has a right adjoint, which we denote \(A \Rightarrow B\) for objects \(A\) and \(B\). By the functor \(A \times (-) : \cat{C} \to \cat{C}\) having a right adjoint we mean that there is a natural bijection \(\mathsf{cur} : \homs{A \times B}{C} \cong \homs{A}{B \Rightarrow C}\). This gives rise to the necessary tools for working with implication like currying, which is given by the bijection itself, and evalution \(\mathsf{eval} : (A \Rightarrow B) \times A \to B\). As an example using these morphisms along with the associator, \(\alpha : (A \times B) \times C \to A \times (B \times C)\), and the symmetry, \(\beta : A \times B \to B \times A\), of the cartesian product we can prove \(\mathsf{cur}(\alpha;(\mathsf{id} \times \beta);\alpha^{-1};(\mathsf{eval} \times \mathsf{id});\beta;\mathsf{eval}) : (A \Rightarrow B) \times (B \Rightarrow C) \to (A \Rightarrow C)\). A category with products, a terminal object, and the right adjoint to the product functor is called a cartesian closed category (CCC), and the right adjoint to the product is often called the interal hom, because it can be seen as a bifunctor: \((-) \Rightarrow (-) : \cat{C}^{\mathsf{op}} \times \cat{C} \to \cat{C}\) which is an internalization of the homspace functor.

Now coimplication corresponds to the left adjoint of the coproduct functor. This is dual to that of implication. Thus, we have a bijection \(\mathsf{cocur} : \homs{B}{C + A} \cong \homs{A – B}{C}\). We also have the coevaluator \(\mathsf{coeval} : B \to (A – B) + A\). The left adjoint to the coproduct functor is called the co-internal hom, and a category with coproducts, an initial object, and a co-internal hom is called a cocartesian coclosed category (coCCC).

The question this post gives an answer to is “does it make sense to have a category that is both cartesian closed and cocartesian co-closed?” The answer happens to be negative and is due to Tristan Crolard. The main result that we will need is due to André Joyal. We will show that any category which is both cartesian closed and cocartesian coclosed is degenerative in the sense that it is a preorder, that is, for any two objects \(A\) and \(B\) the homspace \(\homs{A}{B}\) has at most one element. We call a category that is both a CCC and a coCCC a bi-cartesian closed categories (biCCC).

First, we need some basic results.

In any CCC \(\cat{C}\), if \(\perp\) is an initial object in \(\cat{C}\) and \(\homs{A}{\perp}\) is non-empty, then \(A \cong A \times \perp\).
This follows easily from the universial mapping property for products. ▌
In any CCC \(\cat{C}\), if \(\perp\) is an initial object in \(\cat{C}\), then so is \(\perp \times A\) for any object \(A\) of \(\cat{C}\).
We know that the universal morphism for the initial object is unique, and hence, the homspace \(\homs{\perp}{A \Rightarrow B}\) for any object \(B\) of \(\cat{C}\). Then using the right adjoint to the product functor we know that \(\homs{\perp}{A \Rightarrow B} \cong \homs{\perp \times A}{B}\), and hence, there is only one arrow between \(\perp \times A\) and \(B\). ▌
In any CCC \(\cat{C}\), if \(\top\) is a terminal object in \(\cat{C}\), then for any object \(A\), \(\top \times A \cong A \cong A \times \top\).
This follows easily from the universial mapping property for products. ▌

Observe the following.

A biCCC is a CCC whose dual is also a CCC.
Follows from a straightforward use of duality. ▌

Thus, the three basic results we gave apply to any biCCC.

We have now arrived at the main result by Joyal.

In any CCC \(\cat{C}\), if \(\perp\) is an initial object in \(\cat{C}\) and \(\homs{A}{\perp}\) is non-empty, then \(A\) is an initial object in \(\cat{C}\).
Suppose \(\cat{C}\) is a CCC such that \(\perp\) is an initial object in \(\cat{C}\), and \(A\) is an arbitrary object in \(\cat{C}\). Furthermore, suppose \(\homs{A}{\perp}\) is non-empty. By the first basic lemma above we know that \(A \cong A \times \perp\), and by the second \(A \times \perp\) is initial, thus \(A\) is initial. ▌

Notice that the proof of the previous lemma hinges on the fact that the universal morphism is unique. If we took the initial object to be weak instead, then the previous result would not hold.

Finally, we have the main result of this post due to Crolard.

If \(\cat{C}\) is a biCCC, then for any two object \(A\) and \(B\) of \(\cat{C}\), \(\homs{A}{B}\) has at most one element.
Suppose \(\cat{C}\) is a biCCC, and \(A\) and \(B\) are objects of \(\cat{C}\). We know from above that \(B \cong \top \times B\). Thus, we know that \(\homs{B}{A} \cong \homs{\top \times B}{A}\). Using the internal hom adjunction we know the following:

\(\homs{B}{A} \cong \homs{\top \times B}{A} \cong \homs{\top}{B \Rightarrow A}\)

Taking the dual of this chain of isomorphisms yields:

\(\homs{A}{B} \cong \homs{A}{\perp + B} \cong \homs{B – A}{\perp}\)

Therefore, by Joyal’s theorem above \(\homs{A}{B}\) has at most one element. ▌

Again, the previous result hinges on Joyal’s result, but can be prevented by using weak initial objects.

So, what are the repercussions of all of this? We do not have a categorical proof theory for languages consisting of implication and coimplication. For example, the logics: subtractive logic, L, and dualized intutionistic logic. This is not desirable.

Are there anyways around this? Well, taking weak initial objects is one way. Interestingly enough, the structural rules are causing havoic here. If we take instead of cartesian closed categories and cocartesian coclosed categories we use monoidal closed and monoidal coclosed categories we do not have any issues. The internal hom then would be a right adjoint to the tensor product, and the cointernal hom would be the left adjoint of par. So an option is to work with linear logic instead. In fact, Lambek used the cointernal hom in his work on categorical grammars. Another option is to split the atom and keep the cartesian closed part separate from the co-cartesian closed part. This is the direction I am working on right now. I plan to talk more about this in a future post.

Posted in category theory, computer science, Logic, metatheory, Semantics | Tagged , , , , , , , | Leave a comment

Categorical Note: Natural Numbers as a Coequalizer

There is a nice definition of the natural numbers monoid as a coequalizer. Most people know that we can show that the natural numbers defines a monoid \((\mathbf{N},0,+)\) where \(0\) is the identity element, and \(+ : \mathbf{N} \times \mathbf{N} \to \mathbf{N}\) is the binary operation. We will show that this monoid can be seen as the coequalizer in the category \(\mathsf{Cat}\) of categories and functors.

First, define the discrete category, \(\mathbf{1}\), of one object we call \(0\), and the category \(\mathbf{2}\) of two objects we call \(0\) and \(1\), and one non-identity-morphism we call \(g : 0 \to 1\). There are exactly two parallel functors in \(0,1 \in \mathsf{Hom}(\mathsf{1},\mathsf{2})\). We have given these two morphisms the same names as the objects of \(\mathsf{2}\) because we can view these as generalized elements, and they are isomorphic to the objects.

Now we must find the coequalizer, \(\mathsf{CoEq}(0,1)\), making the following diagram commute:

The previous diagram defining a coequalizer implies that \(0;h = 1;h\), and thus, \(0\) and \(1\) of \(\mathbf{2}\) are collapsed into the same object in \(\mathsf{CoEq}(0,1)\). This then implies that \(h(g) : h(0) \to h(1)\) can be composed with itself. Define \(\mathsf{CoEq}(0,1)\) to be the category with one object, and one non-identity-morphism, such that, \(h(0) = h(1)\) and \(h(g)\) is the non-identity-morphism. The non-identity morphism composes with itself, \(h(g),h(g);h(g),h(g);h(g);h(g),\ldots\). We do not constrain this composition in anyway, because we need each composition to be an unique natural number.

We must show that \(\mathsf{CoEq}(0,1)\) is indeed a coequalizer of \(0\) and \(1\). We already know that \(0;h = 1;h\) by definition of \(h\). Suppose \(k : \mathbf{2} \to N\) such that \(0;k = 1;k\). Then we must find a unique morphism \(l : \mathsf{CoEq}(0,1) \to N\) such that \(k = h;l\). Because we know \(0;k = 1;k\) we know that \(0\) and \(1\) are collapsed in \(N\) at some object \(x\) of \(N\). Define \(l\) to take the object of \(\mathsf{CoEq}(0,1)\) to \(x\) and to take the non-identity morphism of \(\mathsf{CoEq}(0,1)\) to \(k(g)\). At this point we can see that \(k = h;l\). As for uniqeness \(h\) is an epimorphism, and thus \(l\) is unique.

It is now easy to show that \(\mathsf{CoEq}(0,1)\) is the natural number monoid. Take the identity morphism as the natural number \(0\), the only non-identity-morphism as the natural number \(1\), and composition as addition. Clearly, the axioms of a monoid are satisfied by the fact that \(\mathsf{CoEq}(0,1)\) is a category.

I am reading the paper Computability and Complexity of Categorical Structures, and the author takes as the definition of the natural numbers the coequalizer defined above. This was the first time I had seen this, and so naturally I had to figure out the details. I got most of them, but then I also saw this email from Vaughan Pratt that filled in the gaps.

Posted in category theory, computer science, Logic, metatheory | Tagged , , | Leave a comment

Chu Spaces, Dialectica Spaces, and n-ary Relations

Dialectica spaces were first developed by Valeria de Paiva in her thesis. They happen to be a model of linear logic, in particularly they are a model of full intuitionistic linear logic. This fact came as quite a surprise to Valeria and her Ph.D. advisor Martin Hyland. The project they were working on was to give a categorical interpretation of Gödel’s dialectica interpretation. Naturally, they thought it would give rise to a cartesian closed category, but it turned out to be a model of linear logic!

There is a close cousin to dialectica spaces called Chu spaces. These spaces were developed by Michael Barr and his masters student Po-Hsiang Chu as a model of linear logic. They have also been widely studied by Vaughan Pratt and his group at Stanford. One of the most interesting computational applications of Chu spaces is in concurrency theory.

This post can be thought of as some of my notes on understanding the relationship between dialectica spaces and Chu spaces. The results in this post are mostly due to Valeria de Paiva and Vaughan Pratt; citations will be given below. The main objective of this post is to highlight the differences between the two types of spaces, and to show that Chu spaces can be embedded into dialectica spaces using Valeria’s work. Then we show that all \(n\)-ary relational structures can be embedded into dialectica spaces using Pratt’s work. Finally, we conclude with an application.

Consider the following definitions.

A dialectica space is a function \(r : A \times X \to \Sigma\) such that \(\Sigma\) is a lineale. We call \(\Sigma\) the alphabet and \(X\) the set of states of the dialectica space. Given a dialectica space we can define a new function that returns the columns of the space given a state by \(r_c = \mathsf{cur}(\beta;r) : X \to (A \to \Sigma)\) where beta is the canonical isomorphism \(\beta : X \times A \to A \times X\) and \(\mathsf{cur}\) is the canonical currying isomorphism. When \(r_c\) is injective we call \(r\) extensional.
A Chu space is a function \(r : A \times X \to \Sigma\). We call \(\Sigma\) the alphabet and \(X\) the set of states of the Chu space. Chu spaces can be extensional which is defined exactly how it is defined for dialectica spaces.

The previous definitions imply that we can think of dialectica and Chu spaces as matrices where the set of values in their cells are from \(\Sigma\). Extensional spaces are often easier to work with because the states of the space are unique.

There is only one difference between the two previous definitions, which is the requirement that \(\Sigma\) is a lineale in the definition of dialectica spaces. What is a lineale, and why do we need it? Consider the first question.

A monoidal poset is a poset \((\Sigma,\leq)\) with a given given compatible monoidal structure \((L,\circ,e)\). That is, \(L\) is a set with a reflexive, symmetric, and transitive relation \(\leq\,\subseteq L \times L\) together with a monoidal multiplication \(\circ : L \times L \to L\) and distinguished object \(e \in L\) satisfying the following:

  • Associativity: \(a \circ (b \circ c) = (a \circ b) \circ c\)
  • Symmetry: \(a \circ b = b \circ a\)
  • Identity: \(a \circ e = e \circ a = a\)
  • Compatibility: if \(a \leq b\) then \(a \circ c \leq b \circ c\), for all \(c \in L\)

A lineale is a monoidal poset \((L, \leq, \circ, e)\) such that for any \(a,b \in L\), there exists a largest \(x \in L\) where \(a \circ x \leq b\). This element is denoted by \(a \Rightarrow b\) and is called the relative pseudocomplement of \(a\) wrt \(b\). This definition implies that following hold:

  • Application: \(a \circ (a \Rightarrow b) \leq b\)
  • Currying: \(a \circ c \leq b\) iff \(c \leq a \Rightarrow b\)
  • If \(a \leq b\), then for any \(c \in L\), \(c \Rightarrow a \leq c \Rightarrow b\) and \(b \Rightarrow c \leq a \Rightarrow c\)

Thus, lineales can be seen as a trivialization of a symmetric monoidal closed category.

Lineales are needed to define transformations between dialectica spaces. We define these next along with transformations between Chu spaces. These are what really set the two types of spaces apart.

Suppose \(r : A \times X \to \Sigma\) and \(s : B \times Y \to \Sigma\) are two dialectica spaces over \(\Sigma\). Then a dialectica transformation is a pair of functions \((f,F) : r \to s\) where \(f : A \to B\), \(F : Y \to X\), and the following constraint holds:
\(\forall a \in A.\forall y \in Y.r(a,F(y)) \leq_\Sigma s(f(a),y)\).
We call the previous constraint the semi-adjointness condition, and this condition is the reason why we need the alphabet to be a lineale.
Suppose \(r : A \times X \to \Sigma\) and \(s : B \times Y \to \Sigma\) are two Chu spaces over \(\Sigma\). Then a Chu transformation is a pair of functions \((f,F) : r \to s\) where \(f : A \to B\), \(F : Y \to X\), and the following constraint holds:
\(\forall a \in A.\forall y \in Y.r(a,F(y)) = s(f(a),y)\).
We call the previous constraint the adjointness condition.

Taking dialectica spaces over \(\Sigma\) as objects and dialectica transformations as morphisms we obtain a category called \(\mathsf{Dial}(\Sigma)\), and doing the same for Chu spaces we obtain a category called \(\mathsf{Chu}(\Sigma)\). We have arrived at the following result.

Suppose \(\Sigma\) is a lineale. Then there is an embedding \(E : \mathsf{Chu}(\Sigma) \to \mathsf{Dial}(\Sigma)\).
Take \(E\) to be the identity functor. ◼

The results up to now are not new. They were first investigated by Valeria de Paiva in her TAC paper. She makes a lot more interesting connections between the two types of spaces. The interested reader should see her paper for more fun! We now use her result to show that every \(n\)-ary relation can be represented by a dialectica space.

\(n\)-ary Relations in Dialectica Spaces

Vaughan Pratt showed that any \(n\)-ary relation can be represented by a Chu space over \(\mathsf{2}^n = \{0,1\}^n\) for some \(n \in \mathbb{N}\). This results in Chu spaces being able to represent a large number mathematical structures. We would like this same result for dialectical spaces, and we can obtain it by using the embedding discussed above. However, we must show that \(\mathsf{2}^n\) is a lineale in order to obtain our result. We do this now.

First, we show that we can construct a category of lineales. We have morphisms between lineales.

Suppose \((L_1,\leq_1, \circ_1, e_1,\Rightarrow_1)\) and \((L_2,\leq_2, \circ_2, e_2,\Rightarrow_2)\) are two lineales. Then a lineale map between \(L_1\) and \(L_2\) is a function \(f : L_1 \to L_2\) satisfying the following properties:

  • If \(a \leq_1 b\), then \(f(a) \leq_2 f(b)\)
  • \(f(a \circ_1 b) = f(a) \circ_2 f(b)\)
  • \(f(e_1) = e_2\)
  • \(f(a \Rightarrow_1 b) = f(a) \Rightarrow_2 f(b)\)

It is easy to see that we can now form a category of lineales where composition and identities are set theoretic. We denote this category by \(\mathsf{Lin}\). Next we show that this category has products.

\(\mathsf{Lin}\) has all finite products.
Suppose \((L_1,\leq_1, \circ_1, e_1,\Rightarrow_1)\) and \((L_2,\leq_2, \circ_2, e_2,\Rightarrow_2)\) are two lineales. Then we can construct the monoidal poset \((L_1 \times L_2,\leq_\times, \circ_1 \times \circ_2, (e_1,e_2))\) where \(\leq_\times\) is the lexicographic combination of \(\leq_1\) and \(\leq_2\). Now we must prove that for any \((a,b),(c,d) \in L_1 \times L_2\), there exists a largest \((x_1,x_2) \in L_1 \times L_2\) where \((a,c)\,(\circ_1 \times \circ_2)\,(x_1,x_2) \leq (b,d)\). Choose \(a \Rightarrow_1 b\) for \(x_1\) and \(c \Rightarrow_2 d\) for \(x_2\). Certainly, each of these are largest within their respective set, and hence, their pairing will be largest in the cartesian product. Therefore, \((L_1 \times L_2,\leq_\times, \circ_1 \times \circ_2, (e_1,e_2),\Rightarrow_1 \times \Rightarrow_2)\) is a lineale.

Clearly, there are two lineale maps \(\pi_1 : (L_1 \times L_2,\leq_\times, \circ_1 \times \circ_2, (e_1,e_2),\Rightarrow_1 \times \Rightarrow_2) \to (L_1,\leq_1, \circ_1, e_1,\Rightarrow_1)\) and \(\pi_2 : (L_1 \times L_2,\leq_\times, \circ_1 \times \circ_2, (e_1,e_2),\Rightarrow_1 \times \Rightarrow_2) \to (L_2,\leq_2, \circ_2, e_2,\Rightarrow_2)\) defined by the set theoretic projections. Finally, we must show that the following diagram commutes:

where \((L_3,\leq_3, \circ_3, e_3,\Rightarrow_3)\) is a lineale. Suppose \(f : L_3 \to L_1\) and \(g : L_3 \to L_2\) are two lineale maps. Then choose the set theoretic function \(\langle f,g \rangle : L_3 \to L_1 \times L_2\) for \(h\). Clearly, in sets the previous diagram commutes, but we must verify that \(\langle f,g \rangle\) is a lineale map. We do this verification as follows:

  • Suppose \(a,b \in L_3\) and that \(a \leq_3 b\). Then \(\langle f,g \rangle(a) = (f(a),g(a))\) and \(\langle f,g \rangle(b) = (f(b),g(b))\). By assumption \(f\) and \(g\) are lineale maps, and thus, \(f(a) \leq_1 f(b)\) and \(g(a) \leq_2 g(b)\) which implies that \((f(a),g(a)) \leq_\times (f(b),g(b))\).
  • Suppose \(a,b \in L_3\). Then
    \langle f,g \rangle(a \circ_3 b)
    & = & (f(a \circ_3 b),g(a \circ_3 b))\\
    & = & (f(a) \circ_1 f(b),g(a) \circ_2 g(b))\\
    & = & (f(a),g(a))\,(\circ_1 \times \circ_2)\,(f(b),g(b))\\
    & = & \langle f,g \rangle(a)\,(\circ_1 \times \circ_2)\,\langle f,g \rangle(b).\\
  • First, \(\langle f,g \rangle(e_3) = (f(e_3),g(e_3))\), and because \(f\) and \(g\) are lineale maps \((f(e_3),g(e_3)) = (e_1,e_2)\).
  • Suppose \(a,b \in L_3\). Then
    \langle f,g \rangle(a \Rightarrow_3 b)
    & = & (f(a \Rightarrow_3 b),g(a \Rightarrow_3 b))\\
    & = & (f(a) \Rightarrow_1 f(b),g(a) \Rightarrow_2 g(b))\\
    & = & (f(a),g(a))\,(\Rightarrow_1 \times \Rightarrow_2)\,(f(b),g(b))\\
    & = & \langle f,g \rangle(a)\,(\Rightarrow_1 \times \Rightarrow_2)\,\langle f,g \rangle(b).\\

At this point all that is left to do is show that there is a terminal object. Let \(L_T\) be any one element set where \(\star \in L_T\) is its distinguished object. Then we can construct the lineale \((L_T, \leq_T, \circ_T, \star, \Rightarrow_T)\) as follows:

  • Set \(\leq_T = \{(\star,\star)\}\).
  • Set \(\star \circ_T \star = \star\).
  • Set \(\star \Rightarrow_T \star = \star\).

It is trivial to see that \(L_T\) is a lineale given the previous definitions. Suppose \((L, \leq, \circ, \star, \Rightarrow)\) is a lineale. Then there is a lineale map \(\diamond : L_1 \to L_T\) is simply the terminal map from sets. The verification that it is lineale is straightforward. ◼

If \(L\) is a lineale, then \(L^n = \underbrace{L \times \cdots \times L}_n\) is a lineale for any \(n \in \mathbb{N}\).

To conclude that \(\mathsf{2}^n\) is a lineale it is enough to show that \((\mathsf{2} = \{0,1\},\leq_B\,=\{(0,0),(0,1),(1,1)\},\land,1,\Longrightarrow) \), where \(\land\) and \(\Longrightarrow\) are binary conjunction and implication respectively, is a lineale. It is easy to see via truth tables that conjunction is symmetric, associative, and \(1\) is its identity. Thus, \(\mathsf{2}\) is a monoidal poset. Now consider the following truth table:

a & x & a \land x & b\\
0 & 1 & 0 & 0\\
0 & 1 & 0 & 1\\
1 & 0 & 0 & 0\\
1 & 1 & 1 & 1\\

This truth table proves that for any \(a,b \in \mathsf{2}\), there exists a greatest \(x \in \mathsf{2}\) such that \(a \land x \leq_B b\). Furthermore, notice that the columns for \(a\), \(b\), and \(x\) defines binary implication where \(x = a \Longrightarrow b\). Therefore, \((\mathsf{2},\leq_B,\land,1,\Longrightarrow) \) is a lineale. By the fact that \(\mathsf{Lin}\) is cartesian we may conclude that \(\mathsf{2}^n\) is a lineale.

At this point we simply replay Vaughan Pratt’s result. First, we define \(n\)-ary relations.

An \(n\)-ary relational structure \((X,\rho)\) consists of a set \(X\) and an \(n\)-ary relation \(\rho \subseteq X^n\) on \(X\). A homomorphism \(f : (X,\rho) \to (Y,\sigma)\) between \(n\)-ary relational structures is a function \(f : X \to Y\) such that \(f(\rho) = \{(f(a_1),\cdots,f(a_n)) \mid \overrightarrow{a_i} = (a_1,\cdots,a_n) \in \rho \} \subseteq \sigma\). Taking the relational structures as objects and their homomorphisms as morphisms defines a category called \(\mathsf{Str}_n\).

Next we define an embedding \(E’ : \mathsf{Str}_n \to \mathsf{Dial}(\mathsf{2}^n)\).

We define the object part of \(E’ : \mathsf{Str}_n \to \mathsf{Dial}(\mathsf{2}^n)\) as taking the \(n\)-ary relational structure \((A,\rho)\) to the dialectica space \(r : A \times X \to \mathsf{2}^n\) defined as follows. Take the set of states, \(X\), to be the subset of \(n\)-tuples \(r \in \mathcal{P}(A)^n\) for which \(\Pi_i r_i \subseteq \overline{\rho} = A^n – \rho\). Finally, define \(r : A \times X \to \mathsf{2}^n\) by \(v(a,x) = 1\) if \(a \in r_i\), and \(0\) otherwise.

The object part as defined above is injective.

For all \(\overrightarrow{a_i} \in A^n\), \(\overrightarrow{a_i} \in \rho\) iff for any \(r \in X\), there exists an \(i < n\), such that, \(r(a_i,x)_i = 0\).

It also turns out that \(r : A \times X \to \mathsf{2}^n\) is extensional. See lemma 12 of Pratt’s paper.

We still need to define the morphism part of \(E’\).

We define the morphism part of \(E’ : \mathsf{Str}_n \to \mathsf{Dial}(\mathsf{2}^n)\). Suppose \(f : (A, \rho) \to (B, \sigma)\) be a homomorphism between \(n\)-ary relations, where \(E'(A,\rho) = r : A \times X \to \mathsf{2}^n\) and \(E'(B,\sigma) = s : B \times Y \to \mathsf{2}^n\). Define \(f^{-1} : (\mathsf{2}^n)^B \to (\mathsf{2}^n)^A\) by \(f^{-1}(g : B \to \mathsf{2}^n) = f;g : A \to \mathsf{2}^n\). Finally, define \(E'(f) = (f,f’)\). The correctness of this definition can be found in Pratt’s paper in definition 13.

By theorem 14 of Pratt’s paper \(E’\) is concrete, full, and faithful. Thus, it is an embedding.

Application: Multisets in Dialectica Spaces

This line of inquiry of mine was started because I wanted a way to represent multisets by dialectica spaces over a finite alphabet. A multiset, \(m : A \to \mathbb{N}\), can be represent by an equivalence relation, \(\cong_m \subseteq A \times A\), such that, for any \(a \in A\), \(|[a]_{\cong_m}| = m(a)\). That is, the cardinality of the equivalence class of a particular element in the multiset is the elements multiplicity. Taking this representation of multisets and the previous result we now have a means of interpreting multisets into dialectica spaces over a finite alphabet.

Posted in category theory, Chu spaces, computer science, Concurrency, Dialectica Spaces, Logic, metatheory, Semantics | Tagged | 2 Comments

On the Categorical Model of Fragmented Y

\(\newcommand{\interp}[1]{\unicode{x27e6} #1 \unicode{x27e7}}\)
I recently published a post on the categorical model of fragmented system T. Aaron Stump — my Ph.D. advisor — asked a very good question. One property the Trellys team wants in a PL is a non-terminating fragment to conduct general purpose programming. However, as Aaron pointed out fragmented system T has a terminating programmatic fragment, but what if we make it non-terminating? He asked particularly about adding the Y combinator.
My response was that I did not know how to add just the Y combinator, but I argued that the programmatic fragment could be non-terminating by making it uni-typed.

I took his question as a challenge to figure out how to add just the Y combinator, and then obtain a categorical model. One thing had to be true of our model, it must have a cartesian closed subcategory to model the logical fragment in. Adding the Y combinator to STLC is simple enough, and since STLC is modeled by cartesian closed categories, then there should be an extension of cartesian closed categories with fixpoint operators. Keeping this idea in mind I did some thinking, and looked into the literature. It turns out that we can extend a cartesian closed category with fixpoint operators to obtain a model for the Y combinator. This post describes how this is done.

Fragmented Y

First thing is first. We need to define the functional PL we will be analyzing.

Just as we did in the previous post the programmatic fragment contains all typable terms using the rules annotated with \(\mathsf{Y}\), and the logical fragment contains all typable terms using the rules annotated with \(\mathsf{S}\). We can easily see that the programmatic fragment is non-terminating. Clearly, \(\cdot \vdash_{\mathsf{Y}} \mathsf{Y}\,(\lambda x:T.x) : T\), and

\(\mathsf{Y}\,(\lambda x:T.x) \leadsto (\lambda x:T.x)\,(\mathsf{Y}\,(\lambda x:T.x)) \leadsto \mathsf{Y}\,(\lambda x:T.x)\)

In addition, it is well known that the logical fragment is terminating. Thus, the logical fragment is the isolation of a terminating subtheory of a non-terminating theory.

Categorical Model

The idea is to argue how we can model the theory in a cartesian closed category with some additional structure. Just as we have said above the logical fragment can be modeled by a cartesian closed category. The subtheory rule \({\rm Y\_{\small sub}}\) can be modeled by functor from the model of the logical fragment to the model of the programmatic fragment. This is the same as it was for fragmented system T. In addition, it is easy to handle \(\mathsf{zero}\) and \(\mathsf{suc}\). So the most interesting question here is how do we model the programmatic fragment? The answer is well known, and can be found here — this book has a lot of great things in it, but lacks in presentation and the omission of details in some of the equational reasoning.

We model the programmatic fragment in a cartesian closed category extended with fixpoints for each object.

In any cartesian closed category we have the morphism \(\pi_2 : \Gamma \times (T \Rightarrow T) \to (T \Rightarrow T)\). Using this morphism we can define the following morphism in a cartesian closed category with fixpoint operators:

\( \mathsf{cur}(\pi_2;\mathsf{fix}_T) : \Gamma \to (T \Rightarrow T) \Rightarrow T \)

This morphism is the \(\mathsf{Y}\) combinator. That is, we can define

\( \interp{\Gamma \vdash_{\mathsf{Y}} Y : (T \to T) \to T}\,=\,\mathsf{cur}(\pi_2;\mathsf{fix}_{\interp{T}}) \)

A categorical model must have enough structure to model every typable term, but it must also model the reduction rules. That is, for any \(\Gamma \vdash_{\theta} t_1 : T\) and \(\Gamma \vdash_{\theta} t_2 : T\), if \(t_1 \leadsto t_2\), then \(\interp{\Gamma \vdash_{\theta} t_1 : T} = \interp{\Gamma \vdash_{\theta} t_2 : T}\), where \(\theta \in \{\mathsf{S},\mathsf{Y}\}\). It is well-known that if \(\theta = \mathsf{S}\), then the reduction rules of STLC can be modeled by a cartesian closed category. In fact, we have \(\beta\)-equality in the model:

(\(\beta\)-cat) \( \langle \mathsf{cur}(f),g \rangle;\mathsf{app} = \langle \mathsf{id},g \rangle;(\mathsf{cur}(f) \times id);\mathsf{app} = \langle \mathsf{id},g\rangle;f \)

Using \(\beta\)-cat we can prove the following:

We call the previous fact \(\mathsf{Y}\)-cat. Now we can show that a cartesian closed category with fixpoint operators models the reduction rule for the \(\mathsf{Y}\)-combinator:

It took me the better part of the weekend to get the equational reasoning right, so hopefully I did not make any mistakes.

The way we model the Y combinator is slightly different from the book here. There the authors use the morphism \( !_{\Gamma};\mathsf{cur}(\pi_2;\mathsf{fix}_T) : \Gamma \to (T \Rightarrow T) \Rightarrow T \), where \(!_\Gamma : \Gamma \to \top\) is the terminal morphism, but I do not see a reason to use the terminal morphism when we can just use \(\pi_2\). We obtain the same result here, but I might be missing something.

Finally, we arrive at the following main theorem:

Suppose that \(\mathcal{S}\) is cartesian closed category (a model of the logical fragment of fragmented Y), and that \(\mathcal{Y}\) is a cartesian closed category with fixpoint operators (a model of the programmatic fragment of fragmented Y). Then \( (\mathcal{S}, S, \mathcal{Y}) \) is a model of fragmented Y, where \( S : \mathcal{S} \to \mathcal{Y} \) is a full and faithful functor.

It was a lot of fun figuring this out!

Posted in category theory, metatheory, normalization, Semantics, STLC, Trellys, Type Theory | Tagged , , , , , | Leave a comment

On the Categorical Model of Fragmented System T

Recently, I have been thinking of something I wanted to try for a while, but my categorical skills were not good enough to think about it. In this short simple note I show how a fragmented type theory can be modeled using submodels and a functor between them. The theory I discuss is very basic, but contains the setup I wanted. I hope to build on this in the future.

The Trellys project originally set out in 2008 to design a dependently typed functional programming language with a fast amount of features. The most important of them being the isolation of a logical fragment from a non-terminating fragment called the programmatic fragment. The former amounts to a terminating fragment of the overall language with a new property called freedom of speech. This new property allows for the types of the logical fragment to depend on programs of the programmatic fragment. Thus, the logical fragment can be used to verify properties of the programs of the programmatic fragment. In addition, one can use the logical fragment to ones advantage. If one wishes to implement a program that must be terminating, then this can be internally verified by simply implementing it in the logical fragment, because it is simply a fragment of the set of overall programs.

This fragmentation was accomplished by annotating the sequent with either an \(\mathsf{L}\) or a \(\mathsf{P}\) called a consistency classifier. Then maintaining consistency of the logical fragment was achieved by placing value restrictions at key locations in the definition of type-checking algorithm. Then the addition of a rule similar to:

was added to the programmatic fragment. However, this formalization of the language resulted in a theory that was very difficult to study metatheoretically. New attempts are underway to try and modify the language so as to allow for a metatheoretic study. There are a number of references the interested reader can find with respect to this work. See my thesis and Chris Casinghino’s publications, Vilhelm Sjöberg’s publications, Stephanie Weirch’s publications, and Aaron Stump’s publications.

In this note we examine how one might model a fragmented language such as the Trellys language categorically. We start with a very simple language, and then show that there exists a strightforward functorial semantics.

Fragmented System T

We begin with the definition of the simply typed \(\lambda\)-calculus (STLC).

STLC will be considered our logical fragment. Its terms may be considered proofs while its types formulas. We now enrich this definition with a programmatic fragment resulting in our final system called fragmented system T.

The programmatic fragment contains all typable terms using the rules annotated with \(\mathsf{G}\). This fragment does not make for a very good logic, but is a very good statically typed pure functional programming language. In fact, the programmatic fragment is very powerful even if it seems simplistic. For example, we can type the Ackerman’s function:

\( \lambda m : \mathsf{Nat}.\lambda n : \mathsf{Nat}.((\mathsf{rec}\,m\,(\lambda y : \mathsf{Nat}.(\mathsf{suc}\,y)) \\
\,\,\,\,\,(\lambda h : \mathsf{Nat} \to \mathsf{Nat}.\lambda i : \mathsf{Nat}.\lambda y : \mathsf{Nat}.(\mathsf{rec}\,y\,(h\,(\mathsf{suc}\,0))\,(\lambda k : \mathsf{Nat}.\lambda j:\mathsf{Nat}.(h\,k)))))\,n) \)

Categorical Model

The purpose of this note is to define the categorical model of fragmented system T. The logical fragment (STLC) can easily be modeled by a cartesian closed category. See here for a detailed explanation of this. The programmatic fragment is also well known to be modeled by a cartesian closed category extended with a natural number object and the necessary morphisms to model zero and successor. See here for more information.

So the only interesting question we have is how do we model the subtheory rule:

This requires an operation on homspaces:

Clearly, this is corresponds to the morphism part of a functor from the model of the logical fragment to the programmatic fragment. It just so happens that such a functor exists.

Suppose that \(\mathcal{S}\) is the cartesian closed category modeling the logical fragment, and that \(\mathcal{G} \) is the extended cartesian closed category with the necessary structure modeling the programmatic fragment. Clearly, there exists a functor \(S : \mathcal{S} \to \mathcal{G}\). In addition, this functor is full and faithful, because \(\mathcal{S}\) is isomorphic to the cartesian closed proper subcategory of \(\mathcal{G}\). The latter insures that all of the typeable terms of the logical fragment are indeed modeled within \(\mathcal{S}\). Using this reasoning we arrive at the following result:

Suppose that \(\mathcal{S}\) is a model of the logical fragment of fragmented system T, and that \(\mathcal{G}\) is a model of the programmatic fragment. Then \( (\mathcal{S}, S, \mathcal{G}) \) is a model of fragmented system T, where \( S : \mathcal{S} \to \mathcal{G} \) is a full and faithful functor.

The point of the previous result is that if one fragments a language into parts where the constituent parts can be collapsed back down — e.g. the subtheory rule — then there is a functor between the constituent parts. More on this later.

Posted in category theory, metatheory, Semantics, STLC, Trellys, Type Theory | Tagged , , , , , | 3 Comments