Talk:Linear logic
From Wikipedia, the free encyclopedia
 |
This article is within the scope of the WikiProject Philosophy, which collaborates on articles related to philosophy. To participate, you can edit this article or visit the project page for more details. | ||||||||
| ??? | This article has not yet received a rating on the quality scale. | ||||||||
| ??? | This article has not yet received an importance rating on the importance scale. | ||||||||
|
|||||||||
TODO:
- better examples
- connexion to proof nets, ludics, etc.
- linear type theory (Wadler et al)
--Kaustuv Chaudhuri 00:03, 2 Jun 2004 (UTC)
- make it less chatty. Please snip "non-encyclopedic" parts.
--Kaustuv Chaudhuri 09:06, 2 Jun 2004 (UTC)
There are two kinds of non-commutativity: self-dual and non-self-dual. Discussion required. Charles Stewart 02:47, 12 Aug 2004 (UTC)
"While this freeness of truth is usually what is desired, for example in formal mathematics, but for many applications of logic truth can be abstract and unwieldy." I think the word "While" should be removed, changing the sentence to 2 sub-sentences joined by the conjunction "but". But I don't understand the subject well enough to know if that's what he meant to say. Art LaPella 02:14, Aug 21, 2004 (UTC)
- Either the "but" or the "while" should be removed. On a more general note, the present version of this article has major expository issues: it is currently not accessible to the lay reader. Examples that should be illuminating are obscure and ill-constructed. — Kaustuv 03:27, 2004 Aug 21 (UTC)
[edit] Internal and external choice
Can someone please confirm that the names given for the & and ⊕ operators are really internal and external choice, respectively. The reason I ask is that this is exactly the opposite to what I've encountered in other contexts, e.g. process algebra, where an internal choice is one you can't control and an external choice is one you can. I didn't find the names in the papers linked off the bottom of the article (but I only skimmed them).--Malcohol 14:47, 11 August 2006 (UTC)
- I have removed the names as I don't think they are common, and anyway it is probably not meant to be opposite to other computational contexts. 192.75.48.150 18:38, 11 August 2006 (UTC)
[edit] Intuitionstic linear implication
I expect the answer is {{sofixit}}, but:
- Intuitionistic linear logic (ILL) allows only a single conclusion. Unlike CLL, connectives in ILL do not have perfect duals... As a result, linear implication is a basic connective in ILL.
The statement is correct, but the rules for linear implication are not given in the article. They should be. 72.137.20.109 03:52, 2 January 2007 (UTC)
Does linear logic have a not function?
- To answer the previous two questions: there is a linear negation, but it and linear implication are not given in the table of rules (for the CLL sequent calculus). I can't edit that table, and there is some sense to its organisation for purposes of symmetry, and in fact there are (now) explained after it, but I'll try to make that clearer. --Toby Bartels 20:29, 29 June 2007 (UTC)
-
- It depends what you mean by a "not". There's a perfectly good involution which (in the presence of contraction and weakening) would be equivalent to classical not, but which is not the same as linear negation (implies falsity). Francis Davey 09:14, 18 October 2007 (UTC)
Mostly, this makes sense, but the explanations for the & and ? operators really need some work. Can someone who understands this look into it?
[edit] Vending-machine example
I know it seems less professional, but the vending-machine example was much clearer to me when it was in first person rather than third. Having just read a bunch of stuff on linear logic, I think that I finally understand things (at least as far as the distinction between times and par; 1 versus bottom is still subtle). So I'm going to rewrite much of that (especially the bit on par) using what seems the clearest language of all (IMHO): the second person! --Toby Bartels 20:32, 29 June 2007 (UTC)
