Categorical Semantics

Stream: CSLib

[Sehun Kim]

I am very happy to hear that my suggestion was helpful.

I am coincidentally interested in similar topics: in the short term, turning STLC into a category, and in the long term, extending properties such as strong normalization to other systems.

If you plan to push your work on the strong normalization property, it would be very helpful for my work.

[Chris Henson]

Do you mean the categorical semantics for STLC? I've worked on this a lot myself, but there are some technical issues that I think make formalization difficult. I'd be interested to see your approach.

[Chris Henson]

(Maybe I will move this to a new thread if we'd like to discuss this more, just to keep the conversation organized)

[Sehun Kim]

Unfortunately, I do not have much to show right now because I am starting from scratch. However, I hope to be able to contribute to CSlib in the near future.

[Notification Bot]

4 messages were moved here from #CSLib > Strong norm for Stlc by Chris Henson.

[Chris Henson]

I went ahead and moved these messages. Can I ask which references you're looking at? Even for STLC there are a couple of approaches that look a bit different formally. I think it'd be good to discuss a bit beforehand so we don't duplicate each other's work, but it's great to hear others are interested in this.

[Sehun Kim]

Since I am looking for STLC as a part of the other project, It was appeared as a lemma, but if you want specify for STLC,
https://www.paultaylor.eu/stable/prot.pdf
would be my main source.
For showing strictly normalizing of other systems, I am following the source
https://www.irit.fr/~Ralph.Matthes/dissertation/matthesdiss.pdf
The reason why I am interested in this topic is because I am interested in CHAD(Combinatory Homomorphic Automatic Differentiation), So one day I hope to formalize this article.
https://arxiv.org/abs/2007.05283

[Sehun Kim]

But they are now just in consideration.

[Chris Henson]

When I talk about there being different approaches to categorical semantics of STLC, I mean that one could be referring to:

• The most familiar thing people mean: STLC extended with unit and product types, where both contexts and types are mapped to categorical products, see these notes which summarize Crole's book
• STLC without these extensions, which requires an approach like fibered category theory, see the first chapters of Categorical Logic and Type Theory
• Any of the above, but instead using multicategories which are in some sense more natural
• Categorical semantics of normalization, see this thesis and its references

All of these are welcome in CSLib, but I think there are various technical difficulties in formalization. I came to the conclusion that it might be easiest if we have an intrinsically typed formalization of STLC to avoid some universe issues, but hadn't added this to CSLib yet.

[Sehun Kim]

Would you mind explaining what 'intrinsically typed' means?

[Chris Henson]

In the currently locally nameless formalization for instance, we first define untyped terms and types as data (not in Prop) then define a proposition that given a context and term we have a given typing derivation. This is extrinsic. For various reasons, this is nice to do in Lean for an idiomatic formalization that makes use of tactics.

In contrast, we could define a single inductive type that captures all of this, but is no longer a proposition. This is intrinsic typing. For universe reasons, I think this is easier to use with categorical semantics, but not what we really want elsewhere. (It is non-trivial to scale this formalization style to more complicated type systems.)

[Sehun Kim]

I see what you mean. Initially, I thought it would be straightforward to formalize this in an extrinsic setting, as it is in CSlib, but I did not anticipate that universe issues might arise.

Since I only needed it as an intermediary result, I had not examined it very deeply at first. However, because it is required for my subsequent work, I would like to ask whether there is any way I could help or contribute to this effort.

[Chris Henson]

Sehun Kim said:

However, because it is required for my subsequent work, I would like to ask whether there is any way I could help or contribute to this effort.

Yes, please feel free to work on this. We can definitely collaborate on what exactly ends up in CSLib. I'm still not sure precisely what you're aiming to formalize as an intermediate result, so it would help to revisit this once you have gotten further.