Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, d...
详细信息
ISBN:
(纸本)9781450328869
Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, decide whether there exists a first-order definable separator. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation. This yields an EXPTIME algorithm for checking first-order separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. Finally, we prove that this technique can be generalized to answer the same question for regular languages of infinite words.
We employ the well-developed and powerful techniques of algebraic semantics and Priestley duality to set up a Kripke semantics for a modal expansion of Arieli and Avron's bilattice logic, itself based on Belnap...
详细信息
ISBN:
(纸本)9781479904136
We employ the well-developed and powerful techniques of algebraic semantics and Priestley duality to set up a Kripke semantics for a modal expansion of Arieli and Avron's bilattice logic, itself based on Belnap's four-valued logic. We obtain soundness and completeness of a Hilbert-style derivation system for this logic with respect to four-valued Kripke frames, the standard notion of model in this setting. The proof is via intermediary relational structures which are analysed through a topological reading of one of the axioms of the logic. Both local and global consequence on the models are covered.
Martin-Lof's type theory has strong existential elimination (dependent sum type) that allows to prove the full axiom of choice. However the theory is intuitionistic. We give a condition on strong existential elimi...
详细信息
ISBN:
(纸本)9780769547695
Martin-Lof's type theory has strong existential elimination (dependent sum type) that allows to prove the full axiom of choice. However the theory is intuitionistic. We give a condition on strong existential elimination that makes it computationally compatible with classical logic. With this restriction, we lose the full axiom of choice but, thanks to a lazily-evaluated coinductive representation of quantification, we are still able to constructively prove the axiom of countable choice, the axiom of dependent choice, and a form of bar induction in ways that make each of them computationally compatible with classical logic.
We graft synchronization onto Girard's Geometry of Interaction in its most concrete form, namely token machines. This is realized by introducing proof-nets for SMLL, an extension of multiplicative linear logic wit...
详细信息
ISBN:
(纸本)9781450328869
We graft synchronization onto Girard's Geometry of Interaction in its most concrete form, namely token machines. This is realized by introducing proof-nets for SMLL, an extension of multiplicative linear logic with a specific construct modeling synchronization points, and of a multi-token abstract machine model for it. Interestingly, the correctness criterion ensures the absence of deadlocks along reduction and in the underlying machine, this way linking logical and operational properties.
It is shown that order-invariance of two-variable first-logic is decidable in the finite. This is an immediate consequence of a decision procedure obtained for the finite satisfiability problem for existential second-...
详细信息
ISBN:
(纸本)9781450343916
It is shown that order-invariance of two-variable first-logic is decidable in the finite. This is an immediate consequence of a decision procedure obtained for the finite satisfiability problem for existential second-order logic with two first-order variables (ESO2) structures with two linear orders and one induced successor. We also show that finite satisfiability is decidable on structures with two successors and one induced linear order. In both cases, so far only decidability for monadic ESO2 has been known. In addition, the finite satisfiability problem for ESO2 on structures with one linear order and its induced successor relation is shown to be decidable in non-deterministic exponential time.
Graph neural networks (GNNs) are deep learning architectures for machine learning problems on graphs. It has recently been shown that the expressiveness of GNNs can be characterised precisely by the combinatorial Weis...
详细信息
ISBN:
(纸本)9781665448956
Graph neural networks (GNNs) are deep learning architectures for machine learning problems on graphs. It has recently been shown that the expressiveness of GNNs can be characterised precisely by the combinatorial Weisfeiler-Leman algorithms and by finite variable counting logics. The correspondence has even led to new, higher-order GNNs corresponding to the WL algorithm in higher dimensions. The purpose of this paper is to explain these descriptive characterisations of GNNs.
I chart a line of development from category-theoretic models of programs and logics to automatic program verification/analysis techniques that are in deployment at Facebook. Our journey takes in a number of concepts f...
详细信息
ISBN:
(纸本)9781479988754
I chart a line of development from category-theoretic models of programs and logics to automatic program verification/analysis techniques that are in deployment at Facebook. Our journey takes in a number of concepts from the computersciencelogician's toolkit - including categorical logic and model theory, denotational semantics, the Curry-Howard isomorphism, substructural logic, Hoare logic and Separation logic, abstract interpretation, compositional program analysis, the frame problem, and abductive inference.
We study tree-to-tree transformations that can be defined in first-order logic or monadic second-order logic. We prove a decomposition theorem, which shows that every transformation can be obtained from prime transfor...
详细信息
ISBN:
(纸本)9781450371049
We study tree-to-tree transformations that can be defined in first-order logic or monadic second-order logic. We prove a decomposition theorem, which shows that every transformation can be obtained from prime transformations, such as tree-to-tree homomorphisms or pre-order traversal, by using combinators such as function composition.
Negation is not involutive in the lambda C calculus because it does not distinguish captured stacks from continuations. We show that there is a formulae-as-types correspondence between the involutive negation in proof...
详细信息
ISBN:
(纸本)9781450328869
Negation is not involutive in the lambda C calculus because it does not distinguish captured stacks from continuations. We show that there is a formulae-as-types correspondence between the involutive negation in proof theory, and a notion of high-level access to the stacks studied by Felleisen and Clements. We introduce polarised, untyped, calculi compatible with extensionality, for both of classical sequent calculus and classical natural deduction, with connectives for an involutive negation. The involution is due to the l delimited control operator that we introduce, which allows us to implement the idea that captured stacks, unlike continuations, can be inspected. Delimiting control also gives a constructive interpretation to falsity. We describe the isomorphism there is between A and inverted left perpendicular inverted left perpendicularA, and thus between inverted left perpendicular boolean OR and there exists inverted left perpendicular.
Functional Reactive Programming (FRP) is an approach to streaming data with a pure functional semantics as time-indexed values. In previous work, we showed that Linear-time Temporal logic (LTL) can be used as a type s...
详细信息
ISBN:
(纸本)9781450328869
Functional Reactive Programming (FRP) is an approach to streaming data with a pure functional semantics as time-indexed values. In previous work, we showed that Linear-time Temporal logic (LTL) can be used as a type system for discrete-time FRP, and that functional reactive primitives perform two roles: as combinators for building streams of data, and as proof rules for constructive LTL. In this paper, we add a third role, by showing that FRP combinators can be used to define streams of types, and that these functional reactive types can be viewed both as a constructive temporal logic, and as the types for functional reactive programs. As an application of functional reactive types, we show that past-time LTL (pLTL) can be extended with FRP to get a logic pLTL+FRP. This logic is expressed as streams of boolean expressions, and so bounded satisfiability of pLTL can be translated to Satisfiability Modulo Theory (SMT). Thus, pLTL+FRP can be used as a constraint language for problems which mix properties of data with temporal properties.
暂无评论