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 ...


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

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 ...


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: ...


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\...


7

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 ...


7

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 ...


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

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

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