Foundations of Software Science and Computation Structures

Frontmatter

PDF

Open Access

Constructing a universe for the setoid model

Abstract

The setoid model is a model of intensional type theory that validates certain extensionality principles, like function extensionality and propositional extensionality, the latter being a limited form of univalence that equates logically equivalent propositions. The appeal of this model construction is that it can be constructed in a small, intensional, type theoretic metatheory, therefore giving a method to boostrap extensionality. The setoid model has been recently adapted into a formal system, namely Setoid Type Theory (SeTT). SeTT is an extension of intensional Martin-Löf type theory with constructs that give full access to the extensionality principles that hold in the setoid model.

Although already a rich theory as currently defined, SeTT currently lacks a way to internalize the notion of type beyond propositions, hence we want to extend SeTT with a universe of setoids. To this aim, we present the construction of a (non-univalent) universe of setoids within the setoid model, first as an inductive-recursive definition, which is then translated to an inductive-inductive definition and finally to an inductive family. These translations from more powerful definition schemas to simpler ones ensure that our construction can still be defined in a relatively small metatheory which includes a proof-irrelevant identity type with a strong transport rule.

Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Christian Sattler, Filippo Sestini

PDF

Open Access

Nominal Equational Problems

Abstract

We define nominal equational problems of the form \(\exists \overline{W} \forall \overline{Y} : P\), where \(P\) consists of conjunctions and disjunctions of equations \(s\approx _\alpha t\), freshness constraints \(a\#t\) and their negations: \(s \not \approx _\alpha t\) and , where \(a\) is an atom and \(s, t\) nominal terms. We give a general definition of solution and a set of simplification rules to compute solutions in the nominal ground term algebra. For the latter, we define notions of solved form from which solutions can be easily extracted and show that the simplification rules are sound, preserving, and complete. With a particular strategy for rule application, the simplification process terminates and thus specifies an algorithm to solve nominal equational problems. These results generalise previous results obtained by Comon and Lescanne for first-order languages to languages with binding operators. In particular, we show that the problem of deciding the validity of a first-order equational formula in a language with binding operators (i.e., validity modulo \(\alpha \)-equality) is decidable.

Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho, Deivid Vale

PDF

Open Access

Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy

Abstract

In rendez-vous protocols an arbitrarily large number of indistinguishable finite-state agents interact in pairs. The cut-off problem asks if there exists a number B such that all initial configurations of the protocol with at least B agents in a given initial state can reach a final configuration with all agents in a given final state. In a recent paper [17], Horn and Sangnier prove that the cut-off problem is equivalent to the Petri net reachability problem for protocols with a leader, and in for leaderless protocols. Further, for the special class of symmetric protocols they reduce these bounds to and , respectively. The problem of lowering these upper bounds or finding matching lower bounds is left open. We show that the cut-off problem is -complete for leaderless protocols, -complete for symmetric protocols with a leader, and in for leaderless symmetric protocols, thereby solving all the problems left open in [17].

A. R. Balasubramanian, Javier Esparza, Mikhail Raskin

PDF

Open Access

Fixpoint Theory – Upside Down

Abstract

Knaster-Tarski’s theorem, characterising the greatest fix- point of a monotone function over a complete lattice as the largest post-fixpoint, naturally leads to the so-called coinduction proof principle for showing that some element is below the greatest fixpoint (e.g., for providing bisimilarity witnesses). The dual principle, used for showing that an element is above the least fixpoint, is related to inductive invariants. In this paper we provide proof rules which are similar in spirit but for showing that an element is above the greatest fixpoint or, dually, below the least fixpoint. The theory is developed for non-expansive monotone functions on suitable lattices of the form \(\mathbb {M}^Y\), where Y is a finite set and \(\mathbb {M}\) an MV-algebra, and it is based on the construction of (finitary) approximations of the original functions. We show that our theory applies to a wide range of examples, including termination probabilities, behavioural distances for probabilistic automata and bisimilarity. Moreover it allows us to determine original algorithms for solving simple stochastic games.

Paolo Baldan, Richard Eggert, Barbara König, Tommaso Padoan

PDF

Open Access

“Most of” leads to undecidability: Failure of adding frequencies to LTL

Abstract

Linear Temporal Logic (LTL) interpreted on finite traces is a robust specification framework popular in formal verification. However, despite the high interest in the logic in recent years, the topic of their quantitative extensions is not yet fully explored. The main goal of this work is to study the effect of adding weak forms of percentage constraints (e.g. that most of the positions in the past satisfy a given condition, or that \(\sigma \) is the most-frequent letter occurring in the past) to fragments of LTL. Such extensions could potentially be used for the verification of influence networks or statistical reasoning. Unfortunately, as we prove in the paper, it turns out that percentage extensions of even tiny fragments of LTL have undecidable satisfiability and model-checking problems. Our undecidability proofs not only sharpen most of the undecidability results on logics with arithmetics interpreted on words known from the literature, but also are fairly simple. We also show that the undecidability can be avoided by restricting the allowed usage of the negation, and discuss how the undecidability results transfer to first-order logic on words.

Bartosz Bednarczyk, Jakub Michaliszyn

PDF

Open Access

Combining Semilattices and Semimodules

Abstract

We describe the canonical weak distributive law \(\delta :\mathcal S\mathcal P\rightarrow \mathcal P\mathcal S\) of the powerset monad \(\mathcal P\) over the S-left-semimodule monad \(\mathcal S\), for a class of semirings S. We show that the composition of \(\mathcal P\) with \(\mathcal S\) by means of such \(\delta \) yields almost the monad of convex subsets previously introduced by Jacobs: the only difference consists in the absence in Jacobs’s monad of the empty convex set. We provide a handy characterisation of the canonical weak lifting of \(\mathcal P\) to \(\mathbb {EM}(\mathcal S)\) as well as an algebraic theory for the resulting composed monad. Finally, we restrict the composed monad to finitely generated convex subsets and we show that it is presented by an algebraic theory combining semimodules and semilattices with bottom, which are the algebras for the finite powerset monad \(\mathcal P_f\).

Filippo Bonchi, Alessio Santamaria

PDF

Open Access

One-way Resynchronizability of Word Transducers

Abstract

The origin semantics for transducers was proposed in 2014, and it led to various characterizations and decidability results that are in contrast with the classical semantics. In this paper we add a further decidability result for characterizing transducers that are close to one-way transducers in the origin semantics. We show that it is decidable whether a non-deterministic two-way word transducer can be resynchronized by a bounded, regular resynchronizer into an origin-equivalent one-way transducer. The result is in contrast with the usual semantics, where it is undecidable to know if a non-deterministic two-way transducer is equivalent to some one-way transducer.

Sougata Bose, S. N. Krishna, Anca Muscholl, Gabriele Puppis

PDF

Open Access

Fair Refinement for Asynchronous Session Types

Abstract

Session types are widely used as abstractions of asynchronous message passing systems. Refinement for such abstractions is crucial as it allows improvements of a given component without compromising its compatibility with the rest of the system. In the context of session types, the most general notion of refinement is the asynchronous session subtyping, which allows to anticipate message emissions but only under certain conditions. In particular, asynchronous session subtyping rules out candidates subtypes that occur naturally in communication protocols where, e.g., two parties simultaneously send each other a finite but unspecified amount of messages before removing them from their respective buffers. To address this shortcoming, we study fair compliance over asynchronous session types and fair refinement as the relation that preserves it. This allows us to propose a novel variant of session subtyping that leverages the notion of controllability from service contract theory and that is a sound characterisation of fair refinement. In addition, we show that both fair refinement and our novel subtyping are undecidable. We also present a sound algorithm, and its implementation, which deals with examples that feature potentially unbounded buffering.

Mario Bravetti, Julien Lange, Gianluigi Zavattaro

PDF

Open Access

Running Time Analysis of Broadcast Consensus Protocols

Abstract

Broadcast consensus protocols (BCPs) are a model of computation, in which anonymous, identical, finite-state agents compute by sending/receiving global broadcasts. BCPs are known to compute all number predicates in \(\mathsf {NL}=\mathsf {NSPACE}(\log n)\) where n is the number of agents. They can be considered an extension of the well-established model of population protocols. This paper investigates execution time characteristics of BCPs. We show that every predicate computable by population protocols is computable by a BCP with expected \(\mathcal {O}(n \log n)\) interactions, which is asymptotically optimal. We further show that every log-space, randomized Turing machine can be simulated by a BCP with \(\mathcal {O}(n \log n \cdot T)\) interactions in expectation, where T is the expected runtime of the Turing machine. This allows us to characterise polynomial-time BCPs as computing exactly the number predicates in \(\mathsf {ZPL}\), i.e. predicates decidable by log-space, randomised Turing machine with zero-error in expected polynomial time where the input is encoded as unary.

Philipp Czerner, Stefan Jaax

PDF

Open Access

Leafy automata for higher-order concurrency

Abstract

Finitary Idealized Concurrent Algol (\(\mathsf {FICA}\)) is a prototypical programming language combining functional, imperative, and concurrent computation. There exists a fully abstract game model of \(\mathsf {FICA}\), which in principle can be used to prove equivalence and safety of \(\mathsf {FICA}\) programs. Unfortunately, the problems are undecidable for the whole language, and only very rudimentary decidable sub-languages are known.

We propose leafy automata as a dedicated automata-theoretic formalism for representing the game semantics of \(\mathsf {FICA}\). The automata use an infinite alphabet with a tree structure. We show that the game semantics of any \(\mathsf {FICA}\) term can be represented by traces of a leafy automaton. Conversely, the traces of any leafy automaton can be represented by a \(\mathsf {FICA}\) term. Because of the close match with \(\mathsf {FICA}\), we view leafy automata as a promising starting point for finding decidable subclasses of the language and, more generally, to provide a new perspective on models of higher-order concurrent computation.

Moreover, we identify a fragment of \(\mathsf {FICA}\) that is amenable to verification by translation into a particular class of leafy automata. Using a locality property of the latter class, where communication between levels is restricted and every other level is bounded, we show that their emptiness problem is decidable by reduction to Petri net reachability.

Alex Dixon, Ranko Lazić, Andrzej S. Murawski, Igor Walukiewicz

PDF

Open Access

Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic

Abstract

In each variant of the \(\lambda \)-calculus, factorization and normalization are two key properties that show how results are computed. Instead of proving factorization/normalization for the call-by-name (CbN) and call-by-value (CbV) variants separately, we prove them only once, for the bang calculus (an extension of the \(\lambda \)-calculus inspired by linear logic and subsuming CbN and CbV), and then we transfer the result via translations, obtaining factorization/normalization for CbN and CbV.

The approach is robust: it still holds when extending the calculi with operators and extra rules to model some additional computational features.

Claudia Faggian, Giulio Guerrieri

PDF

Open Access

Generalized Bounded Linear Logic and its Categorical Semantics

Abstract

We introduce a generalization of Girard et al.’s BLL called GBLL (and its affine variant GBAL). It is designed to capture the core mechanism of dependency in BLL, while it is also able to separate complexity aspects of BLL. The main feature of GBLL is to adopt a multi-object pseudo-semiring as a grading system of the !-modality. We analyze the complexity of cut-elimination in GBLL, and give a translation from BLL with constraints to GBAL with positivity axiom. We then introduce indexed linear exponential comonads (ILEC for short) as a categorical structure for interpreting the \({!}\)-modality of GBLL. We give an elementary example of ILEC using folding product, and a technique to modify ILECs with symmetric monoidal comonads. We then consider a semantics of BLL using the folding product on the category of assemblies of a BCI-algebra, and relate the semantics with the realizability category studied by Hofmann, Scott and Dal Lago.

Yōji Fukihara, Shin-ya Katsumata

PDF

Open Access

Focused Proof-search in the Logic of Bunched Implications

Abstract

The logic of Bunched Implications (BI) freely combines additive and multiplicative connectives, including implications; however, despite its well-studied proof theory, proof-search in BI has always been a difficult problem. The focusing principle is a restriction of the proof-search space that can capture various goal-directed proof-search procedures. In this paper we show that focused proof-search is complete for BI by first reformulating the traditional bunched sequent calculus using the simpler data-structure of nested sequents, following with a polarised and focused variant that we show is sound and complete via a cut-elimination argument. This establishes an operational semantics for focused proof-search in the logic of Bunched Implications.

Alexander Gheorghiu, Sonia Marin

PDF

Open Access

Interpolation and Amalgamation for Arrays with MaxDiff

Abstract

In this paper, the theory of McCarthy’s extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the extensionality axiom). Our maxdiff operation significantly increases the level of expressivity; however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and it is shown how to convert them into concrete interpolation algorithms via a hierarchical approach.

Silvio Ghilardi, Alessandro Gianola, Deepak Kapur

PDF

Open Access

Adjoint Reactive GUI Programming

Abstract

Most interaction with a computer is via graphical user interfaces. These are traditionally implemented imperatively, using shared mutable state and callbacks. This is efficient, but is also difficult to reason about and error prone. Functional Reactive Programming (FRP) provides an elegant alternative which allows GUIs to be designed in a declarative fashion. However, most FRP languages are synchronous and continually check for new data. This means that an FRP-style GUI will “wake up” on each program cycle. This is problematic for applications like text editors and browsers, where often nothing happens for extended periods of time, and we want the implementation to sleep until new data arrives. In this paper, we present an asynchronous FRP language for designing GUIs called \(\lambda _{\mathsf {Widget}}\). Our language provides a novel semantics for widgets, the building block of GUIs, which offers both a natural Curry–Howard logical interpretation and an efficient implementation strategy.

Christian Uldal Graulund, Dmitrij Szamozvancev, Neel Krishnaswami

PDF

Open Access

On the Expressiveness of Büchi Arithmetic

Abstract

We show that the existential fragment of Büchi arithmetic is strictly less expressive than full Büchi arithmetic of any base, and moreover establish that its \(\varSigma _2\)-fragment is already expressively complete. Furthermore, we show that regular languages of polynomial growth are definable in the existential fragment of Büchi arithmetic.

Christoph Haase, Jakub Różycki

PDF

Open Access

Parametricity for Primitive Nested Types

Abstract

This paper considers parametricity and its resulting free theorems for nested data types. Rather than representing nested types via their Church encodings in a higher-kinded or dependently typed extension of System F, we adopt a functional programming perspective and design a Hindley-Milner-style calculus with primitives for constructing nested types directly as fixpoints. Our calculus can express all nested types appearing in the literature, including truly nested types. At the term level, it supports primitive pattern matching, map functions, and fold combinators for nested types. Our main contribution is the construction of a parametric model for our calculus. This is both delicate and challenging: to ensure the existence of semantic fixpoints interpreting nested types, and thus to establish a suitable Identity Extension Lemma for our calculus, our type system must explicitly track functoriality of types, and cocontinuity conditions on the functors interpreting them must be appropriately threaded throughout the model construction. We prove that our model satisfies an appropriate Abstraction Theorem and verifies all standard consequences of parametricity for primitive nested types.

Patricia Johann, Enrico Ghiorzi, Daniel Jeffries

PDF

Open Access

The Spirit of Node Replication

Abstract

We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools.

Delia Kesner, Loïc Peyrot, Daniel Ventura

PDF

Open Access

Nondeterministic and co-Nondeterministic Implies Deterministic, for Data Languages

Abstract

We prove that if a data language and its complement are both recognized by nondeterministic register automata (without guessing), then they are also recognized by deterministic ones.

Bartek Klin, Sławomir Lasota, Szymon Toruńczyk

PDF

Open Access

Certifying Inexpressibility

Abstract

Different classes of automata on infinite words have different expressive power. Deciding whether a given language \(L \subseteq \varSigma ^\omega \) can be expressed by an automaton of a desired class can be reduced to deciding a game between Prover and Refuter: in each turn of the game, Refuter provides a letter in \(\varSigma \), and Prover responds with an annotation of the current state of the run (for example, in the case of Büchi automata, whether the state is accepting or rejecting, and in the case of parity automata, what the color of the state is). Prover wins if the sequence of annotations she generates is correct: it is an accepting run iff the word generated by Refuter is in L. We show how a winning strategy for Refuter can serve as a simple and easy-to-understand certificate to inexpressibility, and how it induces additional forms of certificates. Our framework handles all classes of deterministic automata, including ones with structural restrictions like weak automata. In addition, it can be used for refuting separation of two languages by an automaton of the desired class, and for finding automata that approximate L and belong to the desired class.

Orna Kupferman, Salomon Sickert

PDF

Open Access

A General Semantic Construction of Dependent Refinement Type Systems, Categorically

Abstract

Dependent refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of dependent refinement type systems from underlying type systems and predicate logic, that is, a construction of liftings of closed comprehension categories from given (underlying) closed comprehension categories and posetal fibrations for predicate logic. We give sufficient conditions to lift structures such as dependent products, dependent sums, computational effects, and recursion from the underlying type systems to dependent refinement type systems. We demonstrate the usage of our construction by giving semantics to a dependent refinement type system and proving soundness.

Satoshi Kura

PDF

Open Access

Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP

Abstract

We study stochastic games with energy-parity objectives, which combine quantitative rewards with a qualitative \(\omega \)-regular condition: The maximizer aims to avoid running out of energy while simultaneously satisfying a parity condition. We show that the corresponding almost-sure problem, i.e., checking whether there exists a maximizer strategy that achieves the energy-parity objective with probability 1 when starting at a given energy level k, is decidable and in \(\mathsf {NP}\cap \mathsf {coNP}\). The same holds for checking if such a k exists and if a given k is minimal.

Richard Mayr, Sven Schewe, Patrick Totzke, Dominik Wojtczak

PDF

Open Access

Nondeterministic Syntactic Complexity

Abstract

We introduce a new measure on regular languages: their nondeterministic syntactic complexity. It is the least degree of any extension of the ‘canonical boolean representation’ of the syntactic monoid. Equivalently, it is the least number of states of any subatomic nondeterministic acceptor. It turns out that essentially all previous structural work on nondeterministic state-minimality computes this measure. Our approach rests on an algebraic interpretation of nondeterministic finite automata as deterministic finite automata endowed with semilattice structure. Crucially, the latter form a self-dual category.

Robert S. R. Myers, Stefan Milius, Henning Urbat

PDF

Open Access

A String Diagrammatic Axiomatisation of Finite-State Automata

Abstract

We develop a fully diagrammatic approach to finite-state automata, based on reinterpreting their usual state-transition graphical representation as a two-dimensional syntax of string diagrams. In this setting, we are able to provide a complete equational theory for language equivalence, with two notable features. First, the proposed axiomatisation is finite— a result which is provably impossible for the one-dimensional syntax of regular expressions. Second, the Kleene star is a derived concept, as it can be decomposed into more primitive algebraic blocks.

Robin Piedeleu, Fabio Zanasi

PDF

Open Access

Work-sensitive Dynamic Complexity of Formal Languages

Abstract

Which amount of parallel resources is needed for updating a query result after changing an input? In this work we study the amount of work required for dynamically answering membership and range queries for formal languages in parallel constant time with polynomially many processors. As a prerequisite, we propose a framework for specifying dynamic, parallel, constant-time programs that require small amounts of work. This framework is based on the dynamic descriptive complexity framework by Patnaik and Immerman.

Jonas Schmidt, Thomas Schwentick, Till Tantau, Nils Vortmeier, Thomas Zeume

PDF

Open Access

Learning Pomset Automata

Abstract

We extend the \(\mathtt {L}^{\!\star }\) algorithm to learn bimonoids recognising pomset languages. We then identify a class of pomset automata that accepts precisely the class of pomset languages recognised by bimonoids and show how to convert between bimonoids and automata.

Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Alexandra Silva

PDF

Open Access

The Structure of Sum-Over-Paths, its Consequences, and Completeness for Clifford

Abstract

We show that the formalism of “Sum-Over-Path” (SOP), used for symbolically representing linear maps or quantum operators, together with a proper rewrite system, has the structure of a dagger-compact PROP. Several consequences arise from this observation:

– Morphisms of SOP are very close to the diagrams of the graphical calculus called ZH-Calculus, so we give a system of interpretation between the two

– A construction, called the discard construction, can be applied to enrich the formalism so that, in particular, it can represent the quantum measurement.

We also enrich the rewrite system so as to get the completeness of the Clifford fragments of both the initial formalism and its enriched version.

Renaud Vilmart

PDF

Open Access

A Quantified Coalgebraic van Benthem Theorem

Abstract

The classical van Benthem theorem characterizes modal logic as the bisimulation-invariant fragment of first-order logic; put differently, modal logic is as expressive as full first-order logic on bisimulation-invariant properties. This result has recently been extended to two flavours of quantitative modal logic, viz. fuzzy modal logic and probabilistic modal logic. In both cases, the quantitative van Benthem theorem states that every formula in the respective quantitative variant of first-order logic that is bisimulation-invariant, in the sense of being nonexpansive w.r.t. behavioural distance, can be approximated by quantitative modal formulae of bounded rank. In the present paper, we unify and generalize these results in three directions: We lift them to full coalgebraic generality, thus covering a wide range of system types including, besides fuzzy and probabilistic transition systems as in the existing examples, e.g. also metric transition systems; and we generalize from real-valued to quantale-valued behavioural distances, e.g. nondeterministic behavioural distances on metric transition systems; and we remove the symmetry assumption on behavioural distances, thus covering also quantitative notions of simulation.

Paul Wild, Lutz Schröder

PDF

Backmatter

PDF