In programming models with a reversible semantics, computational steps can be
undone. This paper addresses the integration of reversible semantics into
process languages for communication-centric systems equipped with behavioral
types. In prior work, we introduced a monitors-as-memories approach to
seamlessly integrate reversible semantics into a process model in which
concurrency is governed by session types (a class of behavioral types),
covering binary (two-party) protocols with synchronous communication. The
applicability and expressiveness of the binary setting, however, is limited.
Here we extend our approach, and use it to define reversible semantics for an
expressive process model that accounts for multiparty (n-party) protocols,
asynchronous communication, decoupled rollbacks, and abstraction passing. As
main result, we prove that our reversible semantics for multiparty protocols is
causally-consistent. A key technical ingredient in our developments is an
alternative reversible semantics with atomic rollbacks, which is conceptually
simple and is shown to characterize decoupled rollbacks.
Inference systems are a widespread framework used to define possibly
recursive predicates by means of inference rules. They allow both inductive and
coinductive interpretations that are fairly well-studied. In this paper, we
consider a middle way interpretation, called regular, which combines advantages
of both approaches: it allows non-well-founded reasoning while being finite. We
show that the natural proof-theoretic definition of the regular interpretation,
based on regular trees, coincides with a rational fixed point. Then, we provide
an equivalent inductive characterization, which leads to an algorithm which
looks for a regular derivation of a judgment. Relying on these results, we
define proof techniques for regular reasoning: the regular coinduction
principle, to prove completeness, and an inductive technique to prove
soundness, based on the inductive characterization of the regular
interpretation. Finally, we show the regular approach can be smoothly extended
to inference systems with corules, a recently introduced, generalised
framework, which allows one to refine the coinductive interpretation, proving
that also this flexible regular interpretation admits an equivalent inductive
characterisation.
We adapt our light Dialectica interpretation to usual and light modal
formulas (with universal quantification on boolean and natural variables) and
prove it sound for a non-standard modal arithmetic based on Goedel's T and
classical S4. The range of this light modal Dialectica is the usual (non-modal)
classical Arithmetic in all finite types (with booleans); the propositional
kernel of its domain is Boolean and not S4. The `heavy' modal Dialectica
interpretation is a new technique, as it cannot be simulated within our
previous light Dialectica. The synthesized functionals are at least as good as
before, while the translation process is improved. Through our modal
Dialectica, the existence of a realizer for the defining axiom of classical S5
reduces to the Drinking Principle (cf. Smullyan).
Word equations are a crucial element in the theoretical foundation of
constraint solving over strings. A word equation relates two words over string
variables and constants. Its solution amounts to a function mapping variables
to constant strings that equate the left and right hand sides of the equation.
While the problem of solving word equations is decidable, the decidability of
the problem of solving a word equation with a length constraint (i.e., a
constraint relating the lengths of words in the word equation) has remained a
long-standing open problem. We focus on the subclass of quadratic word
equations, i.e., in which each variable occurs at most twice. We first show
that the length abstractions of solutions to quadratic word equations are in
general not Presburger-definable. We then describe a class of counter systems
with Presburger transition relations which capture the length abstraction of a
quadratic word equation with regular constraints. We provide an encoding of the
effect of a simple loop of the counter systems in the existential theory of
Presburger Arithmetic with divisibility (PAD). Since PAD is decidable (NP-hard
and is in NEXP), we obtain a decision procedure for quadratic words equations
with length constraints for which the associated counter system is flat (i.e.,
all nodes belong to at most one cycle). In particular, we show a decidability
result (in fact, also an NP algorithm with a PAD oracle) for a recently
proposed NP-complete fragment of word […]
We define a computational type theory combining the contentful equality
structure of cartesian cubical type theory with internal parametricity
primitives. The combined theory supports both univalence and its relational
equivalent, which we call relativity. We demonstrate the use of the theory by
analyzing polymorphic functions between higher inductive types, observe how
cubical equality regularizes parametric type theory, and examine the
similarities and discrepancies between cubical and parametric type theory,
which are closely related. We also abstract a formal interface to the
computational interpretation and show that this also has a presheaf model.
Clock-dependent probabilistic timed automata extend classical timed automata
with discrete probabilistic choice, where the probabilities are allowed to
depend on the exact values of the clocks. Previous work has shown that the
quantitative reachability problem for clock-dependent probabilistic timed
automata with at least three clocks is undecidable. In this paper, we consider
the subclass of clock-dependent probabilistic timed automata that have one
clock, that have clock dependencies described by affine functions, and that
satisfy an initialisation condition requiring that, at some point between
taking edges with non-trivial clock dependencies, the clock must have an
integer value. We present an approach for solving in polynomial time
quantitative and qualitative reachability problems of such one-clock
initialised clock-dependent probabilistic timed automata. Our results are
obtained by a transformation to interval Markov decision processes.
We consider the following problem: given a program, find tight asymptotic
bounds on the values of some variables at the end of the computation (or at any
given program point) in terms of its input values. We focus on the case of
polynomially-bounded variables, and on a weak programming language for which we
have recently shown that tight bounds for polynomially-bounded variables are
computable. These bounds are sets of multivariate polynomials. While their
computability has been settled, the complexity of this program-analysis problem
remained open. In this paper, we show the problem to be PSPACE-complete. The
main contribution is a new, space-efficient analysis algorithm. This algorithm
is obtained in a few steps. First, we develop an algorithm for univariate
bounds, a sub-problem which is already PSPACE-hard. Then, a decision procedure
for multivariate bounds is achieved by reducing this problem to the univariate
case; this reduction is orthogonal to the solution of the univariate problem
and uses observations on the geometry of a set of vectors that represent
multivariate bounds. Finally, we transform the univariate-bound algorithm to
produce multivariate bounds.
Categorical quantum mechanics exploits the dagger compact closed structure of
finite dimensional Hilbert spaces, and uses the graphical calculus of string
diagrams to facilitate reasoning about finite dimensional processes. A
significant portion of quantum physics, however, involves reasoning about
infinite dimensional processes, and it is well-known that the category of all
Hilbert spaces is not compact closed. Thus, a limitation of using dagger
compact closed categories is that one cannot directly accommodate reasoning
about infinite dimensional processes.
A natural categorical generalization of compact closed categories, in which
infinite dimensional spaces can be modelled, is *-autonomous categories and,
more generally, linearly distributive categories. This article starts the
development of this direction of generalizing categorical quantum mechanics. An
important first step is to establish the behaviour of the dagger in these more
general settings. Thus, these notes simultaneously develop the categorical
semantics of multiplicative dagger linear logic.
The notes end with the definition of a mixed unitary category. It is this
structure which is subsequently used to extend the key features of categorical
quantum mechanics.
Given a graph whose nodes may be coloured red, the parity of the number of
red nodes can easily be maintained with first-order update rules in the dynamic
complexity framework DynFO of Patnaik and Immerman. Can this be generalised to
other or even all queries that are definable in first-order logic extended by
parity quantifiers? We consider the query that asks whether the number of nodes
that have an edge to a red node is odd. Already this simple query of quantifier
structure parity-exists is a major roadblock for dynamically capturing
extensions of first-order logic.
We show that this query cannot be maintained with quantifier-free first-order
update rules, and that variants induce a hierarchy for such update rules with
respect to the arity of the maintained auxiliary relations. Towards maintaining
the query with full first-order update rules, it is shown that
degree-restricted variants can be maintained.
Decentralized blockchain platforms have enabled the secure exchange of
crypto-assets without the intermediation of trusted authorities. To this
purpose, these platforms rely on a peer-to-peer network of byzantine nodes,
which collaboratively maintain an append-only ledger of transactions, called
blockchain. Transactions represent the actions required by users, e.g. the
transfer of some units of crypto-currency to another user, or the execution of
a smart contract which distributes crypto-assets according to its internal
logic. Part of the nodes of the peer-to-peer network compete to append
transactions to the blockchain. To do so, they group the transactions sent by
users into blocks, and update their view of the blockchain state by executing
these transactions in the chosen order. Once a block of transactions is
appended to the blockchain, the other nodes validate it, re-executing the
transactions in the same order. The serial execution of transactions does not
take advantage of the multi-core architecture of modern processors, so
contributing to limit the throughput. In this paper we develop a theory of
transaction parallelism for blockchains, which is based on static analysis of
transactions and smart contracts. We illustrate how blockchain nodes can use
our theory to parallelize the execution of transactions. Initial experiments on
Ethereum show that our technique can improve the performance of nodes.
We give extensional and intensional characterizations of functional programs
with nondeterminism: as structure preserving functions between biorders, and as
nondeterministic sequential algorithms on ordered concrete data structures
which compute them. A fundamental result establishes that these extensional and
intensional representations are equivalent, by showing how to construct the
unique sequential algorithm which computes a given monotone and stable
function, and describing the conditions on sequential algorithms which
correspond to continuity with respect to each order. We illustrate by defining
may-testing and must-testing denotational semantics for sequential functional
languages with bounded and unbounded choice operators. We prove that these are
computationally adequate, despite the non-continuity of the must-testing
semantics of unbounded nondeterminism. In the bounded case, we prove that our
continuous models are fully abstract with respect to may-testing and
must-testing by identifying a simple universal type, which may also form the
basis for models of the untyped {\lambda}-calculus. In the unbounded case we
observe that our model contains computable functions which are not denoted by
terms, by identifying a further "weak continuity" property of the definable
elements, and use this to establish that it is not fully abstract.
Bertrand et al. introduced a model of parameterised systems, where each agent
is represented by a finite state system, and studied the following control
problem: for any number of agents, does there exist a controller able to bring
all agents to a target state? They showed that the problem is decidable and
EXPTIME-complete in the adversarial setting, and posed as an open problem the
stochastic setting, where the agent is represented by a Markov decision
process. In this paper, we show that the stochastic control problem is
decidable. Our solution makes significant uses of well quasi orders, of the
max-flow min-cut theorem, and of the theory of regular cost functions. We
introduce an intermediate problem of independence interest called the
sequential flow problem and study its complexity.
Emerging application scenarios, such as cyber-physical systems (CPSs), the
Internet of Things (IoT), and edge computing, call for coordination approaches
addressing openness, self-adaptation, heterogeneity, and deployment
agnosticism. Field-based coordination is one such approach, promoting the idea
of programming system coordination declaratively from a global perspective, in
terms of functional manipulation and evolution in "space and time" of
distributed data structures called fields. More specifically regarding time, in
field-based coordination (as in many other distributed approaches to
coordination) it is assumed that local activities in each device are regulated
by a fair and unsynchronised fixed clock working at the platform level. In this
work, we challenge this assumption, and propose an alternative approach where
scheduling is programmed in a natural way (along with usual field-based
coordination) in terms of causality fields, each enacting a programmable
distributed notion of a computation "cause" (why and when a field computation
has to be locally computed) and how it should change across time and space.
Starting from low-level platform triggers, such causality fields can be
organised into multiple layers, up to high-level, collectively-computed time
abstractions, to be used at the application level. This reinterpretation of
time in terms of articulated causality relations allows us to express what we
call "time-fluid" coordination, […]
Let CMSO denote the counting monadic second order logic of graphs. We give a
constructive proof that for some computable function $f$, there is an algorithm
$\mathfrak{A}$ that takes as input a CMSO sentence $\varphi$, a positive
integer $t$, and a connected graph $G$ of maximum degree at most $\Delta$, and
determines, in time $f(|\varphi|,t)\cdot 2^{O(\Delta \cdot t)}\cdot
|G|^{O(t)}$, whether $G$ has a supergraph $G'$ of treewidth at most $t$ such
that $G'\models \varphi$. The algorithmic metatheorem described above sheds new
light on certain unresolved questions within the framework of graph completion
algorithms. In particular, using this metatheorem, we provide an explicit
algorithm that determines, in time $f(d)\cdot 2^{O(\Delta \cdot d)}\cdot
|G|^{O(d)}$, whether a connected graph of maximum degree $\Delta$ has a planar
supergraph of diameter at most $d$. Additionally, we show that for each fixed
$k$, the problem of determining whether $G$ has an $k$-outerplanar supergraph
of diameter at most $d$ is strongly uniformly fixed parameter tractable with
respect to the parameter $d$. This result can be generalized in two directions.
First, the diameter parameter can be replaced by any contraction-closed
effectively CMSO-definable parameter $\mathbf{p}$. Examples of such parameters
are vertex-cover number, dominating number, and many other
contraction-bidimensional parameters. In the second direction, the planarity
requirement can be relaxed to bounded genus, and more […]
We introduce PHFL, a probabilistic extension of higher-order fixpoint logic,
which can also be regarded as a higher-order extension of probabilistic
temporal logics such as PCTL and the $\mu^p$-calculus. We show that PHFL is
strictly more expressive than the $\mu^p$-calculus, and that the PHFL
model-checking problem for finite Markov chains is undecidable even for the
$\mu$-only, order-1 fragment of PHFL. Furthermore the full PHFL is far more
expressive: we give a translation from Lubarsky's $\mu$-arithmetic to PHFL,
which implies that PHFL model checking is $\Pi^1_1$-hard and $\Sigma^1_1$-hard.
As a positive result, we characterize a decidable fragment of the PHFL
model-checking problems using a novel type system.
The execution of an event in a complex and distributed system where the
dependencies vary during the evolution of the system can be represented in many
ways, and one of them is to use Context-Dependent Event structures. Event
structures are related to Petri nets. The aim of this paper is to propose what
can be the appropriate kind of Petri net corresponding to Context-Dependent
Event structures, giving an operational flavour to the dependencies represented
in a Context/Dependent Event structure. Dependencies are often operationally
represented, in Petri nets, by tokens produced by activities and consumed by
others. Here we shift the perspective using contextual arcs to characterize
what has happened so far and in this way to describe the dependencies among the
various activities.
We show that for every $r \ge 2$ there exists $\epsilon_r > 0$ such that any
$r$-uniform hypergraph with $m$ edges and maximum vertex degree $o(\sqrt{m})$
contains a set of at most $(\frac{1}{2} - \epsilon_r)m$ edges the removal of
which breaks the hypergraph into connected components with at most $m/2$ edges.
We use this to give an algorithm running in time $d^{(1 - \epsilon_r)m}$ that
decides satisfiability of $m$-variable $(d, k)$-CSPs in which every variable
appears in at most $r$ constraints, where $\epsilon_r$ depends only on $r$ and
$k\in o(\sqrt{m})$. Furthermore our algorithm solves the corresponding #CSP-SAT
and Max-CSP-SAT of these CSPs. We also show that CNF representations of
unsatisfiable $(2, k)$-CSPs with variable frequency $r$ can be refuted in
tree-like resolution in size $2^{(1 - \epsilon_r)m}$. Furthermore for Tseitin
formulas on graphs with degree at most $k$ (which are $(2, k)$-CSPs) we give a
deterministic algorithm finding such a refutation.
We developed a procedure to enumerate complete sets of higher-order unifiers
based on work by Jensen and Pietrzykowski. Our procedure removes many redundant
unifiers by carefully restricting the search space and tightly integrating
decision procedures for fragments that admit a finite complete set of unifiers.
We identify a new such fragment and describe a procedure for computing its
unifiers. Our unification procedure, together with new higher-order term
indexing data structures, is implemented in the Zipperposition theorem prover.
Experimental evaluation shows a clear advantage over Jensen and Pietrzykowski's
procedure.
The classical Hennessy-Milner theorem says that two states of an image-finite
transition system are bisimilar if and only if they satisfy the same formulas
in a certain modal logic. In this paper we study this type of result in a
general context, moving from transition systems to coalgebras and from
bisimilarity to coinductive predicates. We formulate when a logic fully
characterises a coinductive predicate on coalgebras, by providing suitable
notions of adequacy and expressivity, and give sufficient conditions on the
semantics. The approach is illustrated with logics characterising similarity,
divergence and a behavioural metric on automata.
Parallelization is an algebraic operation that lifts problems to sequences in
a natural way. Given a sequence as an instance of the parallelized problem,
another sequence is a solution of this problem if every component is
instance-wise a solution of the original problem. In the Weihrauch lattice
parallelization is a closure operator. Here we introduce a dual operation that
we call stashing and that also lifts problems to sequences, but such that only
some component has to be an instance-wise solution. In this case the solution
is stashed away in the sequence. This operation, if properly defined, induces
an interior operator in the Weihrauch lattice. We also study the action of the
monoid induced by stashing and parallelization on the Weihrauch lattice, and we
prove that it leads to at most five distinct degrees, which (in the maximal
case) are always organized in pentagons. We also introduce another closely
related interior operator in the Weihrauch lattice that replaces solutions of
problems by upper Turing cones that are strong enough to compute solutions. It
turns out that on parallelizable degrees this interior operator corresponds to
stashing. This implies that, somewhat surprisingly, all problems which are
simultaneously parallelizable and stashable have computability-theoretic
characterizations. Finally, we apply all these results in order to study the
recently introduced discontinuity problem, which appears as the bottom of a
number of natural […]
Efficient pattern matching is fundamental for practical term rewrite engines.
By preprocessing the given patterns into a finite deterministic automaton the
matching patterns can be decided in a single traversal of the relevant parts of
the input term. Most automaton-based techniques are restricted to linear
patterns, where each variable occurs at most once, and require an additional
post-processing step to check so-called variable consistency. However, we can
show that interleaving the variable consistency and pattern matching phases can
reduce the number of required steps to find all matches. Therefore, we take the
existing adaptive pattern matching automata as introduced by Sekar et al and
extend these with consistency checks. We prove that the resulting deterministic
pattern matching automaton is correct, and show several examples where some
reduction can be achieved.
We examine some combinatorial properties of parallel cut elimination in
multiplicative linear logic (MLL) proof nets. We show that, provided we impose
a constraint on some paths, we can bound the size of all the nets satisfying
this constraint and reducing to a fixed resultant net. This result gives a
sufficient condition for an infinite weighted sum of nets to reduce into
another sum of nets, while keeping coefficients finite. We moreover show that
our constraints are stable under reduction.
Our approach is motivated by the quantitative semantics of linear logic: many
models have been proposed, whose structure reflect the Taylor expansion of
multiplicative exponential linear logic (MELL) proof nets into infinite sums of
differential nets. In order to simulate one cut elimination step in MELL, it is
necessary to reduce an arbitrary number of cuts in the differential nets of its
Taylor expansion. It turns out our results apply to differential nets, because
their cut elimination is essentially multiplicative. We moreover show that the
set of differential nets that occur in the Taylor expansion of an MELL net
automatically satisfies our constraints.
Interestingly, our nets are untyped: we only rely on the sequentiality of
linear logic nets and the dynamics of cut elimination. The paths on which we
impose bounds are the switching paths involved in the Danos--Regnier criterion
for sequentiality. In order to accommodate multiplicative units and weakenings,
our nets come […]
This paper considers parametricity and its consequent 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 level of terms, 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. In particular, 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 also prove that our model satisfies an appropriate Abstraction
Theorem, as well as that it verifies all standard consequences of parametricity
in the presence of primitive nested types. We give several concrete examples
illustrating how our model can be used to derive useful free theorems,
including a short cut fusion transformation, for programs over nested types.
Finally, we consider generalizing our results to GADTs, and […]
We present a general coalgebraic setting in which we define finite and
infinite behaviour with Büchi acceptance condition for systems whose type is
a monad. The first part of the paper is devoted to presenting a construction of
a monad suitable for modelling (in)finite behaviour. The second part of the
paper focuses on presenting the concepts of a (coalgebraic) automaton and its
($\omega$-) behaviour. We end the paper with coalgebraic Kleene-type theorems
for ($\omega$-) regular input. The framework is instantiated on
non-deterministic (Büchi) automata, tree automata and probabilistic automata.
We study the expressive power of subrecursive probabilistic higher-order
calculi. More specifically, we show that endowing a very expressive
deterministic calculus like Gödel's $\mathbb{T}$ with various forms of
probabilistic choice operators may result in calculi which are not equivalent
as for the class of distributions they give rise to, although they all
guarantee almost-sure termination. Along the way, we introduce a probabilistic
variation of the classic reducibility technique, and we prove that the simplest
form of probabilistic choice leaves the expressive power of $\mathbb{T}$
essentially unaltered. The paper ends with some observations about the
functional expressive power: expectedly, all the considered calculi capture the
functions which $\mathbb{T}$ itself represents, at least when standard notions
of observations are considered.
One of the key aspects in component-based design is specifying the software
architecture that characterizes the topology and the permissible interactions
of the components of a system. To achieve well-founded design there is need to
address both the qualitative and non-functional aspects of architectures. In
this paper we study the qualitative and quantitative formal modelling of
architectures applied on parametric component-based systems, that consist of an
unknown number of instances of each component. Specifically, we introduce an
extended propositional interaction logic and investigate its first-order level
which serves as a formal language for the interactions of parametric systems.
Our logics achieve to encode the execution order of interactions, which is a
main feature in several important architectures, as well as to model recursive
interactions. Moreover, we prove the decidability of equivalence,
satisfiability, and validity of first-order extended interaction logic
formulas, and provide several examples of formulas describing well-known
architectures. We show the robustness of our theory by effectively extending
our results for parametric weighted architectures. For this, we study the
weighted counterparts of our logics over a commutative semiring, and we apply
them for modelling the quantitative aspects of concrete architectures. Finally,
we prove that the equivalence problem of weighted first-order extended
interaction logic formulas is decidable in a large class […]