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.
created computational trinitarianism, combining a pointer to an exposition by Bon Harper (thanks to David Corfield) with my table logic/category-theory/type-theory.
brief category:people-entry for hyperlinking references at dependent linear type theory and elsewhere
stub for quantum computation
brief category:people-entry for hyperlinking references at quantum error correction and at quantum computation
brief category:people-entry for hyperlinking references at dependent linear type theory
Following discussion in some other threads, I thought one should make it explicit and so I created an entry
Currently this contains some (hopefully) evident remarks of what “dependent linear type theory” reasonably should be at least, namely a hyperdoctrine with values in linear type theories.
The entry keeps saying “should”. I’d ask readers to please either point to previous proposals for what “linear dependent type theory” is/should be, or criticise or else further expand/refine what hopefully are the obvious definitions.
This is hopefully uncontroversial and should be regarded an obvious triviality. But it seems it might be one of those hidden trivialities which deserve to be highlighted a bit more. I am getting the impression that there is a big story hiding here.
Thanks for whatever input you might have.
added a definition to beta-gamma system
added pointer to:
I had given it an Lab page already a while back, so that I could stably link to it without it being already there:
Now it’s even “there” in the sense of being incarnated as a pdf.
a bare list of references, to be !includ-ed into the list of references of relevant entries, such as at quantum computing and quantum programming, for ease of updating and syncing
brief category:people-entry for hyperlinking references at quantum circuit diagram
brief category:people-entry for hyperlinking references at quantum computation and quantum information
brief category:people-entry for hyperlinking references at quantum computation and quantum information
brief category:people-entry for hyperlinking references at quantum computation and quantum information
Aleks Kissinger has contacted me about his aims to start a collection of nLab entries on quantum information from the point of view of the Bob Coecke school.
Being very much delighted about this offer, I created a template entry quantum information for his convenience.
brief category:people-entry for hyperlinking references at quantum programming language
a stub, to make links work
(This used to be a stub “quantum circuit” which I just quasi-duplicated at a more extensive entry quantum circuit diagram. But since quantum gate was already redirecting here – which is how I discovered/remembered that this entry exists – no harm is done by making that it’s new title.)
created a stub for holographic entanglement entropy in reaction to this MO question.
added to identity type a mentioning of the alternative definition in terms of inductive types (paths).
brief category:people-entry for hyperlinking references at IKKT matrix model
for completeness, to go alongside Mallows kernel
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.
have expanded the Idea-section at quantum logic to now read as follows:
Broadly speaking, quantum logic is meant to be a kind of formal logic that is to traditional formal logic as quantum mechanics is to classical mechanics.
The first proposal for such a formalization was (Birkhoff-vonNeumann 1936), which suggested that given a quantum mechanical system with a Hilbert space of states, the logical propositions about the system are to correspond to (the projections to) closed subspaces, with implication given by inclusion of such subspaces, hence that quantum logic is given by the lattice of closed linear subspaces of Hilbert spaces.
This formalization is often understood as being the default meaning of “quantum logic”. But the proposal has later been much criticized, for its lack of key properties that one would demand of a formal logic. For instance in (Girard 11, page xii) it says:
Among the magisterial mistakes of logic, one will first mention quantum logic, whose ridiculousness can only be ascribed to a feeling of superiority of the language – and ideas, even bad, as soon as they take a written form – over the physical world. Quantum logic is indeed a sort of punishment inflicted on nature, guilty of not yielding to the prejudices of logicians… just like Xerxes had the Hellespont – which had destroyed a boat bridge – whipped.
and for more criticisms see (Girard 11, section 17).
Therefore later other proposals as to what quantum logic should be have been made, and possibly by “quantum logic” in the general sense one should understand any formal framework which is supposed to be able to express the statements whose semantics is the totality of all what is verifiable by measurement in a quantum system.
In particular it can be argued that flavors of linear logic and more generally linear type theory faithfully capture the essence of quantum mechanics (Abramsky-Duncan 05, Duncan 06, see (Baez-Stay 09) for an introductory exposition) due to its categorical semantics in symmetric monoidal categories such as those used in the desctiption of finite quantum mechanics in terms of dagger-compact categories. In particular the category of (finite dimensional) Hilbert spaces that essentially underlies the Birkhoff-vonNeumann quantum logic interprets linear logic.
Another candidate for quantum logic has been argued to be the internal logic of Bohr toposes .
In quantum computing the quantum analog of classical logic gates are called quantum logic gates.
I incorporated some of my spiel from the blog into the page type theory.
I started an article about Martin-Löf dependent type theory. I hope there aren't any major mistakes!
One minor point: I overloaded $\mathrm{cases}$ by using it for both finite sum types and dependent sum types. Can anyone think of a better name for the operation for finite sum types?
I created a stub certified programming.
That’s motivated from me having expanded the Idea-section at type theory. I enjoyed writing the words “is used in industry”. There are not many Lab pages where I can write these words.
I am saying this only half-jokingly. Somehow there is something deep going on.
Anyway, in (the maybe unlikely) case that somebody reading this here has lots of information about the use and relevance of certified programming in industry, I’d enjoy seeing more information added to that entry.
one more in the list of quantum programming languages
stub for homotopy type theory
brief category:people-entry for hyperlinking references at certified programming
brief category:people-entry for hyperlinking references at verified programming and at cryptography
Stub. For now just recording links which go beyond the scope of arithmetic cryptography.
brief category:people-entry for hyperlinking references at verified programming
brief category:people-entry for hyperlinking references at verified programming
I am trying to collect citable/authorative references that amplify the analog of the mass gap problem in particle phenomenology, where it tramslates into the open problem of computing hadron masses and spins from first principles (due to the open problem of showing existence of hadrons in the first place!).
This is all well and widely known, but there is no culture as in mathematics of succinctly highlighting open problems such that one could refer to them easily.
I have now created a section References – Phenomenology to eventually collect references that come at least close to making this nicely explicit. (Also checked with the PF community here)
I have made explicit the example of involutive Hopf algebras, and how most of the other examples previously listed here are special cases of this one. Also expanded a little and organized it all into a new Examples-subsection (here)
added to the Properties-section at Hopf algebra a brief remark on their interpretation as 3-vector spaces.
An old query at twisting cochain which was reaction to somebody putting that the motivation is the homological perturbation lemma:
It is equally true that it is related to 20 more areas like that one (which is not the central). Brown’s paper on twisting cochains, is much earlier than homological perturbation theory. basic idea was to give algebraic models for fibrations. Nowedays you have these things in deformation theory, A-infty, gluing of complexes on varieties, Grothendieck duality on complex manifolds (Toledo-Tong), rational homotopy theory etc. One should either give a fairly balanced view to all applications or not list anything, otherwise it is not fair. This should be done together with massive expansion of Maurer-Cartan equation what is almost the same topic. The same with literature: Smirnov’s book on simplicial and operadic methods in algebraic topology is the most wide reference for twisting cochains and related issues in algebraic topology setup; Keller wrote much and well about this and Lefèvre-Hasegawa thesis (pdf) is very good, and the first reference is E. Brown’s paper from 1959. For applications in deformation theory there are many references, pretty good one from dg point of view and using 2-categorical picture of def functors is a trilogy of Efimov, Lunts and orlov on the arXiv. Few days ago Sharygin wrote a long article on twisting cochains on the arXiv, with more specific purposes in index theory. Interesting is the application of Baranovsky on constructing universal enveloping of L infty algebra. – Zoran
Urs: concerning the “either give a fairly balanced view to all applications or not list anything”, I can see where you are coming from, Zoran, but I would still prefer here to have a little bit of material than to have none. The Lb is imperfect almost everywhere, we’ll have to improve it incrementally as we find time, leisure and energy. But it’s good that you point out further aspects in a query box, so that we remember to fill them in later.
Zoran Skoda My experience is that correcting a rambling and unbalanced entries takes more time than writing a new one at a stage when you really work on it. Plus all the communication explaining to others who made original entry which is hastily written. When it becomes very random and biased I stopped enjoying it at all to work on it.
Ronnie Brown It may not possible for one person to give a “balanced entry” and is certainly not possible for me in this area. On the other hand, this may be endemic to the description of an area of maths for students and research workers.
An advantage of the Homological Perturbation Lemma (HPL) is that it is an explicit formula, and this has been exploited by various writers, especially Gugenheim, Larry Lambe and collaborators, Huebschmann, and others, for symbolic computations in homological algebra. It is good of course to have the wide breadth of applications of twisting cochains explained.
For me, an insight of the HPL was the explicit use of the homotopies in a deformation retract situation to lead to new results. This has been developed to calculate resolutions of groups, where one is constructing inductively a universal cover of a with its contracting homotopy.
So let us continue to have various individually “unbalanced” points of view explained in this wiki, to let the readers be informed, and decide.
Toby: Knowing basically nothing about this, I prefer to see various people explain their own perspectives. Even if they don't try to take the work to integrate them.