Quantitative aspects of linear and affine closed lambda terms
We introduce versions of game-theoretic semantics (GTS) for Alternating-Time Temporal Logic (ATL). In GTS, truth is defined in terms of existence of a winning strategy in a semantic evaluation game, and thus the game-theoretic perspective appears in the framework of ATL on two semantic levels: on the object level in the standard semantics of the strategic operators, and on the meta-level where game-theoretic logical semantics is applied to ATL. We unify these two perspectives into semantic evaluation games specially designed for ATL. The game-theoretic perspective enables us to identify new variants of the semantics of ATL based on limiting the time resources available to the verifier and falsifier in the semantic evaluation game. We introduce and analyse an unbounded and (ordinal) bounded GTS and prove these to be equivalent to the standard (Tarski-style) compositional semantics. We show that in these both versions of GTS, truth of ATL formulae can always be determined in finite time, i.e., without constructing infinite paths. We also introduce a non-equivalent finitely bounded semantics and argue that it is natural from both logical and game-theoretic perspectives.
We present a novel general technique that uses classifier learning to synthesize piece-wise functions (functions that split the domain into regions and apply simpler functions to each region) against logical synthesis specifications. Our framework works by combining a synthesizer of functions for fixed concrete inputs and a synthesizer of predicates that can be used to define regions. We develop a theory of single-point refutable specifications that facilitate generating concrete counterexamples using constraint solvers. We implement the framework for synthesizing piece-wise functions in linear integer arithmetic, combining leaf expression synthesis using constraint-solving with predicate synthesis using enumeration, and tie them together using a decision tree classifier. We demonstrate that this compositional approach is competitive compared to existing synthesis engines on a set of synthesis specifications.
Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that manipulate resources such as memory locations. These logics are abstract because they are independent of any particular concrete resource model. Their assertion languages, called propositional abstract separation logics (PASLs), extend the logic of (Boolean) Bunched Implications (BBI) in various ways. This added expressivity comes at a price since the resulting logics are all undecidable. Given their wide applicability, even a semi-decision procedure for these logics is desirable. Although several PASLs are discussed in the literature, the proof theory and automated reasoning for these logics were open problems solved by the conference version of this paper, which developed a modular proof theory for various PASLs using cut-free labelled sequent calculi. This paper non-trivially improves upon this previous work by giving a general framework of calculi on which any new axiom in the logic satisfying a certain form corresponds to an inference rule in our framework, and the completeness proof is generalised to consider such axioms. Our base calculus handles Calcagno et al.s original logic of separation algebras by adding rules for partial-determinism and cancellativity, while preserving cut-elimination. We then show that many important properties in separation logic, such as indivisible-unit, disjointness, splittability, and cross-split, can be expressed in our general axiom form. Thus our framework offers inference rules and completeness for these properties for free. Finally, we show how our calculi reduce to calculi with global label substitutions, enabling more efficient implementation.
We introduce three formal models of distributed systems for query evaluation on massive databases: Distributed Streaming with Register Automata (DSAs), Distributed Streaming with Register Transducers (DSTs), and Distributed Streaming with Register Transducers and Joins (DSTJs). These models are based on the map-reduce paradigm where the input is transformed into a dataset of key-value pairs, and on each key a local computation is performed on the values associated with that key resulting in another set of key-value pairs. Computation proceeds in a constant number of rounds, where the result of the last round is the input to the next round, and transformation of key-value pairs is required to be generic. The difference between the three models is in the local computation part. In DSAs it is limited to making one pass over its input using a register automaton, while in DSTs it can make two passes: in the first pass it uses a finite-state automaton and in the second it uses a register transducer. The third model DSTJs is an extension of DSTs, where local computations are capable of constructing the Cartesian product of two sets. We obtain the following results: (1)DSAs can evaluate first-order queries over bounded degree databases; (2)DSTs can evaluate semijoin algebra queries over arbitrary databases; (3)DSTJs can evaluate the whole relational algebra over arbitrary databases; (4)DSTJs are strictly stronger than DSTs, which in turn, are strictly stronger than DSAs; (5)within DSAs, DSTs and DSTJs there is a strict hierarchy w.r.t. the number of rounds.
Recent methods have adapted the AGM and belief base frameworks for belief change to cover belief revision in logic programs. In this study here, we present two new sets of belief change operators for logic programs. They focus on preserving the explicit relationships expressed in the rules of a program, a feature that is missing in purely semantic approaches that consider programs only in their entirety. In particular, operators of the latter class fail to satisfy preservation and support, two important properties to ensure intuitive results. We address this shortcoming of existing approaches by introducing partial meet and ensconcement constructions for logic program belief change, which allow us to define syntax-preserving operators that satisfy preservation and support. Our work is novel in that our constructions not only preserve more information from a logic program during a change operation than existing ones, but they also facilitate natural definitions of contraction operators, the first in the field to the best of our knowledge. To evaluate the rationality of our operators, we translate the revision and contraction postulates from the AGM and belief base frameworks to the logic programming setting. We show that our operators fully comply with the belief base framework and formally state the interdefinability between our operators. We further propose a module-based algorithm to optimise partial meet and ensconcement revisions or contractions. Finally, we compare our approach to two state-of-the-art logic program revision methods and demonstrate that our operators address the shortcomings of one and generalise the other method.
We study the expressive power of fragments of inclusion logic under the so-called lax team semantics. The fragments are defined either by restricting the number of universal quantifiers, the number of inclusion atoms, or the arity of inclusion atoms. We show that the whole expressive power of inclusion logic can be captured using only five inclusion atoms in finite ordered models, or alternatively only one universal quantifier in general. The arity hierarchy is shown to be strict by relating the question to the study of arity hierarchies in fixed point logics.
Connections between homotopy theory and type theory have recently attracted a lot of attention, with Voevodsky's univalent foundations and the interpretation of Martin-L\"of's identity types in Quillen model categories as some of the highlights. In this paper we establish a connection between a natural weakening of Martin-L\"of's rules for the identity types which has been considered by Cohen, Coquand, Huber and M\"ortberg in their work on a constructive interpretation of the univalence axiom on the one hand, and the notion of a path category, a slight variation on the classic notion of a category of fibrant objects due to Brown, on the other. This involves showing that the syntactic category associated to a type theory with weak identity types carries the structure of a path category, strengthening earlier results by Avigad, Lumsdaine and Kapulkin. In this way we not only relate a well-known concept in homotopy theory with a natural concept in logic, but also provide a framework for further developments.