The goal of this paper is to prove coherence results with respect to relational graphs for monoidal monads and comonads, that is, monads and comonads in a monoidal category such that the endofunctor of the monad or comonad is a monoidal functor (this means that it preserves the monoidal structure up to a natural transformation that need not be an isomorphism). These results are proved first in the absence of symmetry in the monoidal structure, and then with this symmetry. The monoidal structure is also allowed to be given with finite products or finite coproducts. Monoidal comonads with finite products axiomatise a plausible notion of equality of deductions in a fragment of the modal logic S4.

Models of dependent type theories are contextual categories with some additional structure. We prove that if a theory T has enough structure, then the category T-Mod of its models carries the structure of a model category. We also show that if T has Σ-types, then weak equivalences can be characterized in terms of homotopy categories of models.

This paper clarifies that linear implication defines a branching-time preorder, preserved in all contexts, when used to compare embeddings of process in non-commutative logic. The logic considered is a first-order extension of the proof system BV featuring a de Morgan dual pair of nominal quantifiers, called BV1. An embedding of π-calculus processes as formulae in BV1 is defined, and the soundness of linear implication in BV1 with respect to a notion of weak simulation in the π -calculus is established. A novel contribution of this work is that we generalise the notion of a ‘left proof’ to a class of formulae sufficiently large to compare embeddings of processes, from which simulating execution steps are extracted. We illustrate the expressive power of BV1 by demonstrating that results extend to the internal π -calculus, where privacy of inputs is guaranteed. We also remark that linear implication is strictly finer than any interleaving preorder.

We define a construction operation on hypergraphs based on a colimit and show that its expressiveness is equal to the graph expressions of Bauderon and Courcelle. We also demonstrate that by closing a set of rewrite rules under graph construction we obtain a notion of rewriting equivalent to the double-pushout approach of Ehrig. The usefulness of our approach for the compositional modelling of concurrent systems is then demonstrated by giving a semantics of process graphs (corresponding to a process calculus with mobility) and of Petri nets. We introduce on the basis if a hypergraph construction, a method for the static analysis of process graphs, related to type systems.

We present a novel robust control scheme that deals with multi-body spacecraft attitude tracking problems. The control scheme consists of a radial basis function network (RBFN) and a robust controller. By using the finite time convergence property of the terminal sliding mode (TSM), we derive a new online learning algorithm for updating all the parameters of the RBFN that ensures the RBFN has fast approximation for the parameter uncertainties and external disturbances. We design a robust controller to compensate RBFN approximation errors and realise the anticipative stability and performance properties. We can also achieve closed-loop system stability using Lyapunov stability theory.

No detailed knowledge of the non-linear dynamics of the spacecraft is required at any point in the entire design process, and the proposed robust scheme is simple and effective and can be applied to more complex systems. Simulation results demonstrate the good tracking characteristics of the proposed control scheme in the presence of inertial uncertainties and external disturbances.

We present a comparative study of four product operators on weighted languages: (i) the convolution, (ii) the shuffle, (iii) the infiltration and (iv) the Hadamard product. Exploiting the fact that the set of weighted languages is a final coalgebra, we use coinduction to prove that an operator of the classical difference calculus, the Newton transform, generalises from infinite sequences to weighted languages. We show that the Newton transform is an isomorphism of rings that transforms the Hadamard product of two weighted languages into their infiltration product, and we develop various representations for the Newton transform of a language, together with concrete calculation rules for computing them.

We propose a new framework for representing logics, called LF+, which is based on the Edinburgh Logical Framework. The new framework allows us to give, apparently for the first time, general definitions that capture how well a logic has been represented. These definitions are possible because we are able to distinguish in a generic way that part of the LF+ entailment corresponding to the underlying logic. This distinction does not seem to be possible with other frameworks. Using our definitions, we show that, for example, natural deduction first-order logic can be well-represented in LF+, whereas linear and relevant logics cannot. We also show that our syntactic definitions of representation have a simple formulation as indexed isomorphisms, which both confirms that our approach is a natural one and provides a link between type-theoretic and categorical approaches to frameworks.

We consider the propositional modal mu-calculus, a logic proposed by Kozen in 1983. In this logic two operators μ and v are present, which express the least and greatest fixpoints of monotone operators on sets. Bradfield in 1998 proved for any n the existence of a mu-calculus formula that requires n alternations of μ and v. In this paper we consider the particular case n = 3 and we exhibit a new formula requiring 3 alternations. Our proof is independent of the technique of Bradfield, and is based on a new kind of game on infinite trees.

We present a method for constructing from a given domain representation of a space X with underlying domain D, a domain representation of a subspace of compact subsets of X where the underlying domain is the Plotkin powerdomain of D. We show that this operation is functorial over a category of domain representations with a natural choice of morphisms. We study the topological properties of the space of representable compact sets and isolate conditions under which all compact subsets of X are representable. Special attention is paid to admissible representations and representations of metric spaces.

Several relational program logics have been introduced for integrating reasoning about relational properties of programs and measurement of quantitative difference between computational effects. Toward a general framework for such logics, in this paper, we formalize the concept of quantitative difference between computational effects as divergences on monads, then develop a relational program logic called approximate computational relational logic (acRL for short). It supports generic computational effects and divergences on them. The semantics of the acRL is given by graded strong relational liftings constructed from divergences on monads. We derive two instantiations of the acRL: (1) for the verification of various kinds of differential privacy of higher-order functional probabilistic programs and (2) the other for measuring difference of distributions of cost between higher-order functional probabilistic programs with a cost counting operator.

We show that the problem of whether a finite set of regular-linear axioms defines a rigid theory is undecidable.

Rewriting notions like termination, normal forms and confluence can be described in an abstract way referring to rewriting only as a binary relation. Several theorems on rewriting, like Newman's lemma, can be proved in this abstract setting. For investigating possible generalizations of such theorems, it is fruitful to have counterexamples showing that particular generalizations do not hold. In this paper, we develop a technique to find such counterexamples fully automatically, and we describe our tool Carpa that follows this technique. The basic idea is to fix the number of objects of the abstract rewrite system, and to express the conditions and the negation of the conclusion in a satisfiability (SAT) formula, and then call a current SAT solver. In case the formula turns out to be satisfiable, the resulting satisfying assignment yields a counterexample to the encoded property. We give several examples of finite abstract rewrite systems having remarkable properties that are found in this way fully automatically.

Wind power projects face an uncertain external environment, they are complex projects in themselves and the capabilities of the designers, erectors and operators are limited. All this makes the identification of investment risks for wind power projects extremely complicated. In this paper, we propose a method for identifying the investment risk scientifically and accurately using a back propagation (BP) neural network. Specifically, we propose a hybrid wavelet transform fuzzy BP neural network (WT-FBPNN) optimisation model based on the construction of a risk evaluating index system. This improved model can not only exploit the time frequency localisation characteristic of wavelet transforms (WT), but also enhance the fit precision and algorithm convergence speed. The simulation results show that this model is reliable, and that this method of identifying the investment risk of wind power projects is feasible.

In this paper we present a semantics-based framework for analysing the quantitative behaviour of programs with respect to resource usage. We start from an operational semantics in which costs are modelled using a dioid structure. The dioid structure of costs allows the definition of the quantitative semantics as a linear operator. We then develop a theory of approximation of such a semantics, which is akin to what is offered by the theory of abstract interpretation for analysing qualitative properties, in order to compute effectively global cost information from the program. We focus on the notion of long-run cost, which models the asymptotic average cost of a program. The abstraction of the semantics has to take two distinct notions of order into account: the order on costs and the order on states. We prove that our abstraction technique provides a correct approximation of the concrete long-run cost of a program.

The aim of this paper is to provide mathematical foundations of a graph transformation language, called UnCAL, using categorical semantics of type theory and fixed points. About 20 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.

In order to make UnCAL more flexible and fruitful for further extensions and applications, in this paper, we give a more conceptual understanding of UnCAL using categorical semantics. Our general interest of this paper is to clarify what is the algebra of UnCAL. Thus, we give an equational axiomatisation and categorical semantics of UnCAL, both of which are new. We show that the axiomatisation is complete for the original bisimulation semantics of UnCAL. Moreover, we provide a clean characterisation of the computation mechanism of UnCAL called ‘structural recursion on graphs’ using our categorical semantics. We show a concrete model of UnCAL given by the λG-calculus, which shows an interesting connection to lazy functional programming.

Robinson’s unification algorithm can be identified as the underlying machinery of both C. Meredith’s rule D (condensed detachment) in propositional logic and of the construction of principal types in lambda calculus and combinatory logic. In combinatory logic, it also plays a crucial role in the construction of Meyer, Bunder & Powers’ Fool’s model. This paper now considers pattern matching, the unidirectional variant of unification, as a basis for logical inference, typing, and a very simple and natural model for untyped combinatory logic. An analysis of the new typing scheme will enable us to characterize a large class of terms of combinatory logic which do not change their principal type when being weakly reduced. We also consider the question whether the major or the minor premisse should be used as the fixed pattern.

The homotopical Squier’s theorem relates rewriting properties of a presentation of a monoid with homotopical invariants of this monoid. This theorem has since been extended by Guiraud and Malbos, yielding a so-called polygraphic resolution of a monoid starting from a presentation with suitable rewriting properties. In this article, we argue that cubical categories are a more natural setting in which to express and possibly extend Guiraud and Malbos construction. As a proof-of-concept, we give a new proof of Squier’s homotopical theorem using cubical categories.

This paper gives a new proof of confluence for Carraro and Guerrieri’s call-by-value lambda calculus λ v σ with permutation rules. We adapt the compositional Z theorem to λ v σ .

Hoare Logic has a long tradition in formal verification and has been continuously developed and used to verify a broad class of programs, including sequential, object-oriented, and concurrent programs. Here we focus on partial and total correctness assertions within the framework of Hoare logic and show that a comprehensive categorical analysis of its axiomatic semantics needs the languages of indexed and fibered category theory. We consider Hoare formulas with local, finite contexts, of program and logical variables. The structural features of Hoare assertions are presented in an indexed setting, while the logical features of deduction are modeled in the fibered one.

In model transformations, where source models are automatically translated into target models or code, termination is necessary for the transformation to be well defined. There are a number of specific termination criteria that can be used when specifying model transformations by graph transformation, though termination is undecidable in general. Unfortunately, and particularly for large and heterogeneous specifications, it is often not possible to use a single termination criterion. In this paper, we propose an approach that applies different criteria to suitable subsets of rules so that termination can be shown locally using the most suitable technique for each subset. Global termination then follows if certain causal dependencies between rules in different subsets are acyclic. The theory is developed at the level of typed attributed graphs, and is motivated and illustrated by a case study translating UML activity diagrams to CSP.