Ten years ago, it was shown that nominal techniques can be used to design coalgebraic data types with variable binding, so that alpha-equivalence classes of infinitary terms are directly endowed with a corecursion principle. We introduce "mixed" binding signatures, as well as the corresponding type of mixed inductive-coinductive terms. We extend the aforementioned work to this setting. In particular, this allows for a nominal description of the sets Lambda_abc of abc-infinitary lambda-terms (for a, b, c in 0,1) and of capture-avoiding substitution on alpha-equivalence classes of such terms.
We prove that omega^2 strictly bounds the iterations required for modal definable functions to reach a fixed point across all countable structures. The result corrects and extends the previously claimed result by the first and third authors on closure ordinals of the alternation-free mu-calculus in [3]. The new approach sees a reincarnation of Kozen's well-annotations, devised for showing the finite model property for the modal mu-calculus. We develop a theory of 'conservative' well-annotations where minimality of annotations is guaranteed, and isolate parts of the structure that locally determine the closure ordinal of relevant formulas. This adoption of well-annotations enables a direct and clear pumping process that rules out closure ordinals between omega^2 and the limit of countability.
The characterization of PSPACE-queries over ordered structures as exactly those expressible in first-order logic with partial fixpoints (Vardi'82) is one of the classical results in the field of descriptive complexity. In this paper, we extend this result to characterizations of k-EXPSPACE-queries for arbitrary k, characterizing them as exactly those expressible in order-k+1-higher-order logic with partial fixpoints. For k>1, the restriction to ordered structures is no longer necessary due to the high expressive power of higher-order logic.
The modal mu-calculus is obtained by adding least and greatest fixed-point operators to modal logic. Its alternation hierarchy classifies the mu-formulas by their alternation depth: a measure of the codependence of their least and greatest fixed-point operators. The mu-calculus' alternation hierarchy is strict over the class of all Kripke frames: for all n, there is a mu-formula with alternation depth n+1 which is not equivalent to any formula with alternation depth n. This does not always happen if we restrict the semantics. For example, every mu-formula is equivalent to a formula without fixed-point operators over S5 frames. We show that the multimodal mu-calculus' alternation hierarchy is strict over non-trivial fusions of modal logics. We also comment on two examples of multimodal logics where the mu-calculus collapses to modal logic.
We consider modal logic extended with the well-known temporal operator 'eventually' and provide a cut-elimination procedure for a cyclic sequent calculus that captures this fragment. The work showcases an adaptation of the reductive cut-elimination method to cyclic calculi. Notably, the proposed algorithm applies to a cyclic proof and directly outputs a cyclic cut-free proof without appealing to intermediate machinery for regularising the end proof.
We propose a method for solving parity games with acyclic (DAG) sub-structures by computing nested fixpoints of a DAG attractor function that lives over the non-DAG parts of the game, thereby restricting the domain of the involved fixpoint operators. Intuitively, this corresponds to accelerating fixpoint computation by inlining cycle-free parts during the solution of parity games, leading to earlier convergence. We also present an economic later-appearance-record construction that takes Emerson-Lei games to parity games, and show that it preserves DAG sub-structures; it follows that the proposed method can be used also for the accelerated solution of Emerson-Lei games.
In 1984, Wim Ruitenburg published a surprising result about periodic sequences in intuitionistic propositional calculus (IPC). The property established by Ruitenburg naturally generalizes local finiteness; recall that intuitionistic logic is not locally finite, even in a single variable. One of the two main goals of this note is to illustrate that most "natural" non-classical logics failing local finiteness also do not enjoy the periodic sequence property. IPC is quite unique in separating these properties. The other goal of this note is to present a Coq formalization of Ruitenburg's heavily syntactic proof. Apart from ensuring its correctness, the formalization allows extraction of a program providing a certified implementation of Ruitenburg's algorithm.
Daniyar Shamkanov proved that three distinct systems of sequent calculi for GL are equivalent. These systems consist in one with finite proofs, another with ill-founded proofs and the last one with cyclic proofs. The main tool used for proving the equivalence is corecursion. In this project, we prove the equivalence between a finitary sequent calculus for iGL and a cyclic calculus, using also coinductive methods.
We explore the theory of illfounded and cyclic proofs for the propositional modal μ-calculus. A fine analysis of provability for classical and intuitionistic modal logic provides a novel bridge between finitary, cyclic and illfounded conceptions of proof and re-enforces the importance of two normal form theorems for the logic: guardedness and disjunctiveness.
Formal theories of arithmetic have traditionally been based on either classical or intuitionistic logic, leading to the development of Peano and Heyting arithmetic, respectively. We propose to use μMALL as a formal theory of arithmetic based on linear logic. This formal system is presented as a sequent calculus proof system that extends the standard proof system for multiplicative-additive linear logic (MALL) with the addition of the logical connectives universal and existential quantifiers (first-order quantifiers), term equality and non-equality, and the least and greatest fixed point operators. We first demonstrate how functions defined using μMALL relational specifications can be computed using a simple proof search algorithm. By incorporating weakening and contraction into μMALL, we obtain μLK+, a natural candidate for a classical sequent calculus for arithmetic. While important proof theory results are still lacking for μLK+ (including cut-elimination and the completeness of focusing), we prove that μLK+ is consistent and that it contains Peano arithmetic. We also prove some conservativity results regarding μLK+ over μMALL.
We show how the relatively initial or relatively terminal fixed points for a well-behaved functor $F$ form a pair of adjoint functors between $F$-coalgebras and $F$-algebras. We use the language of locally presentable categories to find sufficient conditions for existence of this adjunction. We show that relative fixed points may be characterized as (co)equalizers of the free (co)monad on $F$. In particular, when $F$ is a polynomial functor on $\mathsf{Set}$ the relative fixed points are a quotient or subset of the free term algebra or the cofree term coalgebra. We give examples of the relative fixed points for polynomial functors and an example which is the Sierpinski carpet. Lastly, we prove a general preservation result for relative fixed points.
In functional programming, datatypes a la carte provide a convenient modular representation of recursive datatypes, based on their initial algebra semantics. Unfortunately it is highly challenging to implement this technique in proof assistants that are based on type theory, like Coq. The reason is that it involves type definitions, such as those of type-level fixpoint operators, that are not strictly positive. The known work-around of impredicative encodings is problematic, insofar as it impedes conventional inductive reasoning. Weak induction principles can be used instead, but they considerably complicate proofs. This paper proposes a novel and simpler technique to reason inductively about impredicative encodings, based on Mendler-style induction. This technique involves dispensing with dependent induction, ensuring that datatypes can be lifted to predicates and relying on relational formulations. A case study on proving subject reduction for structural operational semantics illustrates that the approach enables modular proofs, and that these proofs are essentially similar to conventional ones.
We present a coalgebraic generalisation of Fischer and Ladner's Propositional Dynamic Logic (PDL) and Parikh's Game Logic (GL). In earlier work, we proved a generic strong completeness result for coalgebraic dynamic logics without iteration. The coalgebraic semantics of such programs is given by a monad T, and modalities are interpreted via a predicate lifting λ whose transpose is a monad morphism from T to the neighbourhood monad. In this paper, we show that if the monad T carries a complete semilattice structure, then we can define an iteration construct, and suitable notions of diamond-likeness and box-likeness of predicate-liftings which allows for the definition of an axiomatisation parametric in T, λ and a chosen set of pointwise program operations. As our main result, we show that if the pointwise operations are "negation-free" and Kleisli composition left-distributes over the induced join on Kleisli arrows, then this axiomatisation is weakly complete with respect to the class of standard models. As special instances, we recover the weak completeness of PDL and of dual-free Game Logic. As a modest new result we obtain completeness for dual-free GL extended with intersection (demonic choice) of games.
Usual termination proofs for a functional program require to check all the possible reduction paths. Due to an exponential gap between the height and size of such the reduction tree, no naive formalization of termination proofs yields a connection to the polynomial complexity of the given program. We solve this problem employing the notion of minimal function graph, a set of pairs of a term and its normal form, which is defined as the least fixed point of a monotone operator. We show that termination proofs for programs reducing under lexicographic path orders (LPOs for short) and polynomially quasi-interpretable can be optimally performed in a weak fragment of Peano arithmetic. This yields an alternative proof of the fact that every function computed by an LPO-terminating, polynomially quasi-interpretable program is computable in polynomial space. The formalization is indeed optimal since every polynomial-space computable function can be computed by such a program. The crucial observation is that inductive definitions of minimal function graphs under LPO-terminating programs can be approximated with transfinite induction along LPOs.
In this paper, I establish the categorical structure necessary to interpret dependent inductive and coinductive types. It is well-known that dependent type theories 'a la Martin-Lof can be interpreted using fibrations. Modern theorem provers, however, are based on more sophisticated type systems that allow the definition of powerful inductive dependent types (known as inductive families) and, somewhat limited, coinductive dependent types. I define a class of functors on fibrations and show how data type definitions correspond to initial and final dialgebras for these functors. This description is also a proposal of how coinductive types should be treated in type theories, as they appear here simply as dual of inductive types. Finally, I show how dependent data types correspond to algebras and coalgebras, and give the correspondence to dependent polynomial functors.
We consider relations with no order on their attributes as in Database Theory. An independent partition of the set of attributes S of a finite relation R is any partition X of S such that the join of the projections of R over the elements of X yields R. Identifying independent partitions has many applications and corresponds conceptually to revealing orthogonality between sets of dimensions in multidimensional point spaces. A subset of S is termed self-correlated if there is a value of each of its attributes such that no tuple of R contains all those values. This paper uncovers a connection between independence and self-correlation, showing that the maximum independent partition is the least fixed point of a certain inflationary transformer alpha that operates on the finite lattice of partitions of S. alpha is defined via the minimal self-correlated subsets of S. We use some additional properties of alpha to show the said fixed point is still the limit of the standard approximation sequence, just as in Kleene's well-known fixed point theorem for continuous functions.
In the modal mu-calculus, a formula is well-formed if each recursive variable occurs underneath an even number of negations. By means of De Morgan's laws, it is easy to transform any well-formed formula into an equivalent formula without negations – its negation normal form. Moreover, if the formula is of size n, its negation normal form of is of the same size O(n). The full modal mu-calculus and the negation normal form fragment are thus equally expressive and concise. In this paper we extend this result to the higher-order modal fixed point logic (HFL), an extension of the modal mu-calculus with higher-order recursive predicate transformers. We present a procedure that converts a formula into an equivalent formula without negations of quadratic size in the worst case and of linear size when the number of variables of the formula is fixed.
This paper shows an application of Bloom and Esik's iteration algebras to model graph data in a graph database query language. About twenty years ago, Buneman et al. developed a graph database query language UnQL on the top of a functional meta-language UnCAL for describing and manipulating graphs. Recently, the functional programming community has shown renewed interest in UnCAL, because it provides an efficient graph transformation language which is useful for various applications, such as bidirectional computation. However, no mathematical semantics of UnQL/UnCAL graphs has been developed. In this paper, we give an equational axiomatisation and algebraic semantics of UnCAL graphs. The main result of this paper is to prove that completeness of our equational axioms for UnCAL for the original bisimulation of UnCAL graphs via iteration algebras. Another benefit of algebraic semantics is a clean characterisation of structural recursion on graphs using free iteration algebra.
The polyadic mu-calculus is a modal fixpoint logic whose formulas define relations of nodes rather than just sets in labelled transition systems. It can express exactly the polynomial-time computable and bisimulation-invariant queries on finite graphs. In this paper we show a hierarchy result with respect to expressive power inside the polyadic mu-calculus: for every level of fixpoint alternation, greater arity of relations gives rise to higher expressive power. The proof uses a diagonalisation argument.
This paper studies the relationship between disjunctive form, a syntactic normal form for the modal mu calculus, and the alternation hierarchy. First it shows that all disjunctive formulas which have equivalent tableau have the same syntactic alternation depth. However, tableau equivalence only preserves alternation depth for the disjunctive fragment: there are disjunctive formulas with arbitrarily high alternation depth that are tableau equivalent to alternation-free non-disjunctive formulas. Conversely, there are non-disjunctive formulas of arbitrarily high alternation depth that are tableau equivalent to disjunctive formulas without alternations. This answers negatively the so far open question of whether disjunctive form preserves alternation depth. The classes of formulas studied here illustrate a previously undocumented type of avoidable syntactic complexity which may contribute to our understanding of why deciding the alternation hierarchy is still an open problem.
