Search

We present initial limit Datalog, a new extensible class of constrained Horn clauses for which the satisfiability problem is decidable. The class may be viewed as a generalisation to higher-order logic (with a simple restriction on types) of the first-order language limit Datalog$_Z$ (a fragment of Datalog modulo linear integer arithmetic), but can be instantiated with any suitable background theory. For example, the fragment is decidable over any countable well-quasi-order with a decidable first-order theory, such as natural number vectors under componentwise linear arithmetic, and words of a bounded, context-free language ordered by the subword relation. Formulas of initial limit Datalog have the property that, under some assumptions on the background theory, their satisfiability can be witnessed by a new kind of term model which we call entwined structures. Whilst the set of all models is typically uncountable, the set of all entwined structures is recursively enumerable, and model checking is decidable., Comment: 18 pages. To be published in LICS 2021

We present a simple resolution proof system for higher-order constrained Horn clauses (HoCHC)-a system of higher-order logic modulo theories-and prove its soundness and refutational completeness w.r.t. both standard and Henkin semantics. As corollaries, we obtain the compactness theorem and semi-decidability of HoCHC for semi-decidable background theories, and we prove that HoCHC satisfies a canonical model property. Moreover a variant of the well-known translation from higher-order to 1st-order logic is shown to be sound and complete for HoCHC in both semantics. We illustrate how to transfer decidability results for (fragments of) 1st-order logic modulo theories to our higher-order setting, using as example the Bernays-Schonflukel-Ramsey fragment of HoCHC modulo a restricted form of Linear Integer Arithmetic.

Motivated by a tight connection between Joyal's combinatorial species and quantitative models of linear logic, this paper introduces weighted generalised species (or weighted profunctors), where weights are morphisms of a given symmetric monoidal closed category (SMCC). For each SMCC W, we show that the category of W-weighted profunctors is a Lafont category, a categorical model of linear logic with exponential. As a model of programming languages, the construction of this paper gives a unified framework that induces adequate models of nondeterministic, probabilistic, algebraic and quantum programming languages by an appropriate choice of the weight SMCC.

Automata, logic and games provide the mathematical theory that underpins the model checking of reactive systems.

The model checking of higher-order recursion schemes has important applications in the verification of higher-order programs. Ong has previously shown that the modal mu-calculus model checking of trees generated by ordern recursion scheme is n-EXPTIME complete, but his algorithm and its correctness proof were rather complex. We give an alternative, type-based verification method: Given a modal mucalculus formula, we can construct a type system in which a recursion scheme is typable if, and only if, the (possibly infinite, ranked) tree generated by the scheme satisfies the formula. The model checking problem is thus reduced to a type checking problem. Our type-based approach yields a simple verification algorithm, and its correctness proof (constructed without recourse to game semantics) is comparatively easy to understand. Furthermore, the algorithm is polynomial-time in the size of the recursion scheme, assuming that the formula and the largest order and arity of non-terminals of the recursion scheme are fixed. © 2009 IEEE.

Harmer and McCusker have developed a fully abstract game model for nondeterministic Idealised Algol and, at the same time, revealed difficulties in constructing game models for stateless nondeterministic languages and infinite nondeterminism. We propose a novel approach in which a strategy is not a set, but a tree, of plays, and develop a fully abstract game model for a nondeterministic stateless language. Mathematically such a strategy is formalised as a sheaf over an appropriate site of plays. We conclude with a study on the difficulties pointed out by Harmer and McCusker in terms of the structure of the coverage of the sites.

We consider the following decision problems:ProofNet: Is a given multiplicative linear logic (MLL) proof structure a proof net?EssNet: Is a given essential net (of an intuitionistic MLL sequent) correct?In this article we show how to obtain linear-time algorithms for EssNet. As a corollary, by showing that ProofNet is linear-time reducible to EssNet (by the Trip Translation), we obtain a linear-time algorithm for ProofNet.We show further that it is possible to optimize the verification so that each node of the input structure is visited at most once. Finally, we present linear-time algorithms for sequentializing proof nets and essential nets, that is, for finding derivations of the underlying sequents.

We present a game model of the untyped λ-calculus, with equational theory equal to the Böhm tree λ-theory B, which is universal (i.e. every element of the model is definable by some term). This answers a question of Di Gianantonio, Franco and Honsell. We build on our earlier work, which uses the methods of innocent game semantics to develop a universal model inducing the maximal consistent sensible theory H∗. To our knowledge these are the first syntax-independent universal models of the untyped λ-calculus.

We present a new denotational model for the untyped l-calculus, using the techniques of game semantics. The strategies used are innocent in the sense of Hyland and Ong (Inform. and Comput., to appear) and Nickau (Hereditarily Sequential Functionals: A Game-Theoretic Approach to Sequentiality, Shaker-Verlag, 1996. Dissertation, Universitat Gesamthochschule Siegen, Shaker-Verlag, 1996), but the traditional distinction between "question" and "answer" moves is removed. We first construct models D and DREC as global sections of a reflexive object in the categories A and AREC of arenas and innocent and recursive innocent strategies, respectively. We show that these are sensible le-algebras but are neither extensional nor universal. We then introduce a new representation of innocent strategies in an economical form. We show a strong connexion between the economical form of the denotation of a term in the game models and a variable-free form of the Nakajima tree of the term. Using this we show that the definable elements of DREC are precisely what we call effectively almost-everywhere copycat (EAC) strategies. The category AEAC with these strategies as morphisms gives rise to a λη-model DEAC which we show has the same expressive power as D, i.e. the equational theory of DEAC is the maximal consistent sensible theory H*. We show that the model DEAC is sensible, order-extensional and universal (i.e. every strategy is the denotation of some λ-term). To our knowledge this is the first syntax-free model of the untyped λ-calculus with the universality property. Copyright 2002 Elsevier Science B.V.

Higher-order model checking is the problem of model checking (possibly) infinite trees generated by higher-order recursion schemes (HORS). HORS are a natural abstract model of functional programs, and HORS model checkers play a similar role to checkers of Boolean programs in the imperative setting. Most research effort so far has focused on checking safety properties specified using trivial tree automata i.e. Buechi tree automata all of whose states are final. Building on our previous work, we present a higher-order model checker, TravMC2, which supports properties specified using alternating parity tree automata (or equivalently monadic second order logic). Our experimental results offer an encouraging comparison with an existing checker, TrecS-APT.

We introduce type-checking games, which are ω-regular games over Bohm trees, determined by a type of the Kobayashi-Ong intersection type system. These games are a higher-type extension of parity games over trees, determined by an alternating parity tree automaton. However, in contrast to these games over trees, the "game boards" of our type-checking games are composable, using the composition of Bohm trees. Moreover the winner (and winning strategies) of a composite game is completely determined by the respective winners (and winning strategies) of the component games. To our knowledge, type-checking games give the first compositional analysis of higher-order model checking, or the model checking of trees generated by recursion schemes. We study a higher-type analogue of higher-order model checking, namely, the problem to decide the winner of a type-checking game over the Bohm tree generated by an arbitrary λY-term. We introduce a new type-assignment system and use it to prove that the problem is decidable. On the semantic side, we develop a novel (two-level) arena game model for type-checking games, which is a cartesian closed category equipped with parametric monad and comonad that themselves form a parametrised adjunction.

This paper is about two models of computation that underpin recent developments in the algorithmic verification of higher-order computation. Recursion schemes are in essence the simply-typed lambda calculus with recursion, generated from first-order symbols. Collapsible pushdown automata are a generalisation of pushdown automata to higher-order stacks — which are iterations of stack of stacks — that contain symbols equipped with links. We study and compare the expressive power of the two models and the algorithmic properties of infinite structures such as trees and graphs generated by them. We conclude with a brief overview of recent applications to the model checking of higher-order functional programs. A central theme of the work is the fruitful interplay of ideas between the neighbouring fields of semantics and algorithmic verification.

The simply-typed, call-by-value language, RML, may be viewed as a canonical restriction of Standard ML to ground-type references, augmented by a "bad variable" construct in the sense of Reynolds. By a short type, we mean a type of order at most 2 and arity at most 1. We consider the O-strict fragment of (finitary) RML, RMLO-Str, consisting of terms-in-context x1 : θ1, ..., xn : θn ⊢ M : θ such that θ is short, and every argument type of every θi is short. RMLO-Str is surprisingly expressive; it includes several instances of (in)equivalence in the literature that are challenging to prove using methods based on (state-based) logical relations. We show that it is decidable whether a given pair of RMLO-Str terms-in-context is observationally equivalent. Using the fully abstract game semantics of RML, our algorithm reduces the problem to the language equivalence of visibly pushdown automata. When restricted to terms in canonical form, the problem is EXPTIME-complete.

Higher-order pushdown systems (PDSs) generalise pushdown systems through the use of higher-order stacks, that is, a nested "stack of stacks" structure. We further generalise higher-order PDSs to higher-order Alternating PDSs (APDSs) and consider the backwards reachability problemover these systems.We prove that given an order-n APDS, the set of configurations from which a given regular set of configurations is reachable is itself regular and computable in n-EXPTIME. We show that the result has several useful applications in the verification of higher-order PDSs such as LTL model checking, alternation-free µ-calculus model checking, and the computation of winning regions of reachability games.

Hyland and Ong [HO93] recently showed that given an arbitrary (right-absorptive) conditionally partial combinatory algebra (Cpca), there is a systematic way to construct a Kreisel-style modified realizability topos which has more than sufficient completeness properties to provide a categorical semantics for a wide range of higher type theories. Based on the topos generated from the C-pca of an appropriate quotient of the strongly normalising untyped λ*-terms (where * is just a formal constant), they obtained a “generic” strong normalization argument. This argument reduces the strong normalization property of a class of higher type theories (up to Fω) to the validity of two “stripping arguments” which are reasonably easy to verify. This paper reports work which carries the same programme a step further. We illustrate the general applicability and simplicity of the argument by bringing it to bear on the demanding test case of Coquand and Huets' Calculus of Constructions.

A tree automaton can simulate the successful runs of a word or tree automaton working on the word or tree denoted by a level-2 lambda-tree. In particular the monadic second order theory of trees given by arbitrary, rather than only by safe, recursion schemes of level 2 is decidable. This solves the level-2 case of an open problem by Knapik, Niwinski and Urzyczyn.

We present a game model of the untyped λ-calculus, with equational theory equal to the Bohm tree λ-theory B, which is universal (i.e. every element of the model is definable by some term). This answers a question of Di Gianantonio, Franco and Honsell. Webuild on our earlier work, which uses the methods of innocent game semantics to develop a universal model inducing the maximal consistent sensible theory H*. To our knowledge these are the first syntax-independent universal models of the untyped λ-calculus.

Lambda Calculus is commonly thought to be the basis for functional programming. However, there is a fundamental mismatch between the “standard” theory of sensible Lambda Calculus and the practice of lazy evaluation which is a distinctive feature of functional programming. This paper proposes modification of a number of key notions in the sensible theory along the lines of laziness. Starting from the strongly unsolvables as the meaningless terms, we define and investigate properties of lazy (or weakly sensible) λ-theories, lazy λ-models and a number of lazy behavioural preorders on λ-terms. In the second part, we show that all these notions have a natural place in a class of lazy PSE-models. A major result of this paper is a new local structure theorem for lazy PSE-models. This characterizes the ordering between denotations of λ-terms in the model by a new lazy behavioural preorder.

We consider the non-deterministic extension of the call-by-value lambda calculus, which corresponds to the additive fragment of the linear-algebraic lambda-calculus. We define a fine-grained type system, capturing the right linearity present in such formalisms. After proving the subject reduction and the strong normalisation properties, we propose a translation of this calculus into the System F with pairs, which corresponds to a non linear fragment of linear logic. The translation provides a deeper understanding of the linearity in our setting., 15 pages. To appear in WoLLIC 2012

International audience; We study the decidability status of model-checking freeze LTL over various subclasses of counter machines for which the reachability problem is known to be decidable (reversal-bounded counter machines, vector additions systems with states, flat counter machines, one-counter machines). In freeze LTL, a register can store a counter value and at some future position an equality test can be done between a register and a counter value. Herein, we complete an earlier work started on one-counter machines by considering other subclasses of counter machines, and especially the class of reversal-bounded counter machines. This gives us the opportuniy to provide a systematic classification that distinguishes determinism vs. nondeterminism and we consider subclasses of formulae by restricting the set of atomic formulae or\slash and the polarity of the occurrences of the freeze operators, leading to the flat fragment.

International audience; The reachability analysis of recursive programs that commu- nicate asynchronously over reliable Fifo channels calls for restrictions to ensure decidability. We extend here a model proposed by [La Torre et al. 2008], based on communicating pushdown sys- tems that can dequeue with empty stack only. Our extension adds the dual modality, which allows to dequeue with non-empty stack, and thus models interrupts for working threads. We study (possibly cyclic) net- work architectures under a semantic assumption on communication that ensures the decidability of reachability for finite state systems. Subse- quently, we determine precisely how pushdowns can be added to this setting while preserving the decidability; in the positive case we obtain exponential time as the exact complexity bound of reachability. A sec- ond result is a generalization of the doubly exponential time algorithm of [La Torre et al. 2008] for bounded context analysis to our symmetric queueing policy. We provide here a direct and simpler algorithm.

International audience; The model checking problem for open systems (module checking ) has recently been the sub ject of extensive study. The prob- lem was first studied by Kupferman, Vardi, and Wolper for finite-state systems and properties expressed in the branching time logics CTL and CTL∗ . Further study continued mainly in two directions: considering systems equipped with a pushdown store, and considering environments with imperfect information about the system. A recent paper combined the two directions and considered the CTL pushdown module checking problem in the imperfect information set- ting, i.e., in the case where the environment has only a partial view of the system control states and pushdown store content. It has been shown that this problem is undecidable when the environment has imperfect information about the pushdown store content, while it is decidable and 2Exptime-complete when the imperfect information only concerns con- trol states. It was left open whether the latter remains decidable also for more expressive logics. In this paper, we answer this question in the affirmative, showing that the pushdown module checking problem with imperfect information about the control states is decidable and 2Exptime-complete for the propositional and the graded µ-calculus, and 3Exptime-complete for CTL∗ .

Typing of lambda-terms in Elementary and Light Affine Logic (EAL, LAL, resp.) has been studied for two different reasons: on the one hand the evaluation of typed terms using LAL (EAL, resp.) proof-nets admits a guaranteed polynomial (elementary, resp.) bound; on the other hand these terms can also be evaluated by optimal reduction using the abstract version of Lamping's algorithm. The first reduction is global while the second one is local and asynchronous. We prove that for LAL (EAL, resp.) typed terms, Lamping's abstract algorithm also admits a polynomial (elementary, resp.) bound. We also show its soundness and completeness (for EAL and LAL with type fixpoints), by using a simple geometry of interaction model (context semantics)., Comment: 21 pages

We show that the modular decomposition of a countable graph can be defined from this graph, given with an enumeration of its set of vertices, by formulas of Monadic Second-Order logic. A second main result is the definition of a representation of modular decompositions by a low degree relational structures, also constructible by Monadic Second-Order formulas.