# Tag Info

17

Other resources could be found referenced in Kaustuv Chaudhuri's thesis "The Focused Inverse Method for Linear Logic", and you might be interested in Roy Dyckhoff's "Contraction-Free Sequent Calculi", which is about contraction but not about linear logic. There are opportunities for efficient proof search in linear logic, but I don't think current work ...

15

Proof nets are interesting essentially for three reasons: 1) IDENTITY OF PROOFS. They provide an answer to the problem "when are two proofs the same"? In sequent calculus you may have many different proofs of the same proposition which differ only because sequent calculus forces an order among deduction rules even when this is not necessary. Of course, one ...

14

Let us call a logic "symmetric" where a $-A$ ("not A") assumption means the same as proving $A$ and a proof of $-A$ means the same as an assumption of $A$. Classical logic and linear logic are symmetric in this sense. Intuitionistic logic is not. Girard noticed that natural deduction is asymmetric in exactly this way. That is why it matches up with ...

11

I'm not sure this question is ideal for CSTheory, but given that it's already gathering upvotes, here is an answer somebody might have given had the question been posted on cs.stackexchange. In order to understand linear logic's notion of duality $(\cdot)^{\bot}$, which forces conjunction and disjunction apart much further than we are used to in ...

11

Assuming that the complexity of the provability problem would satisfy you, the landscape of complexities of substructural logics with and without contraction is somewhat complex. I'll try to survey here what is known for propositional linear logic and propositional logic. The short answer is that contraction sometimes helps (e.g. LLC is decidable, while LL ...

11

No, it is only ever harder. Just as the decision problem for intuitionistic propositional logic is harder than of classical propositional logic, so to is linear propositional logic harder still. With either exponentials (which don't lack contraction) or various flavours of noncommutative connective, the logic becomes undecidable and even the weakling ...

10

The intuition behind coherence spaces is that the elements of a coherence space represent observations of some underlying data, and the coherence relation tells you whether two observations could have come from the same piece of data. Concretely, suppose we have a set of animals Animals = {cat, duck, fish} Now, we can have a set of observations: ...

10

If additive commutations are omited in MALL, it's easy to show that the size of a proof decreases with every cut-elimination step. If additive commutations are allowed, the proof is not as easy, but it was provided in the original “Linear Logic” paper. It's called Small Normalization Theorem (Corollary 4.22, p71), which says that as long as the contraction–...

9

Perhaps Dale Miller's Overview of linear logic programming is a good strarting point?

9

This relates mostly to the "how they behave computationally" part of your question. One way to understand proof nets well from the computational perspective is by looking at slightly more concrete interpretations (eg., process algebraic). You might be interested in the following: The paper by Abramsky (the CLL section on Proof Expressions): Computational ...

9

I focus on how proof nets are related to sequent calculus, leaving more dynamic stuff. Proof nets abstract sequent calculus proofs: a proof net represents a set of sequent calculus proofs. Proof nets forget unimportant differences between sequent calculus proofs (like which formula is decomposed below which). The important theorem here is "...

9

For question 1, the answer is no, and is no for almost any type discipline (except certain intersection types): the fact that a term is (strongly or weakly) normalizable does not imply in general that it is typable. Typability implies termination, not the other way around. The specific case of of $\lambda EA$, however, brings up another issue which may be ...

8

First, note that nothing turns on the presence or absence of the empty type: if you have a nonlinear calculus with function types and unrestricted recursive types, then it is inconsistent. Indeed, your derivation works regardless of the type of the answer -- the very same term you have works for $\mu a.\; a \to X$ for any $X$. This is known as Curry's ...

8

I don't want to make a statement about "all linear lambda calculi" since it's hard to make that precise, but for pure linear lambda-calculus the answer is yes. One way to enforce linearity in pure lambda calculus is by trying to type application and abstraction using the linear implication $A \multimap B$, $$\frac{\Gamma \vdash t:A\multimap B\quad \Delta\... 8 Rob, I didn't know this was called the Tarskian Möglichkeit, but Martin Escardo and I have been studying this operator (A -> B) -> A, in the more general case when falsity is an arbitrary formula B, for the past few years, mainly in connection with computational interpretations of classical theorems. If we let B be fixed, then we define J A = (A -> B) -> A ... 7 (Gosh, Neel, that was a tough question.) The "folk model" of linear logic is definitely the coherent spaces model, discussed in Girard's Linear Logic paper (and also in "Proofs and Types"). This is not degenerate in the sense you describe. Whether this semantics throws any light on how a linear functional language can be implemented, I am not sure. When ... 6 Various people are interested in proving this sort of thing. Neel Krishnaswami mentioned this particular theorem here. I’ve also seen Frank Pfenning give some cool examples for ordered logics. For example, if you have A, x : [A], y : [A] \vdash e : [A], then in an ordered type system, e must append the lists x and y. The short answer is that yes, we ... 6 I always had trouble forming an intuition for coherence spaces, until I became more familiar with domain theory and read Girard's "The System F of variable types, fifteen years later". Coherence spaces are just a special kind of domain, and I found it much easier to understand what coherence means starting from there. I'll try to give an explanation that ... 5 You really should read Gowers' essay carefully - it cleanly details the reasons why you need a basis in general. So if there is going to be an algebraic account of Gauss-Jordan, it will necessarily involve some additional conditions. You can get an idea of the kinds of conditions by reading the n-lab page on dual vector spaces. There it shows that there ... 5 Your rule (\ast) is sometimes referred to as "absorption". I think the first who considered it was Jean-Marc Andreoli in his paper on focusing proofs. Indeed, it makes a lot of sense in proof search: read bottom-up, it says that when you have ?A (on the right), you may extract a copy of A and try and do something with it, while keeping ?A for future ... 5 No one knows if there are connections between GoI and GCT. It's quite plausible, since both are used to analyze complexity, and since GoI is formulated in terms of monoidal categories and GCT is based on representation theory. However, to my knowledge there aren't any researchers who understand both well enough to say for certain. 5 There has been a lot of work around the idea of statically checking the memory safety properties of programs. Francois Pottier give an excellent overview of various approaches in this presentation. The main technique you probably would be interested in is region typing. The Wikipedia article is quite complete, but the basic idea is to keep explicit regions ... 5 There has been interesting work recently on making the relation between proof net and focused calculi tighter, using "multi-focused" variants where you may have several simultaneous left holes, and studying "maximally focused" proofs. If you pick the calculus right, maximally-focused proofs can correspond to MLL proof nets or, in classical logic, to ... 4 You can check my paper "A survey of proof nets and matrices for substructural logics". Abstract: This paper is a survey of two kinds of "compressed" proof schemes, the \emph{matrix method} and \emph{proof nets}, as applied to a variety of logics ranging along the substructural hierarchy from classical all the way down to the nonassociative Lambek system. ... 4 I extend what I wrote as a comment. As there is a great number of cases in the proof, I only give an idea of why this transformation terminates. The short answer is: In the case promotion vs contraction, after the transformation, the number of contractions in the part of the proof containing cuts has decreased by one. To go a bit more into details, I would ... 4 For question 1, if by "deadlock" you mean "non-trivial vicious circle", then the answer is obviously yes, simply because a non-trivial vicious circle cannot be typed: you will have a cut between a formula A and a formula F containing A^\bot as strict subformula, so it is impossible that F=A^\bot. But this is kind of trivial: by refusing a priori to ... 3 Your observation about cut-elimination being faithfully represented in the unlabelled interaction nets is correct. However, the answer to your question is no. Let us call \delta the unique agent of the system. Such an agent is binary; we distinguish its two auxiliary ports by referring to as left and right. We call cell an occurrence of the agent in a ... 2 Here is a partial answer: the rule (*) is not conservative over SLL. Indeed, McKinley showed that soft linear set theory with unrestricted comprehension is nontrivial — but adding (*) makes it trivial, by the usual Russell/Curry argument: Given any proposition P, let C = \{ x \mid \;!(x\in x) \multimap P\}. Then if !(C\in C), by (*) we ... 2 Dependency is interesting because of equality, and equality is adjoint to contraction. As a result, substructural calculi (which in general omit contraction) do not have an obvious notion of equality. In type-theoretic language, equality is characterized by the following inference rule[*] being valid in both directions (top-to-bottom and bottom-to-top):$$ ...

Only top voted, non community-wiki answers of a minimum length are eligible