bluuebunny/crossref_metadata_2025 huggingface dataset:
Topological Completeness for Higher-Order Logic
Authors: Awodey Steve , Butz Carsten
Published: February 2016

Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces - so-called "topological semantics". The first is classical higher order logic, with relational quantification of finitely high type; the second system is a predicative fragment thereof with quantification over functions between types, but not over arbitrary relations. The second theorem applies to intuitionistic as well as classical logic.
Syntax and Semantics of the logic L_omega omega^lambda
Authors: Butz Carsten
Published: February 2016

In this paper we study the logic L_omega omega^lambda , which is first order logic
 extended by quantification over functions (but not over relations).
 We give the syntax of the logic, as well as the semantics in Heyting
 categories with exponentials. Embedding the generic model of a theory
 into a Grothendieck topos yields completeness of L_omega omega^lambda with respect
 to models in Grothendieck toposes, which can be sharpened to completeness
with respect to Heyting valued models. The logic L_omega omega^lambda is the
strongest for which Heyting valued completeness is known. Finally,
we relate the logic to locally connected geometric morphisms between toposes.
On the Arithmetical Content of Restricted Forms of Comprehension, Choice and General Uniform Boundedness
Authors: Kohlenbach Ulrich
Published: February 2016

In this paper the numerical strength of fragments of arithmetical
comprehension, choice and general uniform boundedness is studied systematically. These principles are investigated relative to base systems Tn^omega in all finite types which are suited to formalize substantial parts of analysis but nevertheless have provably recursive function(al)s of low growth. We reduce the use of instances of these principles in Tn^omega -proofs of a large class of formulas to the use of instances of certain arithmetical principles thereby determining faithfully the arithmetical
content of the former. This is achieved using the method of elimination of Skolem functions for monotone formulas which was introduced by the author in a previous paper.
As corollaries we obtain new conservation results for fragments of
analysis over fragments of arithmetic which strengthen known purely first-order conservation results.
Relational Reasoning about Contexts
Authors: Lassen Søren B.
Published: February 2016

The syntactic nature of operational reasoning requires techniques to deal with term contexts, especially for reasoning about recursion. In this paper we study applicative bisimulation and a variant of Sands’ improvement theory for a small call-by-value functional language. We explore an indirect, relational approach for reasoning about contexts. It is inspired by Howe’s precise method for proving congruence of simulation orderings and by Pitts’ extension thereof for proving applicative bisimulation up to context. We illustrate this approach with proofs of the unwinding theorem and syntactic continuity and, more importantly, we establish analogues of Sangiorgi’s bisimulation up to context for applicative bisimulation and for improvement. Using these powerful bisimulation up to context techniques, we give concise operational proofs of recursion induction, the improvement theorem, and syntactic minimal invariance. Previous operational proofs of these results involve complex, explicit reasoning about contexts.
Zero-Knowledge Proofs for Finite Field Arithmetic or: Can Zero-Knowledge be for Free?
Authors: Cramer Ronald , Damgård Ivan B.
Published: February 2016

We present zero-knowledge proofs and arguments for arithmetic circuits over finite prime fields, namely given a circuit, show in zero-knowledge that inputs can be selected leading to a given output. For a field GF(q), where q is an n-bit prime, a
circuit of size O(n), and error probability 2^−n, our protocols require communication of O(n^2) bits. This is the same worst-cast complexity as the trivial (non zero-knowledge)
interactive proof where the prover just reveals the input values. If the circuit involves n multiplications, the best previously known methods would in general require communication
of  Omega(n^3 log n) bits.
Variations of the technique behind these protocols lead to other interesting applications.
We first look at the Boolean Circuit Satisfiability problem and give zero-knowledge proofs and arguments for a circuit of size n and error probability 2^−n in which there is an interactive preprocessing phase requiring communication of O(n^2)
bits. In this phase, the statement to be proved later need not be known. Later the prover can non-interactively prove any circuit he wants, i.e. by sending only one message, of size O(n) bits.
As a second application, we show that Shamirs (Shens) interactive proof system for the (IP-complete) QBF problem can be transformed to a zero-knowledge proof
system with the same asymptotic communication complexity and number of rounds. The security of our protocols can be based on any one-way group homomorphism with a particular set of properties. We give examples of special assumptions sufficient for this, including: the RSA assumption, hardness of discrete log in a prime order group, and polynomial security of Die-Hellman encryption. We note that the constants involved in our asymptotic complexities are small enough for our protocols to be practical with realistic choices of parameters.
Model Checking via Reachability Testing for Timed Automata
Authors: Aceto Luca , Burgueno Augusto , Larsen Kim G.
Published: February 2016

In this paper we develop an approach to model-checking for timed automata via reachability testing. As our specification formalism, we consider a dense-time logic with clocks. This logic may be used to express safety and bounded liveness properties of real-time systems. We show how to automatically synthesize, for every logical formula phi, a so-called test automaton T_phi in such a way that checking whether a system S satisfies the property phi can be reduced to a reachability question over the system obtained by making T_phi interact with S.
The testable logic we consider is both of practical and theoretical interest. On the practical side, we have used the logic, and the associated approach to model-checking via reachability testing it supports, in the specification and verification in Uppaal of a collision avoidance protocol. On the theoretical side, we show that the logic is powerful enough to permit the definition of characteristic properties, with respect to a timed version of
the ready simulation preorder, for nodes of deterministic, tau-free timed automata. This allows one to compute behavioural relations via our model-checking technique, therefore effectively reducing the problem of checking the existence of a behavioural relation among states of a timed automaton to a reachability problem.
A Note on Frame Distributions
Authors: Kock Anders , Reyes Gonzalo E.
Published: February 2016

In the context of constructive locale or frame theory (locale
theory over a fixed base locale), we study some aspects of 'frame distributions', meaning sup preserving maps from a frame to the base frame. We derive a relationship between results of Jibladze-Johnstone and Bunge-Funk, and also descriptions in distribution terms, as well as in double negation terms, of the 'interior of closure' operator on open parts of a locale.
Relational Semantics of Non-Deterministic Dataflow
Authors: Hildebrandt Thomas Troels , Panangaden Prakash , Winskel Glynn
Published: February 2016

We recast dataflow in a modern categorical light using profunctors as a generalization of relations. The well known causal anomalies associated with relational semantics of indeterminate dataflow are avoided, but still we preserve
much of the intuitions of a relational model. The development fits with the view of categories of models for concurrency and the general treatment of bisimulation they provide. In particular it fits with the recent categorical formulation of feedback using traced monoidal categories. The payoffs are: (1) explicit relations to existing models and semantics, especially the
usual axioms of monotone IO automata are read off from the definition of profunctors, (2) a new definition of bisimulation for dataflow, the proof of the congruence of which benefits from the preservation properties associated with open maps and (3) a treatment of higher-order dataflow as a biproduct,
essentially by following the geometry of interaction programme.
On the No-Counterexample Interpretation
Authors: Kohlenbach Ulrich
Published: February 2016

In [15],[16] Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano
arithmetic. In particular he proved, using a complicated epsilon-substitution method (due to
W. Ackermann), that for every theorem A (A prenex) of first-order Peano arithmetic (PA) one can find ordinal recursive functionals Phi_A of order type < epsilon_0 which realize the
Herbrand normal form A^H of A.
 Subsequently more perspicuous proofs of this fact via functional interpretation (combined
with normalization) and cut-elimination were found. These proofs however do not carry out the n.c.i. as a local proof interpretation and don't respect the modus
ponens on the level of the n.c.i. of formulas A and A -> B. Closely related to this phenomenon is the fact that both proofs do not establish the condition (delta) and - at
least not constructively - (gamma) which are part of the definition of an `interpretation of a
formal system' as formulated in [15].
In this paper we determine the complexity of the n.c.i. of the modus ponens rule for
(i) PA-provable sentences,
(ii) for arbitrary sentences A;B in L(PA) uniformly in functionals satisfying the n.c.i. of (prenex normal forms of) A and A -> B; and
(iii) for arbitrary A;B in L(PA) pointwise in given alpha(< epsilon_0)-recursive functionals satisfying the n.c.i. of A and A -> B.
 This yields in particular perspicuous proofs of new uniform versions of the conditions ( gamma), (delta).
 Finally we discuss a variant of the concept of an interpretation presented in [17] and
show that it is incomparable with the concept studied in [15],[16]. In particular we show
that the n.c.i. of PA_n by alpha(= 1) is an interpretation in the sense of [17] but not in the sense of [15] since it violates the condition (delta).
On the Density of Normal Bases in Finite Fields
Authors: Frandsen Gudmund Skovbjerg
Published: February 2016

Let Fqn denote the finite field with q^n elements, for q being a prime power. Fqn may be regarded as an n-dimensional vector space over Fq. alpha in Fqn generates a normal basis for this vector space (Fqn : Fq), if
{alpha, alpha^q, alpha^q^2 , . . . , alpha^q^(n−1)} are linearly independent over Fq. Let N(q; n) denote the number of elements in Fqn that generate a normal basis for
Fqn : Fq, and let nu(q, n) = N(q,n)/q^n denote the frequency of such elements.
We show that there exists a constant c > 0 such that
nu(q, n) >= c / sqrt(log _q n) ,for all n, q >= 2
and this is optimal up to a constant factor in that we show
0.28477 <= lim inf (q, n) sqrt( log_q n ) <= 0.62521, for all q >= 2

We also obtain an explicit lower bound:
 nu(q, n) >= 1 / e [log_q n], for all n, q >= 2
Higher-Order Rewriting and Partial Evaluation
Authors: Danvy Olivier , Rose Kristoffer H.
Published: February 2016

We demonstrate the usefulness of higher-order rewriting techniques for specializing programs, i.e., for partial evaluation. More precisely, we demonstrate how casting program specializers as combinatory reduction systems (CRSs) makes it possible to formalize the corresponding program transformations as meta-reductions, i.e., reductions in the internal "substitution calculus." For partial-evaluation problems, this means that instead of having to prove on a case-by-case basis that one's "two-level functions" operate properly, one can concisely formalize them as a combinatory reduction system and obtain as a corollary that static reduction does not go wrong and yields a well-formed residual program.
We have found that the CRS substitution calculus provides an adequate expressive power to formalize partial evaluation: it provides sufficient termination strength while avoiding the need for additional restrictions such as types that would complicate the description unnecessarily (for our purpose). We also review the benefits and penalties entailed by more expressive higher-order formalisms. In addition, partial evaluation provides a number of examples of higher-order rewriting where being higher order is a central (rather than an occasional or merely exotic) property. We illustrate this by demonstrating how standard but non-trivial partial-evaluation examples are
handled with higher-order rewriting.
CoFI: The Common Framework Initiative for Algebraic Specification and Development
Authors: Mosses Peter D.
Published: February 2016

An open collaborative effort has been initiated: to design a
common framework for algebraic specification and development of software. The rationale behind this initiative is that the lack of such a common framework greatly hinders the dissemination and application of research
results in algebraic specification. In particular, the proliferation
of specification languages, some differing in only quite minor ways from each other, is a considerable obstacle for the use of algebraic methods in industrial contexts, making it difficult to exploit standard examples, case studies and training material. A common framework with widespread acceptance
throughout the research community is urgently needed.
The aim is to base the common framework as much as possible on a critical selection of features that have already been explored in various contexts. The common framework will provide a family of specification
languages at different levels: a central, reasonably expressive language, called CASL, for specifying (requirements, design, and architecture of) conventional software; restrictions of CASL to simpler languages, for use primarily in connection with prototyping and verification tools; and extensions
of CASL, oriented towards particular programming paradigms,
such as reactive systems and object-based systems. It should also be possible
to embed many existing algebraic specification languages in members of the CASL family. A tentative design for CASL has already been proposed. Task groups
are studying its formal semantics, tool support, methodology, and other aspects, in preparation for the finalization of the design.
Online Type-Directed Partial Evaluation
Authors: Danvy Olivier
Published: February 2016

In this experimental work, we extend type-directed partial evaluation (a.k.a. "reduction-free normalization" and "normalization by evaluation") to make it online, by enriching it with primitive operations (delta-rules). Each call to a primitive operator is either unfolded or residualized, depending on the operands and either with a default policy or with a user-supplied filter. The user can also specify how to residualize an operation, by pattern-matching over the operands. Operators may be pure or have a computational effect.
We report a complete implementation of online type-directed partial evaluation in Scheme, extending our earlier offline implementation.
Our partial evaluator is native in that it runs compiled code instead of using the usual meta-level technique of symbolic evaluation.
A Simple Solution to Type Specialization
Authors: Danvy Olivier
Published: February 2016

Partial evaluation specializes terms, but traditionally this
specialization does not apply to the type of these terms. As a result, specializing, e.g., an interpreter written in a typed language, which requires a "universal" type to encode expressible values, yields residual programs with type tags all over. Neil Jones has stated that getting rid of these type tags was an open problem, despite possible solutions such as Torben Mogensen's "constructor specialization." To solve this problem, John Hughes has proposed a new paradigm for partial evaluation, "Type Specialization," based on type inference instead of being based on symbolic interpretation. Type Specialization is very elegant in principle but it also appears non-trivial in practice. Stating the problem in terms of types instead of in terms of type encodings suggests a very simple type-directed solution, namely, to use a projection from the universal type to the specific type of the residual program. Standard partial evaluation then yields a residual program
without type tags, simply and efficiently.
Assessing the Overhead of ML Exceptions by Selective CPS Transformation
Authors: Kim Jung-taek , Yi Kwangkeun , Danvy Olivier
Published: February 2016

ML's exception handling makes it possible to describe exceptional execution flows conveniently, but it also forms a performance bottleneck. Our goal is to reduce this overhead by source-level transformation.
To this end, we transform source programs into continuation-passing style (CPS), replacing handle and raise expressions by continuation-catching and throwing expressions, respectively. CPS-transforming every expression, however, introduces a new cost. We therefore use an exception analysis to transform expressions selectively: if an expression is statically determined to involve exceptions then it is CPS-transformed; otherwise, it is left in direct style.
In this article, we formalize this selective CPS transformation, prove its correctness, and present early experimental data indicating its effect on ML programs.
Generating Hard Tautologies Using Predicate Logic and the Symmetric Group
Authors: Riis Søren , Sitharam Meera
Published: February 2016

We introduce methods to generate uniform families of hard propositional tautologies. The tautologies are essentially generated from a single propositional formula by a natural action of the symmetric group Sn.
The basic idea is that any Second Order Existential sentence Psi can be systematically translated into a conjunction phi of a finite collection of clauses such that the models of size n of an appropriate Skolemization Psi~   are in one-to-one correspondence with the satisfying assignments to phi_n: the Sn-closure of phi, under a natural action of the symmetric group Sn. Each phi_n is a CNF and thus has depth at most 2. The size of the phi_n's is bounded by a polynomial in n. Under the assumption NEXPTIME |= co- NEXPTIME, for any such sequence phi_n for which the spectrum S := {n : phi_n satisfiable} is NEXPTIME-complete, the tautologies not phi_(n not in S) do not have polynomial length proofs in any propositional proof system.
 Our translation method shows that most sequences of tautologies being studied in propositional proof complexity can be systematically generated from Second Order Existential sentences and moreover, many natural mathematical statements can be converted into sequences of propositional tautologies in this manner.
 We also discuss algebraic proof complexity issues for such sequences of tautologies. To this end, we show that any Second Order Existential sentence  Psi    can be systematically translated into a finite collection of polynomial equations Q = 0 such that the models of size n of an appropriate skolemization Psi~   are in one-to-one correspondence with the solutions to Qn = 0: the Sn-closure of Q = 0, under a natural action of the symmetric group Sn. The degree of Qn is the same as that of Q, and hence is independent of n, and the number of variables is no more than a polynomial in n. Furthermore, using results in [19] and [20], we briefly describe how, for the corresponding sequences of tautologies phi_n, the rich structure of the Sn closed, uniformly generated, algebraic systems Qn has profound consequences on the algebraic proof complexity of phi_n.
A Representation Result for Free Cocompletions
Authors: Power John , Cattani Gian Luca , Winskel Glynn
Published: February 2016

Given a class F of weights, one can consider the construction that
takes a small category C to the free cocompletion of C under weighted colimits, for which the weight lies in F. Provided these free Fcocompletions are small, this construction generates a 2-monad on Cat, or more generally on V-Cat for monoidal biclosed complete and cocomplete V. We develop the notion of a dense 2-monad on V-Cat and characterise free F-cocompletions by dense KZ-monads on V-Cat. We prove various corollaries about the structure of such 2-monads and their Kleisli 2-categories, as needed for the use of open maps in giving an axiomatic study of bisimulation in concurrency. This requires the introduction of the concept of a pseudo-commutativity for a strong 2-monad on a symmetric monoidal 2-category, and a characterisation of it in terms of structure on the Kleisli 2-category.
On Encoding p pi in m pi
Authors: Quaglia Paola , Walker David
Published: February 2016

This paper is about the encoding of p pi, the polyadic pi-calculus, in m pi, the monadic pi-calculus. A type system for m pi processes is introduced that captures the interaction regime underlying the encoding of p pi processes respecting a sorting. A full-abstraction result is shown: two p pi processes are typed barbed congruent iff their m pi encodings are monadic-typed barbed congruent.
Timed Bisimulation and Open Maps
Authors: Nielsen Mogens , Hune Thomas S.
Published: February 2016

Formal models for real-time systems have been studied intensively over the past decade. Much of the theory of untimed systems has been lifted to real-time settings. One example is the notion of bisimulation applied to timed transition systems, which is studied here within the general categorical framework of open maps. We define a category of timed transition systems, and show how to characterize standard timed bisimulation in terms of spans of open maps with a natural choice of a path category. This allows us to apply general results from the theory of open maps, e.g. the existence of canonical models and characteristic logics. Also, we obtain here an alternative proof of decidability of bisimulation for finite transition systems, and illustrate the use of open maps in finite presentations of bisimulations
A Compositional Proof System for the Modal mu-Calculus
Authors: Andersen Henrik Reif , Stirling Colin , Winskel Glynn
Published: February 2016

We present a proof system for determining satisfaction between
processes in a fairly general process algebra and assertions of the modal mu-calculus. The proof system is compositional in the structure of processes. It extends earlier work on compositional reasoning within the modal mu-calculus and combines it with techniques from work on local model checking. The proof system is sound for all processes and complete for a class of finite-state processes.
The Computational Strength of Extensions of Weak König’s Lemma
Authors: Kohlenbach Ulrich
Published: February 2016

The weak König's lemma WKL is of crucial significance in the study of fragments of mathematics which on the one hand are mathematically strong but on the other hand have a low proof-theoretic and computational strength. In addition to the restriction to binary trees (or equivalently bounded trees), WKL
is also `weak' in that the tree predicate is quantifier-free. Whereas in general the computational and proof-theoretic strength increases when logically more complex trees are allowed, we show that this is not the case for trees which are
given by formulas in a class Phi where we allow an arbitrary function quantifier prefix over bounded functions in front of a Pi^0_1-formula. This results in a schema Phi-WKL.
Another way of looking at WKL is via its equivalence to the principle
 For all x there exists y<=1 for all z A0(x; y; z) -> there exists f <= lambda x.1 for all x, z A0(x, fx, z);
where A0 is a quantifier-free formula (x, y, z are natural number variables).
 We generalize this to Phi-formulas as well and allow function quantifiers `there exists g <= s'
instead of `there exists y <= 1', where g <= s is defined pointwise. The resulting schema is called Phi-b-AC^0,1.
In the absence of functional parameters (so in particular in a second order context), the corresponding versions of Phi-WKL and Phi-b-AC^0,1 turn out to
be equivalent to WKL. This changes completely in the presence of functional
variables of type 2 where we get proper hierarchies of principles Phi_n-WKL and
Phi_n-b-AC^0,1. Variables of type 2 however are necessary for a direct representation
of analytical objects and - sometimes - for a faithful representation of
such objects at all as we will show in a subsequent paper. By a reduction of
Phi-WKL and Phi-b-AC^0,1 to a non-standard axiom F (introduced in a previous paper) and a new elimination result for F relative to various fragment of arithmetic in all finite types, we prove that Phi-WKL and Phi-b-AC^0,1 do
neither contribute to the provably recursive functionals of these fragments nor to their proof-theoretic strength. In a subsequent paper we will illustrate the greater mathematical strength of these principles (compared to WKL).
Real-Time Layered Video Compression using SIMD Computation
Authors: Jensen Morten Vadskær , Nielsen Brian
Published: February 2016

We present the design and implementation of a high performance layered video codec, designed for deployment in bandwidth heterogeneous networks. The codec combines wavelet based subband decomposition and discrete cosine transforms to facilitate layered spatial and SNR (signal-to-noise ratio) coding for bit-rate adaptation to a wide range of receiver capabilities. We show how a test video stream can be partitioned into several distinct layers of increasing visual quality and bandwidth requirements, with the difference between highest and lowest requirement being 47 : 1. Through the use of the Visual Instruction Set on SUN's Ultra-SPARC platform we demonstrate how SIMD parallel image processing enables real-time layered encoding and decoding in software. Our 384 * 320 * 24-bit test video stream is partitioned into 21 layers at a speed of 39 frames per second and reconstructed at 28 frames per second. Our VIS accelerated encoder stages are about 3-4 times as fast as an optimized C version. We find that this speed-up is well worth the extra implementation effort.
Fixpoint Alternation: Arithmetic, Transition Systems, and the Binary Tree
Authors: Bradfield Julian C.
Published: February 2016

We provide an elementary proof of the fixpoint alternation
hierarchy in arithmetic, which in turn allows us to simplify the proof of the modal mu-calculus alternation hierarchy. We further show that the alternation hierarchy on the binary tree is strict, resolving a problem of Niwinski.
Compilation and Equivalence of Imperative Objects (Revised Report)
Authors: Gordon Andrew D. , Hankin Paul D. , Lassen Søren B.
Published: February 2016

We adopt the untyped imperative object calculus of Abadi and
Cardelli as a minimal setting in which to study problems of compilation
and program equivalence that arise when compiling object oriented
languages. We present both a big-step and a small-step
substitution-based operational semantics for the calculus. Our first
two results are theorems asserting the equivalence of our substitution based semantics with a closure-based semantics like that given by Abadi and Cardelli. Our third result is a direct proof of the correctness of compilation to a stack-based abstract machine via a small-step decompilation algorithm. Our fourth result is that contextual equivalence of objects coincides with a form of Mason and Talcott's CIU
equivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in
our prototype compiler, for statically resolving method offsets. This is
the first study of correctness of an object-oriented abstract machine,
and of operational equivalence for the imperative object calculus.
Further Results on Partial Order Equivalences on Infinite Systems
Authors: Sunesen Kim
Published: February 2016

In [26], we investigated decidability issues for standard language equivalence for process description languages with two generalisations based on traditional approaches
for capturing non-interleaving behaviour: pomset equivalence reflecting global causal dependency, and location equivalence reflecting spatial distribution of events. In this paper, we continue by investigating the role played by TCSP-style renaming and hiding combinators with respect to decidability. One result of [26] was that in contrast to pomset equivalence, location equivalence remained decidable for a class of processes consisting of finite sets of BPP processes communicating in a TCSP manner. Here, we show that location equivalence becomes undecidable when either renaming or hiding is added to this class of processes. Furthermore, we investigate the weak versions of location and pomset equivalences.
We show that for BPP with prefixing, both weak pomset and weak location equivalence are decidable. Moreover, we show that weak location equivalence is undecidable for BPP semantically extended with CCS communication.
Encoding Types in ML-like Languages (Preliminary Version)
Authors: Yang Zhe
Published: February 2016

A Hindley-Milner type system such as ML's seems to prohibit typeindexed values, i.e., functions that map a family of types to a family of values. Such functions generally perform case analysis on the input types and return values of possibly different types. The goal of our work is to demonstrate how to program with type-indexed values within a Hindley-Milner type system.
Our first approach is to interpret an input type as its corresponding
value, recursively. This solution is type-safe, in the sense that the ML type system statically prevents any mismatch between the input type and function arguments that depend on this type.
Such specific type interpretations, however, prevent us from combining different type-indexed values that share the same type. To meet this objection, we focus on finding a value-independent type encoding that can be shared by different functions. We propose and compare two solutions. One requires first-class and higher-order polymorphism, and, thus, is not implementable in the core language of ML, but it
can be programmed using higher-order functors in Standard ML of New Jersey. Its usage, however, is clumsy. The other approach uses embedding/projection functions. It appears to be more practical. We demonstrate the usefulness of type-indexed values through examples including type-directed partial evaluation, C printf-like formatting, and subtype coercions. Finally, we discuss the tradeoffs between our approach and some other solutions based on more expressive typing disciplines.
An Improved Algorithm for RNA Secondary Structure Prediction
Authors: Lyngsø Rune B. , Zuker Michael , Pedersen Christian N. S.
Published: February 2016

Though not as abundant in known biological processes as proteins,
RNA molecules serve as more than mere intermediaries between
DNA and proteins, e.g. as catalytic molecules. Furthermore,
RNA secondary structure prediction based on free energy
rules for stacking and loop formation remains one of the few major
breakthroughs in the field of structure prediction. We present a
new method to evaluate all possible internal loops of size at most
k in an RNA sequence, s, in time O(k|s|^2); this is an improvement
from the previously used method that uses time O(k^2|s|^2).
For unlimited loop size this improves the overall complexity of
evaluating RNA secondary structures from O(|s|^4) to O(|s|^3) and
the method applies equally well to finding the optimal structure
and calculating the equilibrium partition function. We use our
method to examine the soundness of setting k = 30, a commonly
used heuristic.
Hereditary History Preserving Bisimilarity is Undecidable
Authors: Jurdzinski Marcin , Nielsen Mogens
Published: February 2016

We show undecidability of hereditary history preserving bisimilarity
for finite asynchronous transition systems by a reduction from the halting
problem of deterministic 2-counter machines. To make the proof more
transparent we introduce an intermediate problem of checking domino
bisimilarity for origin constrained tiling systems. First we reduce the
halting problem of deterministic 2-counter machines to origin constrained
domino bisimilarity. Then we show how to model domino bisimulations as
hereditary history preserving bisimulations for finite asynchronous transitions
systems. We also argue that the undecidability result holds for
finite 1-safe Petri nets, which can be seen as a proper subclass of finite
asynchronous transition systems.
An Error in the Mixed Adversary Protocol by Fitzi, Hirt and Maurer
Authors: Damgård Ivan B.
Published: February 2016

We point out an error in the protocol for mixed adversaries and
zero error from the Crypto 98 paper by Fitzi, Hirt and Maurer. We
show that the protocol only works under a stronger requirement on the
adversary than the one claimed. Hence the bound on the adversary's
corruption capability given there is not tight. Subsequent work has
shown, however, a new bound which is indeed tight.
An Extensional Characterization of Lambda-Lifting and Lambda-Dropping
Authors: Danvy Olivier
Published: February 2016

Lambda-lifting and lambda-dropping respectively transform a block-structured
functional program into recursive equations and vice versa.
Lambda-lifting was developed in the early 80's, whereas lambda-dropping
is more recent. Both are split into an analysis and a transformation.
Published work, however, has only concentrated on the analysis parts.
We focus here on the transformation parts and more precisely on their
correctness, which appears never to have been proven. To this end, we
define extensional versions of lambda-lifting and lambda-dropping and
establish their correctness with respect to a least fixed-point semantics.
A Complexity Gap for Tree-Resolution
Authors: Riis Søren
Published: February 2016

It is shown that any sequence  psi_n of tautologies which expresses the
validity of a fixed combinatorial principle either is "easy" i.e. has polynomial
size tree-resolution proofs or is "difficult" i.e requires exponential
size tree-resolution proofs. It is shown that the class of tautologies which
are hard (for tree-resolution) is identical to the class of tautologies which
are based on combinatorial principles which are violated for infinite sets.
Actually it is shown that the gap-phenomena is valid for tautologies based
on infinite mathematical theories (i.e. not just based on a single proposition).
We clarify the link between translating combinatorial principles (or
more general statements from predicate logic) and the recent idea of using
 the symmetrical group to generate problems of propositional logic.
Finally, we show that it is undecidable whether a sequence  psi_n (of the
kind we consider) has polynomial size tree-resolution proofs or requires
exponential size tree-resolution proofs. Also we show that the degree of
the polynomial in the polynomial size (in case it exists) is non-recursive,
but semi-decidable.

Keywords: Logical aspects of Complexity, Propositional proof complexity,
Resolution proofs.

 
Two Notes on the Computational Complexity of One-Dimensional Sandpiles
Authors: Miltersen Peter Bro
Published: February 2016

We prove that the one-dimensional sandpile prediction problem is
in AC1. The previously best known upper bound on the ACi-scale
was AC2. We also prove that it is not in AC1−epsilon for any constant
 epsilon > 0.
Foundational and Mathematical Uses of Higher Types
Authors: Kohlenbach Ulrich
Published: February 2016

In this paper we develop mathematically strong systems of analysis in
higher types which, nevertheless, are proof-theoretically weak, i.e. conservative
over elementary resp. primitive recursive arithmetic. These systems
are based on non-collapsing hierarchies (Phi_n-WKL+, Psi_n-WKL+) of principles
which generalize (and for n = 0 coincide with) the so-called `weak' K¨onig's
lemma WKL (which has been studied extensively in the context of second order
arithmetic) to logically more complex tree predicates. Whereas the second
order context used in the program of reverse mathematics requires an encoding
of higher analytical concepts like continuous functions F : X -> Y between
Polish spaces X, Y , the more flexible language of our systems allows to treat
such objects directly. This is of relevance as the encoding of F used in reverse
mathematics tacitly yields a constructively enriched notion of continuous functions
which e.g. for F : N^N -> N can be seen (in our higher order context) to be equivalent
 to the existence of a continuous modulus of pointwise continuity.
For the direct representation of F the existence of such a modulus is
independent even of full arithmetic in all finite types E-PA^omega plus quantifier-free
choice, as we show using a priority construction due to L. Harrington.
The usual WKL-based proofs of properties of F given in reverse mathematics
make use of the enrichment provided by codes of F, and WKL does not seem
to be sufficient to obtain similar results for the direct representation of F in
our setting. However, it turns out that   Psi_1-WKL+ is sufficient.
Our conservation results for (Phi_n-WKL+,  Psi_n-WKL+) are proved via a new
elimination result for a strong non-standard principle of uniform Sigma^0_1-
boundedness
which we introduced in 1996 and which implies the WKL-extensions studied
in this paper.
The Max-Plus Algebra of the Natural Numbers has no Finite Equational Basis
Authors: Aceto Luca , Ésik Zoltán , Ingólfsdóttir Anna
Published: February 2016

This paper shows that the collection of identities which hold in
the algebra N of the natural numbers with constant zero, and binary
operations of sum and maximum is not finitely based. Moreover, it
is proven that, for every n, the equations in at most n variables that
hold in N do not form an equational basis. As a stepping stone in
the proof of these facts, several results of independent interest are
obtained. In particular, explicit descriptions of the free algebras in the
variety generated by N are offered. Such descriptions are based upon
a geometric characterization of the equations that hold in N, which
also yields that the equational theory of N is decidable in exponential
time.
The Second Futamura Projection for Type-Directed Partial Evaluation
Authors: Grobauer Bernd , Yang Zhe
Published: February 2016

A generating extension of a program specializes it with respect to
some specified part of the input. A generating extension of a program
can be formed trivially by applying a partial evaluator to the program;
the second Futamura projection describes the automatic generation
of non-trivial generating extensions by applying a partial evaluator to
itself with respect to the programs.
We derive an ML implementation of the second Futamura projection
 for Type-Directed Partial Evaluation (TDPE). Due to the differences
 between `traditional', syntax-directed partial evaluation and
TDPE, this derivation involves several conceptual and technical steps.
These include a suitable formulation of the second Futamura projection
 and techniques for making TDPE amenable to self-application. In
the context of the second Futamura projection, we also compare and
relate TDPE with conventional offline partial evaluation.
We demonstrate our technique with several examples, including
compiler generation for Tiny, a prototypical imperative language.
Decoding Choice Encodings
Authors: Nestmann Uwe , Pierce Benjamin C.
Published: February 2016

We study two encodings of the asynchronous pi-calculus with input-guarded choice into its choice-free fragment. One encoding is divergence-free, but refines the atomic commitment of choice into gradual commitment. The other preserves atomicity, but introduces divergence. The divergent encoding is fully abstract with respect to weak bisimulation, but the more natural divergence-free encoding is not. Instead, we show that it is fully abstract with respect to coupled simulation, a slightly coarser - but still coinductively defined - equivalence that does not enforce bisimilarity of internal branching decisions. The correctness proofs for the two choice encodings introduce a novel proof technique exploiting the properties of explicit decodings from translations to source terms.
Aliasing Models for Mobile Objects
Authors: Nestmann Uwe , Hüttel Hans , Kleist Josva , Merro Massimo
Published: February 2016

In Obliq, a lexically scoped, distributed, object-oriented programming language, object migration was suggested as the creation of a copy of an object's state at the target site, followed by turning the object itself into an alias, also called surrogate, for the remote copy. We consider the creation of object surrogates as an abstraction of the above-mentioned style of migration. We introduce Øjeblik, a typed distribution-free subset of Obliq, and provide four different configuration-style semantics, which only differ in the respective aliasing model. We show that two of the semantics, one of which matches Obliq's implementation, render migration unsafe, while our new proposal allows for safe migration at least for a large class of program contexts. In addition, we propose a type system that allows a programmer to statically guarantee that programs belong to that class. Our work suggests a straightforward repair of Obliq's aliasing model.
Formalizing Implementation Strategies for First-Class Continuations
Authors: Danvy Olivier
Published: February 2016

We present the first formalization of implementation strategies
 for first-class continuations. The formalization hinges on abstract
machines for continuation-passing style (CPS) programs with a special
treatment for the current continuation, accounting for the essence of
first-class continuations. These abstract machines are proven equivalent
to a standard, substitution-based abstract machine. The proof techniques
work uniformly for various representations of continuations. As a byproduct
, we also present a formal proof of the two folklore theorems that one
continuation identifier is enough for second-class continuations and that
second-class continuations are stackable.
A large body of work exists on implementing continuations, but it is
predominantly empirical and implementation-oriented. In contrast, our
formalization abstracts the essence of first-class continuations and provides
a uniform setting for specifying and formalizing their representation.
Pseudoknots in RNA Secondary Structures
Authors: Lyngsø Rune B. , Pedersen Christian N. S.
Published: February 2016

RNA molecules are sequences of nucleotides that serve as more than mere intermediaries between DNA and proteins, e.g. as catalytic molecules. Computational prediction of RNA secondary structure is among the few structure prediction problems that can be solved satisfactorily in polynomial time. Most work has been done to predict structures that do not contain pseudoknots. Allowing pseudoknots introduce modelling and computational problems. In this paper we consider the problem of predicting RNA secondary structure when certain types of pseudoknots are allowed. We first present an algorithm that in time O(n^5) and space O(n^3) predicts the secondary structure of an RNA sequence of length n in a model that allows certain kinds of pseudoknots. We then prove that the general problem of predicting RNA secondary structure containing pseudoknots is NP-complete for a large class of reasonable models of pseudoknots.
Matching Modulo Associativity and Idempotency is NP-Complete
Authors: Klima Ondrej , Srba Jirí
Published: February 2016

We show that AI-matching (AI denotes the theory of an
associative and idempotent function symbol), which is solving matching
word equations in free idempotent semigroups, is NP-complete.
Note: this is a full version of the paper [9] and a revision of [8].
Multiparty Computation from Threshold Homomorphic Encryption
Authors: Cramer Ronald , Damgård Ivan B. , Nielsen Jesper Buus
Published: February 2016

We introduce a new approach to multiparty computation (MPC) basing
it on homomorphic threshold crypto-systems. We show that given
keys for any sufficiently efficient system of this type, general MPC protocols
for n players can be devised which are secure against an active
adversary that corrupts any minority of the players. The total number of
bits sent is O(nk|C|), where k is the security parameter and |C| is the size
of a (Boolean) circuit computing the function to be securely evaluated.
An earlier proposal by Franklin and Haber with the same complexity was
only secure for passive adversaries, while all earlier protocols with active
security had complexity at least quadratic in n. We give two examples
of threshold cryptosystems that can support our construction and lead
to the claimed complexities.
Syntactic Accidents in Program Analysis: On the Impact of the CPS Transformation
Authors: Damian Daniel , Danvy Olivier
Published: February 2016

We show that a non-duplicating CPS transformation has no effect on control-flow analysis and that it has a positive effect on binding-time analysis: a monovariant control-flow analysis yields equivalent results on a direct-style program
and on its CPS counterpart, and a monovariant binding-time analysis yields more precise results on a CPS program than on its direct-style counterpart. Our proof technique amounts to constructing the continuation-passing style (CPS) counterpart of flow information and of binding times.
Our results confirm a folklore theorem about binding-time analysis, namely
that CPS has a positive effect on binding times. What may be more surprising is that this benefit holds even if contexts or continuations are not duplicated. The present study is symptomatic of an unsettling property of program analyses: their quality is unpredictably vulnerable to syntactic accidents in source programs, i.e., to the way these programs are written. More reliable program analyses require a better understanding of the effect of syntactic change.
Complexity of Weak Bisimilarity and Regularity for BPA and BPP
Authors: Srba Jirí
Published: February 2016

It is an open problem whether weak bisimilarity is decidable
for Basic Process Algebra (BPA) and Basic Parallel Processes (BPP). A
PSPACE lower bound for BPA and NP lower bound for BPP have been
demonstrated by Stribrna. Mayr achieved recently a result, saying that
weak bisimilarity for BPP is Pi^P_2-hard. We improve this lower bound to
PSPACE, moreover for the restricted class of normed BPP.
Weak regularity (finiteness) of BPA and BPP is not known to be decidable
either. In the case of BPP there is a Pi^P_2-hardness result by Mayr,
which we improve to PSPACE. No lower bound has previously been established
for BPA. We demonstrate DP-hardness, which in particular
implies both NP and co-NP-hardness.
In each of the bisimulation/regularity problems we consider also the
classes of normed processes.
Heuristics for Hierarchical Partitioning with Application to Model Checking
Authors: Möller M. Oliver , Alur Rajeev
Published: February 2016

Given a collection of connected components, it is often desired to cluster together
parts of strong correspondence, yielding a hierarchical structure. We address the
automation of this process and apply heuristics to battle the combinatorial and
computational complexity.
We define a cost function that captures the quality of a structure relative to the
connections and favors shallow structures with a low degree of branching. Finding
a structure with minimal cost is shown to be NP-complete. We present a greedy
polynomial-time algorithm that creates an approximate good solution incrementally
by local evaluation of a heuristic function. We compare some simple heuristic
functions and argue for one based on four criteria: The number of enclosed connections,
the number of components, the number of touched connections and the depth of the structure.
We report on an application in the context of formal verication, where our
algorithm serves as a preprocessor for a temporal scaling technique, called \"ext" heuristic
 [AW99]. The latter is applicable in enumerative reachability analysis and is included
in the recent version of the Mocha model checking tool.
We demonstrate performance and benefits of our method and use an asynchronous
parity computer, a standard leader election algorithm, and an opinion poll protocol as
case studies.