Editors: Thomas A Henzinger, Dale Miller

We provide elementary algorithms for two preservation theorems forfirst-order sentences (FO) on the class âd of all finite structures of degreeat 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 iscomplemented by lower bounds showing that a 3-fold exponential blow-up of thecomputed existential (existential-positive) sentence is unavoidable. Bothalgorithms can be extended (while maintaining the upper and lower bounds ontheir time complexity) to input first-order sentences with modulo m countingquantifiers (FO+MODm). Furthermore, we show that for an input FO-formula, aâd-equivalent Feferman-Vaught decomposition can be computed in 3-foldexponential time. We also provide a matching lower bound.

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

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

We give a characterization, with respect to a large class of models ofuntyped lambda-calculus, of those models that are fully abstract forhead-normalization, i.e., whose equational theory is H* (observations for headnormalization). An extensional K-model $D$ is fully abstract if and only if itis hyperimmune, {\em i.e.}, not well founded chains of elements of D cannot becaptured 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 ofthe result as opposed to its companion paper that presents an independent andpurely syntactical proof of the same result.