Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
collected some references on the interpretation of the !-modality as the Fock space construction at !-modality.
Cross-linked briefly with he stub entries_Fock space_ and second quantization.
I de-stubbified !-modality with some discussion of the various ways to interpret it categorically.
I added to !-modality some comments about term calculi.
It seems that !-modality doesn’t render as a link on some pages, e.g., at Fock space. Is there a problem starting with ’!’ ?
Thanks for the alert. I am fixing it in the entries. “exponential modality” is a better link word, anyway.
But of course there remains a bug which would be good to fix in any case. So I have moved the non-rendering “!-modality”-link to the Sandbox.
OK, have changed a number of links.
I’m currently on holiday, and unfortunately will not be able to look at the bug for at least a week. Would it be possible to create a single thread ’Bugs and feature requests’ where all bugs and feature requests are registered (and maybe a note could be added to the HowTo to this effect)? It is then much less likely that I will forget about or overlook something. To keep it easy to get an overview, maybe discussion can be avoided in that thread, and instead when registering the bug one can link to a thread where one can discuss it?
I have a vague memory of reading a paper that decomposed the !-modality into two separate modalities, one that allows only contraction and another that allows only weakening. Does anyone know a reference doing something like that?
This paper does something like that, though for the closely related “tensor logic” rather than linear I think.
Thanks. I don’t think that’s the paper I was half-remembering, but it’s useful to have.
Added these pointers:
A quantum programming language based on this linear/non-linear type theory adunction is QWIRE:
applied to verified programming after implementation in Coq:
and using ambient homotopy type theory:
also pointer to:
added cross-links by !include
-ing the logic symbols – table
added pointer to:
I have fixed and completed this bibitem:
here and in a couple of other entries.
(It also appears at linear-non-linear logic and still needs to be reformatted there, but that entry is suffering from some bug which prevents it from being edited. I have contacted the technical team about it.)
also polished up this bibitem:
I have recovered this reference here via the WaybackMachine:
Unfortunately, the pdf is just a tad larger than the upload limit for the nLab server. I have tried to compress it a little, but couldn’t quite bring it below the threshold.
So for the time being the pdf is sitting in my Dropbox.
1 to 27 of 27