 |
 |
Volume 16, Issue 1
2020
1. On the logical complexity of cyclic arithmetic
We study the logical complexity of proofs in cyclic arithmetic ($\mathsf{CA}$), as introduced in Simpson '17, in terms of quantifier alternations of formulae occurring. Writing $C\Sigma_n$ for (the logical consequences of) cyclic proofs containing only $\Sigma_n$ formulae, our main result is that $I\Sigma_{n+1}$ and $C\Sigma_n$ prove the same $\Pi_{n+1}$ theorems, for all $n\geq 0$. Furthermore, due to the 'uniformity' of our method, we also show that $\mathsf{CA}$ and Peano Arithmetic ($\mathsf{PA}$) proofs of the same theorem differ only exponentially in size. The inclusion $I\Sigma_{n+1} \subseteq C\Sigma_n$ is obtained by proof theoretic techniques, relying on normal forms and structural manipulations of $\mathsf{PA}$ proofs. It improves upon the natural result that $I\Sigma_n$ is contained in $C\Sigma_n$. The converse inclusion, $C\Sigma_n \subseteq I\Sigma_{n+1}$, is obtained by calibrating the approach of Simpson '17 with recent results on the reverse mathematics of Büchi's theorem in Ko{\l}odziejczyk, Michalewski, Pradic & Skrzypczak '16 (KMPS'16), and specialising to the case of cyclic proofs. These results improve upon the bounds on proof complexity and logical complexity implicit in Simpson '17 and also an alternative approach due to Berardi & Tatsuta '17. The uniformity of our method also allows us to recover a metamathematical account of fragments of $\mathsf{CA}$; in particular we show that, for $n\geq […]
2. Modalities in homotopy type theory
Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a "localization" higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.
3. Non-idempotent types for classical calculi in natural deduction style
In the first part of this paper, we define two resource aware typing systems for the {\lambda}{\mu}-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments-based on decreasing measures of type derivations-to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the lengths of the head reduction and the maximal reduction sequences to normal-form. In the second part of this paper, the {\lambda}{\mu}-calculus is refined to a small-step calculus called {\lambda}{\mu}s, which is inspired by the substitution at a distance paradigm. The {\lambda}{\mu}s-calculus turns out to be compatible with a natural extensionof the non-idempotent interpretations of {\lambda}{\mu}, i.e., {\lambda}{\mu}s-reduction preserves and decreases typing derivations in an extended appropriate typing system. We thus derive a simple arithmetical characterization of strongly {\lambda}{\mu}s-normalizing terms by means of typing.
4. A Categorical Reconstruction of Quantum Theory
We reconstruct finite-dimensional quantum theory from categorical principles. That is, we provide properties ensuring that a given physical theory described by a dagger compact category in which one may `discard' objects is equivalent to a generalised finite-dimensional quantum theory over a suitable ring $S$. The principles used resemble those due to Chiribella, D'Ariano and Perinotti. Unlike previous reconstructions, our axioms and proof are fully categorical in nature, in particular not requiring tomography assumptions. Specialising the result to probabilistic theories we obtain either traditional quantum theory with $S$ being the complex numbers, or that over real Hilbert spaces with $S$ being the reals.
5. Language Preservation Problems in Parametric Timed Automata
Parametric timed automata (PTA) are a powerful formalism to model and reason about concurrent systems with some unknown timing delays. In this paper, we address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter valuation with the same untimed language, or with the same set of traces? We show that these problems are undecidable both for general PTA and for the restricted class of L/U-PTA, even for integer-valued parameters, or over bounded time. On the other hand, we exhibit decidable subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA. We also consider robust versions of these problems, where we additionally require that the language be preserved for all valuations between the reference valuation and the new valuation.
6. Probabilistic logics based on Riesz spaces
We introduce a novel real-valued endogenous logic for expressing properties of probabilistic transition systems called Riesz modal logic. The design of the syntax and semantics of this logic is directly inspired by the theory of Riesz spaces, a mature field of mathematics at the intersection of universal algebra and functional analysis. By using powerful results from this theory, we develop the duality theory of the Riesz modal logic in the form of an algebra-to-coalgebra correspondence. This has a number of consequences including: a sound and complete axiomatization, the proof that the logic characterizes probabilistic bisimulation and other convenient results such as completion theorems. This work is intended to be the basis for subsequent research on extensions of Riesz modal logic with fixed-point operators.
7. Call-by-name Gradual Type Theory
We present gradual type theory, a logic and type theory for call-by-name gradual typing. We define the central constructions of gradual typing (the dynamic type, type casts and type error) in a novel way, by universal properties relative to new judgments for gradual type and term dynamism, which were developed in blame calculi and to state the "gradual guarantee" theorem of gradual typing. Combined with the ordinary extensionality ($\eta$) principles that type theory provides, we show that most of the standard operational behavior of casts is uniquely determined by the gradual guarantee. This provides a semantic justification for the definitions of casts, and shows that non-standard definitions of casts must violate these principles. Our type theory is the internal language of a certain class of preorder categories called equipments. We give a general construction of an equipment interpreting gradual type theory from a 2-category representing non-gradual types and programs, which is a semantic analogue of Findler and Felleisen's definitions of contracts, and use it to build some concrete domain-theoretic models of gradual typing.
8. Efficient and Modular Coalgebraic Partition Refinement
We present a generic partition refinement algorithm that quotients coalgebraic systems by behavioural equivalence, an important task in system analysis and verification. Coalgebraic generality allows us to cover not only classical relational systems but also, e.g. various forms of weighted systems and furthermore to flexibly combine existing system types. Under assumptions on the type functor that allow representing its finite coalgebras in terms of nodes and edges, our algorithm runs in time $\mathcal{O}(m\cdot \log n)$ where $n$ and $m$ are the numbers of nodes and edges, respectively. The generic complexity result and the possibility of combining system types yields a toolbox for efficient partition refinement algorithms. Instances of our generic algorithm match the run-time of the best known algorithms for unlabelled transition systems, Markov chains, deterministic automata (with fixed alphabets), Segala systems, and for color refinement.
9. Descriptive Complexity for Counting Complexity Classes
Descriptive Complexity has been very successful in characterizing complexity classes of decision problems in terms of the properties definable in some logics. However, descriptive complexity for counting complexity classes, such as FP and #P, has not been systematically studied, and it is not as developed as its decision counterpart. In this paper, we propose a framework based on Weighted Logics to address this issue. Specifically, by focusing on the natural numbers we obtain a logic called Quantitative Second Order Logics (QSO), and show how some of its fragments can be used to capture fundamental counting complexity classes such as FP, #P and FPSPACE, among others. We also use QSO to define a hierarchy inside #P, identifying counting complexity classes with good closure and approximation properties, and which admit natural complete problems. Finally, we add recursion to QSO, and show how this extension naturally captures lower counting complexity classes such as #L.
10. Signatures and Induction Principles for Higher Inductive-Inductive Types
Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support equality constructors, thus generalizing higher inductive types of homotopy type theory. Examples that make use of both features are the Cauchy real numbers and the well-typed syntax of type theory where conversion rules are given as equality constructors. In this paper we propose a general definition of HIITs using a small type theory, named the theory of signatures. A context in this theory encodes a HIIT by listing the constructors. We also compute notions of induction and recursion for HIITs, by using variants of syntactic logical relation translations. Building full categorical semantics and constructing initial algebras is left for future work. The theory of HIIT signatures was formalised in Agda together with the syntactic translations. We also provide a Haskell implementation, which takes signatures as input and outputs translation results as valid Agda code.
11. An operational interpretation of coinductive types
We introduce an operational rewriting-based semantics for strictly positive nested higher-order (co)inductive types. The semantics takes into account the "limits" of infinite reduction sequences. This may be seen as a refinement and generalization of the notion of productivity in term rewriting to a setting with higher-order functions and with data specified by nested higher-order inductive and coinductive definitions. Intuitively, we interpret lazy data structures in a higher-order functional language by potentially infinite terms corresponding to their complete unfoldings. We prove an approximation theorem which essentially states that if a term reduces to an arbitrarily large finite approximation of an infinite object in the interpretation of a coinductive type, then it infinitarily (i.e. in the "limit") reduces to an infinite object in the interpretation of this type. We introduce a sufficient syntactic correctness criterion, in the form of a type system, for finite terms decorated with type information. Using the approximation theorem, we show that each well-typed term has a well-defined interpretation in our semantics.
12. Undecidability of a weak version of MSO+U
We prove the undecidability of MSO on $\omega$-words extended with the second-order predicate $U_1(X)$ which says that the distance between consecutive positions in a set $X \subseteq \mathbb{N}$ is unbounded. This is achieved by showing that adding $U_1$ to MSO gives a logic with the same expressive power as $MSO+U$, a logic on $\omega$-words with undecidable satisfiability. As a corollary, we prove that MSO on $\omega$-words becomes undecidable if allowing to quantify over sets of positions that are ultimately periodic, i.e., sets $X$ such that for some positive integer $p$, ultimately either both or none of positions $x$ and $x+p$ belong to $X$.
13. Overlap Algebras: a Constructive Look at Complete Boolean Algebras
The notion of a complete Boolean algebra, although completely legitimate in constructive mathematics, fails to capture some natural structures such as the lattice of subsets of a given set. Sambin's notion of an overlap algebra, although classically equivalent to that of a complete Boolean algebra, has powersets and other natural structures as instances. In this paper we study the category of overlap algebras as an extension of the category of sets and relations, and we establish some basic facts about mono-epi-isomorphisms and (co)limits; here a morphism is a symmetrizable function (with classical logic this is just a function which preserves joins). Then we specialize to the case of morphisms which preserve also finite meets: classically, this is the usual category of complete Boolean algebras. Finally, we connect overlap algebras with locales, and their morphisms with open maps between locales, thus obtaining constructive versions of some results about Boolean locales.
14. Minimization of visibly pushdown automata is NP-complete
We show that the minimization of visibly pushdown automata is NP-complete. This result is obtained by introducing immersions, that recognize multiple languages (over a usual, non-visible alphabet) using a common deterministic transition graph, such that each language is associated with an initial state and a set of final states. We show that minimizing immersions is NP-complete, and reduce this problem to the minimization of visibly pushdown automata.
15. Covariance and Controvariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers)
Twenty years ago, in an article titled "Covariance and contravariance: conflict without a cause", I argued that covariant and contravariant specialization of method parameters in object-oriented programming had different purposes and deduced that, not only they could, but actually they should both coexist in the same language. In this work I reexamine the result of that article in the light of recent advances in (sub-)typing theory and programming languages, taking a fresh look at this old issue. Actually, the revamping of this problem is just an excuse for writing an essay that aims at explaining sophisticated type-theoretic concepts, in simple terms and by examples, to undergraduate computer science students and/or willing functional programmers. Finally, I took advantage of this opportunity to describe some undocumented advanced techniques of type-systems implementation that are known only to few insiders that dug in the code of some compilers: therefore, even expert language designers and implementers may find this work worth of reading. This is a corrected version of the paper arXiv:1809.01427v7 published originally on Feb. 13, 2020.
16. Regular Tree Algebras
We introduce a class of algebras that can be used as recognisers for regular tree languages. We show that it is the only such class that forms a pseudo-variety and we prove the existence of syntactic algebras. Finally, we give a more algebraic characterisation of the algebras in our class.
17. Continuous Regular Functions
Following Chaudhuri, Sankaranarayanan, and Vardi, we say that a function $f:[0,1] \to [0,1]$ is $r$-regular if there is a Büchi automaton that accepts precisely the set of base $r \in \mathbb{N}$ representations of elements of the graph of $f$. We show that a continuous $r$-regular function $f$ is locally affine away from a nowhere dense, Lebesgue null, subset of $[0,1]$. As a corollary we establish that every differentiable $r$-regular function is affine. It follows that checking whether an $r$-regular function is differentiable is in $\operatorname{PSPACE}$. Our proofs rely crucially on connections between automata theory and metric geometry developed by Charlier, Leroy, and Rigo.
18. McShane-Whitney extensions in constructive analysis
Within Bishop-style constructive mathematics we study the classical McShane-Whitney theorem on the extendability of real-valued Lipschitz functions defined on a subset of a metric space. Using a formulation similar to the formulation of McShane-Whitney theorem, we show that the Lipschitz real-valued functions on a totally bounded space are uniformly dense in the set of uniformly continuous functions. Through the introduced notion of a McShane-Whitney pair we describe the constructive content of the original McShane-Whitney extension and examine how the properties of a Lipschitz function defined on the subspace of the pair extend to its McShane-Whitney extensions on the space of the pair. Similar McShane-Whitney pairs and extensions are established for Hölder functions and $\nu$-continuous functions, where $\nu$ is a modulus of continuity. A Lipschitz version of a fundamental corollary of the Hahn-Banach theorem, and the approximate McShane-Whitney theorem are shown.
19. On Nominal Syntax and Permutation Fixed Points
We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness relation between atoms and terms can be derived from the more primitive notion of permutation fixed-point, and use this result to prove the correctness of the new $\alpha$-equivalence axiomatisation. This gives rise to a new notion of nominal unification, where solutions for unification problems are pairs of a fixed-point context and a substitution. Although it may seem less natural than the standard notion of nominal unifier based on freshness constraints, the notion of unifier based on fixed-point constraints behaves better when equational theories are considered: for example, nominal unification remains finitary in the presence of commutativity, whereas it becomes infinitary when unifiers are expressed using freshness contexts. We provide a definition of $\alpha$-equivalence modulo equational theories that take into account A, C and AC theories. Based on this notion of equivalence, we show that C-unification is finitary and we provide a sound and complete C-unification algorithm, as a first step towards the development of nominal unification modulo AC and other equational theories with permutative properties.
20. Recursion Schemes, the MSO Logic, and the U quantifier
We study the model-checking problem for recursion schemes: does the tree generated by a given higher-order recursion scheme satisfy a given logical sentence. The problem is known to be decidable for sentences of the MSO logic. We prove decidability for an extension of MSO in which we additionally have an unbounding quantifier U, saying that a subformula is true for arbitrarily large finite sets. This quantifier can be used only for subformulae in which all free variables represent finite sets (while an unrestricted use of the quantifier leads to undecidability). We also show that the logic has the properties of reflection and effective selection for trees generated by recursion schemes.
21. The Complexity of Combinations of Qualitative Constraint Satisfaction Problems
The CSP of a first-order theory $T$ is the problem of deciding for a given finite set $S$ of atomic formulas whether $T \cup S$ is satisfiable. Let $T_1$ and $T_2$ be two theories with countably infinite models and disjoint signatures. Nelson and Oppen presented conditions that imply decidability (or polynomial-time decidability) of $\mathrm{CSP}(T_1 \cup T_2)$ under the assumption that $\mathrm{CSP}(T_1)$ and $\mathrm{CSP}(T_2)$ are decidable (or polynomial-time decidable). We show that for a large class of $\omega$-categorical theories $T_1, T_2$ the Nelson-Oppen conditions are not only sufficient, but also necessary for polynomial-time tractability of $\mathrm{CSP}(T_1 \cup T_2)$ (unless P=NP).
22. A syntactic approach to continuity of T-definable functionals
We give a new proof of the well-known fact that all functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$ which are definable in Gödel's System T are continuous via a syntactic approach. Differing from the usual syntactic method, we firstly perform a translation of System T into itself in which natural numbers are translated to functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$. Then we inductively define a continuity predicate on the translated elements and show that the translation of any term in System T satisfies the continuity predicate. We obtain the desired result by relating terms and their translations via a parametrized logical relation. Our constructions and proofs have been formalized in the Agda proof assistant. Because Agda is also a programming language, we can execute our proof to compute moduli of continuity of T-definable functions.
23. Decreasing Diagrams for Confluence and Commutation
Like termination, confluence is a central property of rewrite systems. Unlike for termination, however, there exists no known complexity hierarchy for confluence. In this paper we investigate whether the decreasing diagrams technique can be used to obtain such a hierarchy. The decreasing diagrams technique is one of the strongest and most versatile methods for proving confluence of abstract rewrite systems. It is complete for countable systems, and it has many well-known confluence criteria as corollaries. So what makes decreasing diagrams so powerful? In contrast to other confluence techniques, decreasing diagrams employ a labelling of the steps with labels from a well-founded order in order to conclude confluence of the underlying unlabelled relation. Hence it is natural to ask how the size of the label set influences the strength of the technique. In particular, what class of abstract rewrite systems can be proven confluent using decreasing diagrams restricted to 1 label, 2 labels, 3 labels, and so on? Surprisingly, we find that two labels suffice for proving confluence for every abstract rewrite system having the cofinality property, thus in particular for every confluent, countable system. Secondly, we show that this result stands in sharp contrast to the situation for commutation of rewrite relations, where the hierarchy does not collapse. Thirdly, investigating the possibility of a confluence hierarchy, we determine the first-order (non-)definability of the […]
24. Continuity of Functional Transducers: A Profinite Study of Rational Functions
A word-to-word function is continuous for a class of languages~$\mathcal{V}$ if its inverse maps $\mathcal{V}$_languages to~$\mathcal{V}$. This notion provides a basis for an algebraic study of transducers, and was integral to the characterization of the sequential transducers computable in some circuit complexity classes. Here, we report on the decidability of continuity for functional transducers and some standard classes of regular languages. To this end, we develop a robust theory rooted in the standard profinite analysis of regular languages. Since previous algebraic studies of transducers have focused on the sole structure of the underlying input automaton, we also compare the two algebraic approaches. We focus on two questions: When are the automaton structure and the continuity properties related, and when does continuity propagate to superclasses?
25. First-order queries on classes of structures with bounded expansion
We consider the evaluation of first-order queries over classes of databases with bounded expansion. The notion of bounded expansion is fairly broad and generalizes bounded degree, bounded treewidth and exclusion of at least one minor. It was known that over a class of databases with bounded expansion, first-order sentences could be evaluated in time linear in the size of the database. We give a different proof of this result. Moreover, we show that answers to first-order queries can be enumerated with constant delay after a linear time preprocessing. We also show that counting the number of answers to a query can be done in time linear in the size of the database.
26. Distances between States and between Predicates
This paper gives a systematic account of various metrics on probability distributions (states) and on predicates. These metrics are described in a uniform manner using the validity relation between states and predicates. The standard adjunction between convex sets (of states) and effect modules (of predicates) is restricted to convex complete metric spaces and directed complete effect modules. This adjunction is used in two state-and-effect triangles, for classical (discrete) probability and for quantum probability.
27. Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix
This paper establishes a bridge between linear logic and mainstream graph theory, building on previous work by Retoré (2003). We show that the problem of correctness for MLL+Mix proof nets is equivalent to the problem of uniqueness of a perfect matching. By applying matching theory, we obtain new results for MLL+Mix proof nets: a linear-time correctness criterion, a quasi-linear sequentialization algorithm, and a characterization of the sub-polynomial complexity of the correctness problem. We also use graph algorithms to compute the dependency relation of Bagnol et al. (2015) and the kingdom ordering of Bellin (1997), and relate them to the notion of blossom which is central to combinatorial maximum matching algorithms. In this journal version, we have added an explanation of Retoré's "RB-graphs" in terms of a general construction on graphs with forbidden transitions. In fact, it is by analyzing RB-graphs that we arrived at this construction, and thus obtained a polynomial-time algorithm for finding trails avoiding forbidden transitions; the latter is among the material covered in another paper by the author focusing on graph theory (arXiv:1901.07028).
28. A Universal Ordinary Differential Equation
An astonishing fact was established by Lee A. Rubel (1981): there exists a fixed non-trivial fourth-order polynomial differential algebraic equation (DAE) such that for any positive continuous function $\varphi$ on the reals, and for any positive continuous function $\epsilon(t)$, it has a $\mathcal{C}^\infty$ solution with $| y(t) - \varphi(t) | < \epsilon(t)$ for all $t$. Lee A. Rubel provided an explicit example of such a polynomial DAE. Other examples of universal DAE have later been proposed by other authors. However, Rubel's DAE \emph{never} has a unique solution, even with a finite number of conditions of the form $y^{(k_i)}(a_i)=b_i$. The question whether one can require the solution that approximates $\varphi$ to be the unique solution for a given initial data is a well known open problem [Rubel 1981, page 2], [Boshernitzan 1986, Conjecture 6.2]. In this article, we solve it and show that Rubel's statement holds for polynomial ordinary differential equations (ODEs), and since polynomial ODEs have a unique solution given an initial data, this positively answers Rubel's open problem. More precisely, we show that there exists a \textbf{fixed} polynomial ODE such that for any $\varphi$ and $\epsilon(t)$ there exists some initial condition that yields a solution that is $\epsilon$-close to $\varphi$ at all times. In particular, the solution to the ODE is necessarily analytic, and we show that the initial condition is computable from the target […]
29. Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems
In the present paper, we propose a technology for translating algorithmic descriptions of discrete functions to SAT. The proposed technology is aimed at applications in algebraic cryptanalysis. We describe how cryptanalysis problems are reduced to SAT in such a way that it should be perceived as natural by the cryptographic community. In~the theoretical part of the paper we justify the main principles of general reduction to SAT for discrete functions from a class containing the majority of functions employed in cryptography. Then, we describe the Transalg software tool developed based on these principles with SAT-based cryptanalysis specifics in mind. We demonstrate the results of applications of Transalg to construction of a number of attacks on various cryptographic functions. Some of the corresponding attacks are state of the art. We compare the functional capabilities of the proposed tool with that of other domain-specific software tools which can be used to reduce cryptanalysis problems to SAT, and also with the CBMC system widely employed in symbolic verification. The paper also presents vast experimental data, obtained using the SAT solvers that took first places at the SAT competitions in the recent several years.
30. Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory
We describe categorical models of a circuit-based (quantum) functional programming language. We show that enriched categories play a crucial role. Following earlier work on QWire by Paykin et al., we consider both a simple first-order linear language for circuits, and a more powerful host language, such that the circuit language is embedded inside the host language. Our categorical semantics for the host language is standard, and involves cartesian closed categories and monads. We interpret the circuit language not in an ordinary category, but in a category that is enriched in the host category. We show that this structure is also related to linear/non-linear models. As an extended example, we recall an earlier result that the category of W*-algebras is dcpo-enriched, and we use this model to extend the circuit language with some recursive types.
31. A new coinductive confluence proof for infinitary lambda calculus
We present a new and formal coinductive proof of confluence and normalisation of Böhm reduction in infinitary lambda calculus. The proof is simpler than previous proofs of this result. The technique of the proof is new, i.e., it is not merely a coinductive reformulation of any earlier proofs. We formalised the proof in the Coq proof assistant.
32. Automata Minimization: a Functorial Approach
In this paper we regard languages and their acceptors - such as deterministic or weighted automata, transducers, or monoids - as functors from input categories that specify the type of the languages and of the machines to categories that specify the type of outputs. Our results are as follows: A) We provide sufficient conditions on the output category so that minimization of the corresponding automata is guaranteed. B) We show how to lift adjunctions between the categories for output values to adjunctions between categories of automata. C) We show how this framework can be instantiated to unify several phenomena in automata theory, starting with determinization, minimization and syntactic algebras. We provide explanations of Choffrut's minimization algorithm for subsequential transducers and of Brzozowski's minimization algorithm in this setting.