Special Issue for the Conferences on Computer Science Logic and Logic in Computer Sciences (CSL-LICS) 2014

Editors: Thomas A Henzinger, Dale Miller

The Vienna Summer of Logic in July 2014 attracted a great number of researchers working in logic to Vienna. To take advantage of this unprecedented confluence of logicians, especially those working in computational logic, the organizers of the CSL and LICS series of meetings decided to merge the 2014 editions of these meetings into one meeting titled the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). This joint meeting had one program committee, one program, and one proceedings.

A small number of papers from the proceedings were selected and their authors were invited to submit a full version of their paper to this special issue. All submissions were refereed according to the usual standards of LMCS with each paper being reviewed by three experts in the field. We are grateful to the authors for their excellent submissions and to the reviewers for their efforts to evaluate and improve these papers.

Thomas A. Henzinger and Dale Miller
CSL-LICS 2014, Program Committee Chairs

1. Preservation and decomposition theorems for bounded degree structures

Frederik Harwath ; Lucas Heimberg ; Nicole Schweikardt.

We provide elementary algorithms for two preservation theorems for first-order sentences (FO) on the class âd of all finite structures of degree at most d: For each FO-sentence that is preserved under extensions (homomorphisms) on âd, a âd-equivalent existential (existential-positive) FO-sentence can be constructed in 5-fold (4-fold) exponential time. This is complemented by lower bounds showing that a 3-fold exponential blow-up of the computed existential (existential-positive) sentence is unavoidable. Both algorithms can be extended (while maintaining the upper and lower bounds on their time complexity) to input first-order sentences with modulo m counting quantifiers (FO+MODm). Furthermore, we show that for an input FO-formula, a âd-equivalent Feferman-Vaught decomposition can be computed in 3-fold exponential time. We also provide a matching lower bound.

2. Proof equivalence in MLL is PSPACE-complete

Willem Heijltjes ; Robin Houston.

MLL proof equivalence is the problem of deciding whether two proofs in multiplicative linear logic are related by a series of inference permutations. It is also known as the word problem for star-autonomous categories. Previous work has shown the problem to be equivalent to a rewiring problem on proof nets, which are not canonical for full MLL due to the presence of the two units. Drawing from recent work on reconfiguration problems, in this paper it is shown that MLL proof equivalence is PSPACE-complete, using a reduction from Nondeterministic Constraint Logic. An important consequence of the result is that the existence of a satisfactory notion of proof nets for MLL with units is ruled out (under current complexity assumptions). The PSPACE-hardness result extends to equivalence of normal forms in MELL without units, where the weakening rule for the exponentials induces a similar rewiring problem.

3. (Leftmost-Outermost) Beta Reduction is Invariant, Indeed

Beniamino Accattoli ; Ugo Dal Lago.

Slot and van Emde Boas' weak invariance thesis states that reasonable machines can simulate each other within a polynomially overhead in time. Is lambda-calculus a reasonable machine? Is there a way to measure the computational complexity of a lambda-term? This paper presents the first complete positive answer to this long-standing problem. Moreover, our answer is completely machine-independent and based over a standard notion in the theory of lambda-calculus: the length of a leftmost-outermost derivation to normal form is an invariant cost model. Such a theorem cannot be proved by directly relating lambda-calculus with Turing machines or random access machines, because of the size explosion problem: there are terms that in a linear number of steps produce an exponentially long output. The first step towards the solution is to shift to a notion of evaluation for which the length and the size of the output are linearly related. This is done by adopting the linear substitution calculus (LSC), a calculus of explicit substitutions modeled after linear logic proof nets and admitting a decomposition of leftmost-outermost derivations with the desired property. Thus, the LSC is invariant with respect to, say, random access machines. The second step is to show that LSC is invariant with respect to the lambda-calculus. The size explosion problem seems to imply that this is not possible: having the same notions of normal form, evaluation in the LSC is exponentially longer than in […]

4. On the characterization of models of H*: The semantical aspect

Flavien Breuvart.

We give a characterization, with respect to a large class of models of untyped lambda-calculus, of those models that are fully abstract for head-normalization, i.e., whose equational theory is H* (observations for head normalization). An extensional K-model $D$ is fully abstract if and only if it is hyperimmune, {\em i.e.}, not well founded chains of elements of D cannot be captured by any recursive function. This article, together with its companion paper, form the long version of [Bre14]. It is a standalone paper that presents a purely semantical proof of the result as opposed to its companion paper that presents an independent and purely syntactical proof of the same result.