Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Ordering on logics of the lambda cube

nrs (Sep 08 2024 at 10:26):

Can the logic corresponding to the calculi on the lambda cube be given any interesting ordering? Maybe in terms of expressive power? Does categorical semantics have anything to say about this?

nrs (Sep 08 2024 at 10:37):

Or, in a related sense, can categorical semantics provide an ordering on logics wrt to some kind of notion of expressive power?

John Baez (Sep 09 2024 at 12:56):

What's the lambda cube?

Jean-Baptiste Vienney (Sep 09 2024 at 13:30):

All I know is that it is a cube with a different kind of $\lambda$-calculus on each vertex.

This is on Wikipedia. The page seems to give an ordering along each dimension of the cube.

Jean-Baptiste Vienney (Sep 09 2024 at 13:34):

Honestly, I don’t know much about the other vertices than the $(0,0,0)$ which is the simply typed $\lambda$-calculus. I just know that the vertex $(1,1,1)$ which is the calculus of constructions is the theoretical framework on which the proof assistant Coq is based.

John Baez (Sep 09 2024 at 13:44):

Thanks, @Jean-Baptiste Vienney. Now I can answer one of nrs' questions: the logics in a lambda cube have a [[partial ordering]] in terms of expressive power. Moving $\uparrow$, $\rightarrow$ or $\nearrow$ in the cube increases expressive power.

Damiano Mazza (Sep 09 2024 at 14:06):

The answers to this TCS Stack Exchange question give some information about the expressive power of the calculi of the lambda cube. In the context of that question, expressiveness is measured by how many problems (i.e., subsets of the set $\{0,1\}^\ast$ of binary strings) may be decided by terms of type $\mathsf{Str}\to\mathsf{Bool}$, where $\mathsf{Str}$ and $\mathsf{Bool}$ are suitable types of binary strings and Booleans, respectively (there are subtleties in exactly how these types are defined, hinted at in the answers).

Damiano Mazza (Sep 09 2024 at 18:49):

nrs said:

Or, in a related sense, can categorical semantics provide an ordering on logics wrt to some kind of notion of expressive power?

Sorry, I come back to this because I had missed this question. I think it's interesting because I'm not sure that all corners of the cube actually have a well-established categorical semantics:

• the bottom-left corner is the simply-typed $\lambda$-calculus ($\lambda\!\!\to$ on Wikipedia) and corresponds to cartesian closed categories;
• going in the direction $\rightarrow$ means moving to locally cartesian closed categories;
• but what do the directions $\uparrow$ and $\nearrow$ correspond to?

I guess that going simultaneously in both the $\uparrow$ and $\nearrow$ directions corresponds to adding power objects, so that the top-right corner of the cube (the calculus of constructions, $\lambda C$ on Wikipedia) corresponds to something like an elementary topos that fails to have equalizers. But I realize that I don't know, for example, what categorical structure corresponds to system F ($\lambda 2$ on Wikipedia). Does anyone know?

(For the sake of the question, this would distinguish the corners by assigning to each of them a categorical structure such that, whenever one moves up, right or diagonally, one finds a strictly stronger structure. "Strictly stronger" in the sense that that there are categories of the weaker kind which are not of the stronger kind, but not vice versa).

Kevin Carlson (Sep 09 2024 at 19:07):

The nLab says the semantics of system F should be in a fiberwise cc hyperdoctrine, ie a fibration of ccc's over a cartesian category, plus an object of the base that represents the functor of objects in the fibers and a Beck-Chevalley condition.

Kevin Carlson (Sep 09 2024 at 19:08):

So there's something about closedness of the category of kinds at the heart of the difference between the right-hand and the left-hand sides, maybe

dusko (Sep 10 2024 at 20:12):

nrs said:

Can the logic corresponding to the calculi on the lambda cube be given any interesting ordering? Maybe in terms of expressive power? Does categorical semantics have anything to say about this?

i was in henk barendregt's class here the lambda cube got defined, and categorical logic was, in a sense, the source of it, though henk presented it as a syntactic taxonomy.

the three dimensions of the lambda cube are: dependency, impredicativity, and comprehension. in lawvere's doctrinal diagram, dependent sums and products are the top side, impredicative sums and product (aka the quantifiers) are the bottom side adjunction, and comprehension is the adjunctions on the sides.

the lambda cube came about when it was realized that the Martin-Loef type theory vs Girard's system(s) F are the top and the bottom adjunctions, which meant that Girard's system F-omega was Girard+Martin-Loef. but Gerard Huet wanted to embed one in the other, and Thierry Coquand spelled that out in his thesis. when we realized (as reported in my thesis) that applying the type constructors after that embedding was the comprehension, henk said that the doctrinal diagram should be presented as a cube.

dusko (Sep 10 2024 at 21:09):

PS funny enough, i just mentioned the doctrinal diagram the other day in the tread On Categorical Logic. i hope i am not getting doctrinal myself. i think someone said that dependent types seemed like the most natural language for toposes and i said that lawvere definitely included them in his diagram which displayed the language of hyperdoctrines (meant to be topos++) as the adjunction between slices.

now we could maybe even say that lambda cube could be used as a "logical frame or reference" for toposes :upside_down:

nrs (Sep 10 2024 at 23:40):

Thank you very much to everyone for your answers! Lots of material to mull over and topics to investigate