Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [linear-logic]

Logic with limited contraction and weakening.

10
votes
0answers
118 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 ...
5
votes
2answers
92 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{\...
8
votes
1answer
130 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 ...
7
votes
1answer
104 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 ...
4
votes
1answer
71 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
vote
1answer
114 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, ...
6
votes
1answer
204 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-...
1
vote
0answers
37 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 ...
6
votes
1answer
82 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 ...
10
votes
1answer
431 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 ...
8
votes
0answers
137 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
votes
0answers
70 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 ...
6
votes
1answer
200 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)....
3
votes
0answers
109 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} ...
9
votes
1answer
313 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 ...
13
votes
2answers
566 views

Can you explain an intuition behind Coherent Spaces?

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 ...
5
votes
1answer
244 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 ...
2
votes
1answer
176 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 ...
6
votes
1answer
294 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. ...
23
votes
6answers
2k 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 ...
15
votes
1answer
407 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\...
18
votes
4answers
711 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 ...
8
votes
1answer
438 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 \...
15
votes
1answer
342 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 ...
12
votes
1answer
2k 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 (...
11
votes
1answer
339 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 ...
23
votes
2answers
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 ...