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.
Paolo Perrone (Jul 01 2020 at 20:24):Hello all! This is the thread of discussion for the talk of Vladimir Zamdzhiev, "Computational Adequacy for Substructural Lambda Calculi".
Date and time: Friday July 10, 16:40 UTC.
Zoom meeting: https://mit.zoom.us/j/7488874897
YouTube live stream: https://www.youtube.com/watch?v=EVNjVmjJtrs&list=PLCOXjXDLt3pZDHGYOIqtg1m1lLOURjl1Q
Paolo Perrone (Jul 10 2020 at 15:20):Hello all. Please note the "new" Zoom address: https://mit.zoom.us/j/7488874897
Paolo Perrone (Jul 10 2020 at 16:30):The talk will start in 10 minutes! https://mit.zoom.us/j/7488874897
Valeria de Paiva (Jul 10 2020 at 18:41):hi @Vladimir, the question I had was to do with the fact that whenever you have recursion, you already have lost your logical Curry-Howard connection, as every type needs to be inhabited, so the logic is inconsistent.(this was the traditional view, spelled out by Gordon Plotkin in his 1993 LICS invited talk) so the argument in your paper seems to me a bit back to front when you say
"We also show, under basic assumptions, that interpreting lambda abstractions via a monoidal closed structure (a popular method for linear type systems) necessarily leads to degenerate and inadequate models for call-by-value affine type systems". there's nothing degenerate and inadequate about monoidal closed structure, it's the non-terminating object that causes the problem, which it already caused in the intuitionistic setting.
Paolo Perrone (Jul 10 2020 at 21:14):Video here!
https://www.youtube.com/watch?v=rcBg24AjWWk&list=PLCOXjXDLt3pYot9VNdLlZqGajHyZUywdI
Vladimir Zamdzhiev (Jul 12 2020 at 17:59):Hi Valeria,
The degeneration in the categorical model is caused by the combination of the following:
This is proven in my paper. If you take any two of the above, then it is possible to construct non-degenerate models. In particular, there are adequate models for linear type systems with recursion where lambda abstractions are interpreted by monoidal closure. I list several such examples in my paper.
But I see how what I wrote in the abstract can be a little confusing. I will reword it to:
"We also show, under basic assumptions, that interpreting lambda abstractions via a monoidal closed structure (a popular method for linear type systems) necessarily leads to degenerate and inadequate models for call-by-value affine type systems with recursion."
Hopefully this should clear any confusion. Thanks for the feedback!
Valeria de Paiva (Jul 12 2020 at 23:08):Hi Vladimir, thanks! the rewriting of the sentence already improves things for me! But I don't think you can have non-degenerate models of Weakening and Recursion. Recursion and a totally linear system work together for some version of "work together" as in the thesis of Torben Brauner (http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=33C5FEC7DFE2B8A62B235D53BC6913E5?doi=10.1.1.71.7991&rep=rep1&type=pdf, https://www.seas.upenn.edu/~sweirich/types/archive/1995/msg00375.html), but this is a kind of a degenerate way too, as the whole of domain theory works by moving into a logic that is inconsistent: every type needs to be inhabited, as the non-terminating element is an element of every type. But I haven't read your paper carefully enough, I will check it.
Vladimir Zamdzhiev (Jul 13 2020 at 11:15):By "degenerate model" I mean a category which is categorically equivalent to 1, i.e., every homset has only one morphism. Obviously, when recursion is allowed, the corresponding logic is inconsistent. But the categorical model may still be non-degenerate in the sense I just described.