this paper resolves two open problems on linear integer arithmetic (LIA), also known as Presburger arithmetic. First, we give a triply exponential geometric decision procedure for LIA, i.e., a procedure based on manip...
详细信息
Semiring semantics evaluates logical statements by values in some commutative semiring (K, +, •, 0, 1). Random semiring interpretations, induced by a probability distribution on K, generalise random structures, and we...
详细信息
Polynomial closure is a standard operator which is applied to a class of regular languages. In this paper, we investigate three restrictions called left (LPol), right (RPol) and mixed polynomial closure (MPol). the fr...
详细信息
Automatic structures are infnite structures that are fnitely represented by synchronized fnite-state automata. this paper concerns specifcally automatic structures over fnite words and trees (ranked/unranked). We inve...
详细信息
It is a longstanding open problem whether there is an algorithm to decide the Skolem Problem for linear recurrence sequences (LRS) over the integers, namely whether a given such sequence un n8=0 has a zero term (i.e.,...
详细信息
the framework of quantitative equational logic has been successfully applied to reason about algebras whose carriers are metric spaces and operations are nonexpansive. We extend this framework in two orthogonal direct...
详细信息
ISBN:
(纸本)9781450393515
the framework of quantitative equational logic has been successfully applied to reason about algebras whose carriers are metric spaces and operations are nonexpansive. We extend this framework in two orthogonal directions: algebras endowed with generalised metric space structures, and operations being nonexpansive up to a lifting. We apply our results to the algebraic axiomatisation of the Łukaszyk–Karmowski distance on probability distributions, which has recently found application in the field of representation learning on Markov processes.
the λμ-calculus plays a central role in the theory of programming languages as it extends the Curry-Howard correspondence to classical logic. A major drawback is that it does not satisfy Böhm’s theorem and it ...
详细信息
ISBN:
(纸本)9781450393515
the λμ-calculus plays a central role in the theory of programming languages as it extends the Curry-Howard correspondence to classical logic. A major drawback is that it does not satisfy Böhm’s theorem and it lacks the corresponding notion of approximation. On the contrary, we show that Ehrhard and Regnier’s Taylor expansion can be easily adapted, thus providing a resource conscious approximation theory. this produces a sensible λμ-theory with which we prove some advanced properties of the λμ-calculus, such as Stability and Perpendicular Lines Property, from which the impossibility of parallel computations follows.
In quantitative reasoning one compares objects by distances, instead of equivalence relations, so that one can measure how much they are similar, rather than just saying whether they are equivalent or not. In this pap...
详细信息
ISBN:
(纸本)9781450393515
In quantitative reasoning one compares objects by distances, instead of equivalence relations, so that one can measure how much they are similar, rather than just saying whether they are equivalent or not. In this paper we aim at providing a logical ground to quantitative reasoning with distances in Linear logic, using the categorical language of Lawvere’s doctrines. the key idea is to see distances as equality predicates in Linear logic. We use graded modalities to write a resource sensitive substitution rule for equality, which allows us to give it a quantitative meaning by distances. We introduce a deductive calculus for (Graded) Linear logic with quantitative equality and the notion of Lipschitz doctrine to give it a sound and complete categorical semantics. We also describe a universal construction of Lipschitz doctrines, which generates examples based for instance on metric spaces and quantitative realisability.
暂无评论