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.
Cody Roux (Apr 24 2020 at 17:41):Ok I'm finally creating a topic for this, now that I finally have a day off. The idea is to try to summarize the main ideas of normalization by evaluation, namely how they pertain to certain categorical concepts like Presheaves and Sheaves, the Yoneda lemma, categorical models of type theory, categorical glueing and global sections.
Cody Roux (Apr 24 2020 at 17:42):I feel like @Dan Doel, @Mike Shulman have some special insight into this...
Cody Roux (Apr 24 2020 at 17:43):Also possibly @Steve Awodey
Cody Roux (Apr 24 2020 at 17:48):The starting point, AFAIK, is this paper: https://dl.acm.org/doi/10.1017/S0960129597002508
Dan Doel (Apr 24 2020 at 17:51):I think that paper is kind of an anomaly. It uses a rather different approach than many of the others.
Dan Doel (Apr 24 2020 at 17:52):I like it better, because it feels more like NbE just falling out of categorical stuff automatically, while the rest are more explicit constructions.
Cody Roux (Apr 24 2020 at 17:58):My goal is to see if this paper reconstructs into proofs of normalization for categories with sums, and a simple version of MLTT
Cody Roux (Apr 24 2020 at 17:58):But there are some subtleties about the paper itself I don't quite understand though.
Mike Shulman (Apr 24 2020 at 19:18):My only insight is to hand you off to someone else's insight: https://arxiv.org/abs/1809.08646.
Mike Shulman (Apr 24 2020 at 19:20):Jon Sterling recently shared with me a draft of an even better categorical reconstruction of NbE. He doesn't appear to be on this zulip (though perhaps @Bas Spitters is), but he's on the HoTT zulip so you could ask there.
Dan Doel (Apr 24 2020 at 19:22):Oh yeah. I still haven't had time to fully digest that paper.
Dan Doel (Apr 24 2020 at 19:25):It seems like this is in the less 'magical' line of things, though. Like, talking about presheaves of neutral terms and normal forms seems motivated by experience with syntactic handling of type theory, whereas the first paper above somehow seems to avoid talking about that.
Dan Doel (Apr 24 2020 at 19:26):Although maybe it's just hidden somehow.
Dan Doel (Apr 24 2020 at 19:31):I think maybe the enriched setting lets you do that? The first paper above notes that if you just carry out their argument with normal categories, you don't get anything interesting. So talking about neutral and normal presheaves may be a way of staying in the ordinary setting.
Dan Doel (Apr 24 2020 at 19:33):Anyhow, the method that talks about neutral/normal terms is significantly more developed as far as I can tell. I only know of that one paper for the other one.
Dan Doel (Apr 24 2020 at 19:38):Well, maybe that's not quite true, but I guess the other sort of paper isn't specifically about NbE.
Dan Doel (Apr 24 2020 at 19:46):@Cody Roux You might want to study this as well: https://arxiv.org/pdf/1905.05636.pdf
It uses enriched categories to talk about various notions of operational semantics for Lawvere theories. And of course it mentions that being set-enriched is like denotational semantics. The paper you linked is PER-enriched instead, and I think an important part is that you can equip the same set with multiple PERs. So, you can equip the lambda terms with α equality or αβη equality, but they have the same underlying set. So I guess that is an alternate way of constructing the right presheaves without getting into details that seem motivated by syntactic normalization.
Mike Shulman (Apr 24 2020 at 19:57):I think Jon once explained to me why he thought the normal/neutral approach was better than the PER-enriched-category approach, but I don't remember now. Or maybe I'm misremembering.
Dan Doel (Apr 24 2020 at 20:00):Well, one reason I can think of is that you want normalization to actually produce the things that are free of redexes. The PER argument just gives you a canonical witness of each equivalence class, and it only gives you the actual normal form because of the exact details of their proof, I think.
Dan Doel (Apr 24 2020 at 20:01):Although maybe if you enriched in something potentially directed instead, that could be made to necessarily work out.
Cody Roux (Apr 24 2020 at 20:05):Something that seems important to me is A) Building an equivalence checker and B) Proving the disjunction property. A) because that's what's actually needed for implementation and B) because it implies consistency and all that proof-theoretic good stuff like the subterm property and interpolation.
Cody Roux (Apr 24 2020 at 20:06):Neither of those really need neutral terms as a concept. Alternately, if the definition of neutral terms could arise organically from the theoretical model, that would be swell. It's quite a subtle concept (at first) particularly in the presence of connectives. Also, the notion of eta normal forms can be quite finicky
Philip Saville (Apr 24 2020 at 20:21):For more references, there's a lot of work in this area by Thorsten Altenkirch and coauthors : for dependent types https://dl.acm.org/doi/10.1109/LICS.2007.33 and https://lmcs.episciences.org/4005/pdf, and for coproducts (but no empty type if I remember right) https://dl.acm.org/doi/10.5555/871816.871869.
Philip Saville (Apr 24 2020 at 20:26):For neutral and normal terms, Phil Scott told me that they considered it a benefit of their approach that they never had to work with neutral terms -- they wanted it to be completely algebraic (though they need neutral terms at the end to prove they have actually got the normal forms). I have looked for but never found a really conceptual explanation of what neutral terms really do in categorical versions of NbE. The closest I know of is around Lemma 3 of Fiore's semantic treatment of NbE for stlc https://www.cl.cam.ac.uk/~mpf23/papers/Types/nbe.pdf. It seems somewhat related to the "standardisation" theorems for lambda calculus but it's not clear there's a connection
Cody Roux (Apr 24 2020 at 20:33):I'm actually mostly aware of all these references, I'm trying to understand and synthesize them, mostly. Not to say they aren't very appreciated though!
Cody Roux (Apr 24 2020 at 20:34):Standardization is certainly a crucial lemma in proofs of strong normalization, and there's a fascinating paper relating the so-called "Girard conditions" to sheaves: https://repository.upenn.edu/cgi/viewcontent.cgi?article=1141&context=ircs_reports. I never was able to understand whether this was related to anything else, though.
Philip Saville (Apr 24 2020 at 20:44):Cody Roux said:
My goal is to see if this paper reconstructs into proofs of normalization for categories with sums, and a simple version of MLTT
am I right in understanding that you are aiming for a Scott et al NbE argument for these cases^^ ? I take it the Altenkirch-Scott paper doesn't do what you want? Just trying to get a sense of the target!
(I have seen the Gallier paper but never got round to learning the prerequisites for it...)
Dan Doel (Apr 25 2020 at 01:15):Oh, Jon's paper actually explains the gist of what's going on in the two approaches, and for the P-category one it's essentially what I said above, and the same as the Lawvere theory paper.
Dan Doel (Apr 25 2020 at 01:16):The set category version requires you to pre-quotient your syntax, so the 'normalization' is trivial, while the PER-enriched setting lets you work with unquotiented sets, and observe more details of the actual procedure.
Dan Doel (Apr 25 2020 at 01:16):End of section 2.
Dan Doel (Apr 25 2020 at 01:30):Anyhow, I think this paper seems great for laying out a categorical/algebraic framework for thinking about syntactic issues that type theorists traditionally think about (which, I think, is the goal). However, if you want NbE to automatically fall out of general categorical principles without thinking about syntactic details, it's probably not that.
Cody Roux (Apr 25 2020 at 02:39):That's mostly what I want, or at least I want the syntactic details to be well isolated. But I'll check these papers again and try to summarize the big ideas. As far as I know, there hasn't been a categorical reconstruction of the normalization proof for dependent type theory though, right?
Mike Shulman (Apr 25 2020 at 02:45):Dan Doel said:
Oh, Jon's paper actually explains the gist of what's going on in the two approaches, and for the P-category one it's essentially what I said above, and the same as the Lawvere theory paper.
Yes, but it doesn't really explain why they prefer their approach, which is what I was trying to reconstruct.
Dan Doel (Apr 25 2020 at 02:46):Yeah, not sure about that.
Liang-Ting Chen (Nov 12 2020 at 07:37):Is there any paper on PER-topos or alike? It seems that to generalise Scott et al’s arguments to other more sophisticated type theories it is natural to look for topos enriched over PER if one wants to avoid the syntactic approach to NbE.
Dan Doel (Nov 12 2020 at 15:24):@Liang-Ting Chen You should look at Andrej Bauer's thesis. Modest sets are essentially the same as PERs, I believe; just a different vocabulary/emphasis.
Dan Doel (Nov 12 2020 at 15:26):Also anything else about modest sets, I guess. I was working through this years ago, but never got to the modest sets part. But it might be good.
Dan Doel (Nov 12 2020 at 15:33):Oh wait, maybe this is better for your other question in the topos theory thread. Is your question here about toposes developed with PER-enriched categories? I haven't seen that.
Liang-Ting Chen (Nov 13 2020 at 02:35):Oh, that's two different questions but somehow relevant to me. I happen to work on a topos which is also enriched over PER. This reminds me the paper by Cubric et al. It seems possible to apply their arguments to dependent type theories in this setting. The syntactic approach via neutral/normal terms is popular, and the other approach does not seem to scale very well. Yet, as there is always some CT ninja who can show everything is an instance of Yoneda lemma, I am just curious if this is also a result of some more general theorem. :grinning_face_with_smiling_eyes:
Dan Doel (Nov 13 2020 at 02:48):Ah, yeah. That's the only paper of that sort that I've seen. I've also heard of people studying "E-categories" which are enriched in setoids, basically. Not sure how thorougly developed that is, though, or how it'd translate.
Liang-Ting Chen (Nov 13 2020 at 03:53):Alright, thanks. At least I know where we are.
Cody Roux (Dec 04 2020 at 16:12):Obviously Thorsten Altenkirsh's PhD is also relevant. Are you interested in a Topos of PERs, or a PER enriched Topos?
Liang-Ting Chen (Dec 05 2020 at 13:25):The latter. It might be used to integrate Cubric et al’s approach to more sophisticated models of type theory.