In this paper, we introduce the notion of expansion tree for linear logic. As in Miller's original work, we have a shallow reading of an expansion tree that corresponds to the conclusion of the proof, and a deep reading which is a formula that can be proved by propositional rules. We focus our attention to MLL2, and we also present a deep inference system for that logic. This allows us to give a syntactic proof to a version of Herbrand's theorem.

Inspired by the work of S. Kaplan on positive/negative conditional rewriting, we investigate initial semantics for algebraic specifications with Gentzen formulas. Since the standard initial approach is limited to conditional equations (i.e. positive Horn formulas), the notion of semi-initial and quasi-initial algebras is introduced, and it is shown that all specifications with (positive) Gentzen formulas admit quasi-initial models.

The whole approach is generalized to the parametric case where quasi-initiality generalizes to quasi-freeness. Since quasi-free objects need not be isomorphic, the persistency requirement is added to obtain a unique semantics for many interesting practical examples. Unique persistent quasi-free semantics can be described as a free construction if the homomorphisms of the parameter category are suitably restricted. Furthermore, it turns out that unique persistent quasi-free semantics applies especially to specifications where the Gentzen formulas can be interpreted as hierarchical positive/negative conditional equations. The data type constructor of finite function spaces is used as an example that does not admit a correct initial semantics, but does admit a correct unique persistent quasi-initial semantics. The example demonstrates that the concepts introduced in this paper might be of some importance in practical applications.

Concrete computing machines, either sequential or concurrent, rely on an intimate relationship between computation and time. We recall the general characteristic properties of physical time and of present realisations of computing systems. We emphasise the role of computing interferences, that is, the necessity of avoiding them in order to give a causal implementation to logical operations. We compare synchronous and asynchronous systems, and give a brief survey of some methods used to deal with computing interferences. Using a graphic representation, we show that synchronous and asynchronous circuits reflect the same opposition as the Newtonian and relativistic causal structures for physical space-time.

We present a discussion concerning the opposition between discreteness and the continuum in quantum mechanics. In particular, it is shown that this duality was not restricted to the early days of the theory, but remains current, and features different aspects of discretisation. In particular, the discreteness of quantum mechanics is key for quantum information and quantum computation. We propose a conclusion involving a concept of completeness linking discreteness and the continuum.

In this paper, I discuss the extent to which Kolmogorov drew upon von Mises' work in addressing the problem of why probability is applicable to events in the real world, which I refer to as the problem of the applicability of probability, or the applicability problem for short. In particular, I highlight the role of randomness in Kolmogorov's account, and I argue that this role differs significantly from the role that randomness plays in von Mises' account.

The paper defines and studies the genus of finite state deterministic automata (FSA) and regular languages. Indeed, an FSA can be seen as a graph for which the notion of genus arises. At the same time, an FSA has a semantics via its underlying language. It is then natural to make a connection between the languages and the notion of genus. After we introduce and justify the the notion of the genus for regular languages, the following questions are addressed. First, depending on the size of the alphabet, we provide upper and lower bounds on the genus of regular languages: we show that under a relatively generic condition on the alphabet and the geometry of the automata, the genus grows at least linearly in terms of the size of the automata. Second, we show that the topological cost of the powerset determinization procedure is exponential. Third, we prove that the notion of minimization is orthogonal to the notion of genus. Fourth, we build regular languages of arbitrary large genus: the notion of genus defines a proper hierarchy of regular languages.

In this paper we prove that every non-zero Δ20e-degree is cuppable to 0e′ by a 1-generic Δ20e-degree (and is thus low and non-total), and that every non-zero ω-c.e. e-degree is cuppable to 0e′ by an incomplete 3-c.e. e-degree.

Consider the first-order theory of a category.d It has a sort of objects, and a sort of arrows (so we may think of it as a small category). We show that, assuming the principle of unique substitutions, the setoids inside a type theoretic universe provide a model for this first-order theory. We also show that the principle of unique substitutions is not derivable in type theory, but that it is strictly weaker than the principle of unique identity proofs.

Directed paths have been used by several authors to describe concurrent executions of a program. Spaces of directed paths in an appropriate state space contain executions with all possible legal schedulings. It is interesting to investigate whether one obtains different topological properties of such a space of executions if one restricts attention to schedulings with “nice” properties, e.g. involving synchronisations. This note shows that this is not the case, i.e. that one may operate with nice schedulings without inflicting any harm. Several of the results in this note had previously been obtained by Ziemiański in Ziemiański (2017. Applicable Algebra in Engineering, Communication and Computing28 497–525; 2020a. Journal of Applied and Computational Topology4 (1) 45–78). We attempt to make them accessible for a wider audience by giving an easier proof for these findings by an application of quite elementary results from algebraic topology; notably the nerve lemma.

In this paper, we discuss the crucial but little-known fact that, as Kolmogorov himself claimed, the mathematical theory of probabilities cannot be applied to factual probabilistic situations. This is because it is nowhere specified how, for any given particular random phenomenon, we should construct, effectively and without circularity, the specific and stable distribution law that gives the individual numerical probabilities for the set of possible outcomes. Furthermore, we do not even know what significance we should attach to the simple assertion that such a distribution law “exists”. We call this problem Kolmogorov's aporia†.

We provide a solution to this aporia in this paper. To do this, we first propose a general interpretation of the concept of probability on the basis of an example, and then develop it into a non-circular and effective general algorithm of semantic integration for the factual probability law involved in a specific factual probabilistic situation. The development of the algorithm starts from the fact that the concept of probability, unlike a statistic, does not apply to naturally pre-existing situations but is a conceptual artefact that ensures, locally in space and time, a predictability that is more stable and definite than that permitted by primary statistical data.

The algorithm, which is constructed within a method of relativised conceptualisation, leads to a probability distribution expressed in rational numbers and involving a sort of quantification of the factual concept of probability. Furthermore, it also provides a definite meaning to the simple assertion that a factual probability law exists. We also show that the semantic integration algorithm is compatible with the weak law of large numbers.

The results we give provide a complete solution to Kolmogorov's aporia. They also define a concept of probability that is explicitly organised into a semantic, epistemological and syntactic whole. In a broader context, our results can be regarded as a strong, pragmatic and operational specification of Karl Popper's propensity interpretation of probabilities.

This paper describes a family of logics whose categorical semantics is based on functors with structure rather than on categories with structure. This allows the consideration of logics that contain possibly distinct logical subsystems whose interactions are mediated by functorial mappings. For example, within one unified framework, we shall be able to handle logics as diverse as modal logic, ordinary linear logic, and the ‘noncommutative logic’ of Abrusci and Ruet, a variant of linear logic that has both commutative and noncommutative connectives.

Although this paper will not consider in depth the categorical basis of this approach to logic, preferring instead to emphasise the syntactic novelties that it generates in the logic, we shall focus on the particular case when the logics are based on a linear functor, in order to give a definite presentation of these ideas. However, it will be clear that this approach to logic has considerable generality.

Given a program, a quotient can be obtained from it by deleting zero or more statements. The field of program slicing is concerned with computing a quotient of a program that preserves part of the behaviour of the original program. All program slicing algorithms take account of the structural properties of a program, such as control dependence and data dependence, rather than the semantics of its functions and predicates, and thus work, in effect, with program schemas. The dynamic slicing criterion of Korel and Laski requires only that program behaviour is preserved in cases where the original program follows a particular path, and that the slice/quotient follows this path. In this paper we formalise Korel and Laski's definition of a dynamic slice as applied to linear schemas, and also formulate a less restrictive definition in which the path through the original program need not be preserved by the slice. The less restrictive definition has the benefit of leading to smaller slices. For both definitions, we compute complexity bounds for the problems of establishing whether a given slice of a linear schema is a dynamic slice and whether a linear schema has a non-trivial dynamic slice, and prove that the latter problem is NP-hard in both cases. We also give an example to prove that minimal dynamic slices (whether or not they preserve the original path) need not be unique.

In this paper, we investigate splitting and non-splitting properties in the Ershov difference hierarchy, in which area major contributions have been made by Barry Cooper with his students and colleagues. In the first part of the paper, we give a brief survey of his research in this area and discuss a number of related open questions. In the second part of the paper, we consider a splitting of 0′ with some additional properties.

This paper addresses the H∞ state feedback stabilisation problem for networked control systems (NCSs) in the presence of time delays and packet losses. By introducing the concept of an effective sensor packet, the NCS is transformed into a new discrete-time switched model, where the parameters have a clear physical meaning and can be easily determined. In this framework, we derive the stability conditions of the closed-loop system in the H∞ sense, and also provide the corresponding H∞ stabilising controller design method. Finally, we give simulation and experimental results to demonstrate the effectiveness of the proposed approaches.

We study the functorial characterisation of bisimulation-based equivalences over a categorical model of labelled trees. We show that in a setting where all labels are visible, strong bisimilarity can be characterised in terms of enriched functors by relying on the reflection of paths with their factorisations. For an enriched functor F, this notion requires that a path (an internal morphism in our framework) π going from F(A) to C corresponds to a path p going from A to K, with F(K) = C, such that every possible factorisation of π can be lifted in an appropriate factorisation of p. This last property corresponds to a Conduché property for enriched functors, and a very rigid formulation of it has been used by Lawvere to characterise the determinacy of physical systems. We also consider the setting where some labels are not visible, and provide characterisations for weak and branching bisimilarity. Both equivalences are still characterised in terms of enriched functors that reflect paths with their factorisations: for branching bisimilarity, the property is the same as the one used to characterise strong bisimilarity when all labels are visible; for weak bisimilarity, a weaker form of path factorisation lifting is needed. This fact can be seen as evidence that strong and branching bisimilarity are strictly related and that, unlike weak bisimilarity, they preserve process determinacy in the sense of Milner.

We formalize in Constructive Type Theory the Lambda Calculus in its classical first-order syntax, employing only one sort of names for both bound and free variables, and with α-conversion based upon name swapping. As a fundamental part of the formalization, we introduce principles of induction and recursion on terms which provide a framework for reproducing the use of the Barendregt Variable Convention as in pen-and-paper proofs within the rigorous formal setting of a proof assistant. The principles in question are all formally derivable from the simple principle of structural induction/recursion on concrete terms. We work out applications to some fundamental meta-theoretical results, such as the Church–Rosser Theorem and Weak Normalization for the Simply Typed Lambda Calculus. The whole development has been machine checked using the system Agda.

Lambda-calculi with vectorial structures have been studied in various ways, but their semantics remain largely uninvestigated. The main contribution of this paper is to provide a categorical framework for the semantics of such algebraic lambda-calculi. We first develop a categorical analysis of a general simply typed lambda-calculus endowed with the structure of a module. We study the problems arising from the addition of a fixed-point combinator and show how to modify the equational theory to solve them. The categorical analysis carries nicely over to the modified language. We provide various concrete models for both the case without fixpoints and for the case with them.

In this work we show how some useful reductions known from ordinary intuitionistic propositional calculus can be modified for Intuitionistic Linear Logic (without modalities). The main reductions we consider are: (1) the reduction of the depth of formulas in the sequents by addition of new variables, and (2) the elimination of linear disjunction, tensor and constant F. Both transformations preserve deducibility, that is, a transformed sequent is deducible if and only if the initial one was deducible. The size of the sequent grows linearly in case (1) and ≤ On8 in case (2).

This paper is a part of the ongoing program of analysing the complexity of various problems in computable analysis in terms of the complexity of the associated index sets. In the framework of effectively enumerable topological spaces, we investigate the following question: given an effectively enumerable topological space whether there exists a computable numbering of all its computable elements. We present a natural sufficient condition on the family of basic neighbourhoods of computable elements that guarantees the existence of a principal computable numbering. We show that weakly-effective ω–continuous domains and the natural numbers with the discrete topology satisfy this condition. We prove weak and strong analogues of Rice's theorem for computable elements. Then, we construct principal computable numberings of partial majorant-computable real-valued functions and co-effectively closed sets and calculate the complexity of index sets for important problems such as root verification and function equality. For example, we show that, for partial majorant-computable real functions, the equality problem is Π11-complete.

We show how systems of session types can enforce interactions to take bounded time for all typable processes. The type system we propose is based on Lafont's soft linear logic and is strongly inspired by recent works about session types as intuitionistic linear logic formulas. Our main result is the existence, for every typable process, of a polynomial bound on the length of reduction sequences starting from it and on the size of its reducts.