Questions tagged [linear-logic]
Logic with limited contraction and weakening.
34
questions
5
votes
2
answers
218
views
An untyped lambda calculus for explicit memory management
I am trying to find resources on a lambda calculus one would use for explicit memory management, assuming there is such a calculus.
The concept is as follows: one takes untyped lambda calculus, ...
- 291
1
vote
1
answer
179
views
Which are the rules for minimal logic in both sequent calculus and natural deduction styles?
Are there any references I could use which explictly contain the rules for minimal logic, both as a sequent calculus and in natural deduction? (Doesn't need to be the same reference for both!)
To give ...
- 387
10
votes
0
answers
235
views
True origin story of linear logic?
When I was a master's student in Paris I was exposed to the following standard narrative: "J.-Y. Girard invented coherence spaces, then he noticed the decomposition $A \to B~=~!A \multimap B$ and ...
4
votes
0
answers
268
views
Is there any logical concept that Rust lifetimes correspond to?
We're all used to invoking Curry–Howard to find correspondences between type systems and logical systems.
Rust has a very interesting type system, that is typically compared to a substructural logic. ...
- 487
-1
votes
1
answer
86
views
Is logic in computation of computation constructivist?
Is logic in computation of computation constructivist?
I think so, because dynamic languages are comparable to constructivist set theory (try a demonstration of the axiom of choice in computing: it ...
0
votes
0
answers
70
views
What does impredicativity mean in substructural and co-intuitionistic logics?
Predicative foundations puts restrictions on power sets and function sets.
Entirely apart from the philosophy predicative theories are a lot easier to prove things about and this sounds interesting to ...
5
votes
1
answer
364
views
How does linear logic achieve resource management?
TL;DR: I want to know how linear logic works. Sorry for the long question, I try to explain myself as best as I can in hopes of receiving good answers, especially because I don't know anyone else to ...
11
votes
0
answers
218
views
Do Banach spaces and linear contraction maps form a model of ILL with an exponential?
Recently, I read on the nLab that the category of Banach spaces and linear contractions is small complete, small cocomplete, and monoidal closed.
This means that Banach spaces and short linear maps ...
- 32.8k
6
votes
2
answers
217
views
A stronger multiplexing rule for soft linear logic?
In (intuitionistic) linear logic the usual rules for the storage modality $!$ are promotion, dereliction, contraction, and weakening:
$$\frac{!\Gamma\vdash A}{!\Gamma\vdash !A}(prom) \qquad \frac{\...
- 675
10
votes
1
answer
362
views
Parametricity of Linear Logic
Are we able to prove a free parametricity theorems about functions like $f : \forall A . [A] ⊸ [A]$?
It is supposed to state that $f$ takes a list and always returns a permutation of it.
Another ...
- 1,187
7
votes
1
answer
286
views
Does this variant of Multiplicative Linear Logic with mix rule enjoy cut elimination?
In Multiplicative Linear Logic (MLL), addition of the mix rule eliminates 'connectedness' from Danos-Regnier criterion. I'm investigating how the criterion changes if we do not distinguish between ...
- 1,187
4
votes
1
answer
104
views
Is the set of Multiplicative Proof Nets a proper subset of set of well formed single-agent Interaction Nets?
There are various criteria for the correctness of multiplicative proof nets.
In Correctness of Multiplicative Proof Nets is Linear, Stefano Guerrini nicely describes few of them with an efficient ...
- 1,187
1
vote
1
answer
180
views
How could one define a language based on the Calculus of Constructions, but with fixed points and EAL-style duplication restrictions?
Suppose that we take the Calculus of Constructions as a basis, but take away exponential functions (allowing only linear functions), and add the controlled duplication rules of EAL. That'd, I believe, ...
- 3,177
6
votes
1
answer
291
views
Algebraic account of Gaussian elimination?
For fun, I've been looking at the interpretation of linear logic in terms of finite-dimensional vector spaces, and ran into an interesting
question about the interpretation of double-negation-...
- 32.8k
1
vote
0
answers
49
views
Is it possible to use arbitrary fixpoint values on EAL without losing strong normalization?
From this question, the answerer states EAL-based languages can use arbitrary fixpoint types without losing strong normalization, because their normalization (and complexity) properties comes from ...
- 3,177
6
votes
1
answer
125
views
Can you assign a type to any term of the λEA-calculus?
The untyped language of System-F and similar is the λ-calculus. That language has terms that can't be typed on System-F, λx.(x x) λx.(x x) being the most obvious ...
- 3,177
12
votes
1
answer
723
views
What is the intuition behind linear logic?
I'm trying to understand linear logic to understand linear type systems better. However, when I read the rules, I fail to get an intuition behind it as I've done in modal logic - $\Box A$ means $A$ is ...
- 231
8
votes
1
answer
225
views
deciding $\beta$-equality of planar lambda terms
Mairson showed that the problem of computing the $\beta$-normal form of a linear lambda term (or equivalently, computing its principal type) is complete for polynomial time.
Harry Mairson. Linear ...
- 4,561
4
votes
0
answers
100
views
Coherence spaces and full completeness for the implicative fragment of linear logic
Linear logic isn't complete for coherence space semantics since $1$ and $\top$ get identified. But it is, I believe, complete for the fragment of linear logic whose only connective is $\multimap$.
I ...
- 453
6
votes
1
answer
387
views
Recursive types and the empty type
In John Mitchell's book "The Foundations of Programming Languages", he considers a typed lambda calculus with unit, exponential, product, (binary) coproduct types, and arbitrary recursive types (p126)....
- 453
2
votes
0
answers
123
views
Applications of the monoidal closed structure in LTL?
A simple model of temporal logic is via time-indexed truth
functions. This lets us model the Boolean connectives, as well as the
next-step operator and modal always operator:
$$
\begin{array}{lclll}
...
- 32.8k
8
votes
1
answer
409
views
Why does this cut elimination procedure terminate (contraction case)?
In Melliès’ survey Categorical Semantics of Linear Logic, a cut elimination procedure for intuitionistic linear logic is given which includes the following case:
3.9.3 Promotion vs. contraction
The ...
18
votes
2
answers
1k
views
How to think about coherent spaces intuitively?
Linear Logic is interpreted using coherent spaces, and they feature prominently in Girard's papers. I know all the three main ways to formally define them, and they don't really pose any problem to ...
- 487
5
votes
1
answer
669
views
Can all linear lambda calculi be linearity checked syntactically?
Given a lambda calculus with explicit linearity and usual application and abstraction, can the linearity check be done on an untyped syntax tree if we keep track of the structural types? Are the ...
- 53
2
votes
1
answer
252
views
Are there links between Geometry of Interaction and Geometric Complexity Theory?
I'm very much a novice in these subjects, but Geometry of Interaction and Geometric Complexity Theory seem to speak similar language and have vaguely similar goals. Am I not mistaken? Are there any ...
- 487
7
votes
1
answer
380
views
Type theory for memory safe data structures
Data structures such as a doubly linked list and a B+ tree have blocks of memory that have multiple pointers to it. This creates the risk that a bug will allow memory to be accessed after being freed.
...
- 83
29
votes
6
answers
3k
views
How should I think about proof nets?
In his answer to this question, Stephane Gimenez pointed me to a polynomial-time normalization algorithm for proofs in linear logic. The proof in Girard's paper uses proof nets, which are an aspect of ...
- 32.8k
15
votes
1
answer
532
views
Is MALL + unrestricted recursive types Turing-complete?
If you look at the recursive combinators in the untyped lambda-calculus, such as the Y combinator or the omega combinator:
$$
\begin{array}{lcl}
\omega & = & (\lambda x.\,x\;x)\;(\lambda x.\,x\...
- 32.8k
18
votes
4
answers
863
views
Automated theorem proving in linear logic
Is automatic theorem proving and proof searching easier in linear and other propositional substructural logics which lack contraction?
Where can I read more about automatic theorem proving in these ...
- 4,041
8
votes
1
answer
476
views
Can consume/produce be modeled in linear logic?
Question is whether it is possible to model in linear logic
two modes of access to a resource. I know that two modes
of resources are possible, i.e:
$!r \vdash$ r is infinitely available
$r \...
user4258
15
votes
1
answer
384
views
Looking for papers and articles on the Tarskian Möglichkeit
Some background: Łukasiewicz many-valued logics were intended as modal logics, and Łukasiewicz gave an extensional definition of the modal operator:
$\Diamond A =_{def} \neg A \to A$ (which he ...
- 815
15
votes
1
answer
3k
views
Data structures in programming language with linear types
Assume we are dealing with a programming language that has support for linear types (terms of linear type can be used at most once, so to say). This allows for treating some computational effects (...
user3722
12
votes
1
answer
388
views
When do coherence spaces have pullbacks and pushouts?
$\newcommand{\symp}{\Bumpeq}$
A coherence relation $\symp_X$ on a set $X$ is a reflexive and symmetric relation. A coherence space is a pair $(X, \symp_X)$, and a morphism $f : X \to Y$ between ...
- 32.8k
25
votes
2
answers
1k
views
What is the folk model of linear logic?
Probably the most common application of linear types in PL is to use them to give languages which control aliasing (i.e., a linear value has a single pointer to it, more or less).
But there's a ...
- 32.8k