The notions of weak Cartesian closed category and very weak CCC are introduced by dropping the extensionality (and the naturality) requirements in the adjunction defining the closed structure of a CCC. A number of specific examples of these categories are given. The weak notions are shown to be equivalent from both the semantic and syntactic standpoint to the typed non-extensional lambda-calculus and to the typed Combinatory Logic, extended with surjective pairs. Type-free models are characterized as reflexive objects in wCCCs. Finally, categorical models for the second-order non-extensional calculus are defined, by introducing a simple generalization of the notion of PL-category.

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.

We consider the structure of the intestinal epithelial tissue and of cell–cell junctions as the biological model inspiring a new class of P systems. First we define the concept of cell polarity, a formal property derived from epithelial cells, which present morphologically and functionally distinct regions of the plasma membrane. Then we show two preliminary results for this new model of computation: on the theoretical side, we show that P systems with cell polarity are computationally (Turing) complete; on the modelling side, we show that the transepithelial movement of glucose from the intestinal lumen into the blood can be described by such a formal system. Finally, we define tissue P systems with cell polarity, where each cell has fixed connections to the neighbouring cells and to the environment, according to both the cell polarity and specific cell–cell junctions.

It is interesting to note that the very first papers related to isomorphism of types were written before the notion itself appeared. Their subjects were the study of equality of terms defined on numbers, the isomorphism of objects in certain categories and the invertibility of $\lambda$-terms, but not the isomorphism of types ‘as such’. One may cite the so-called ‘Tarsky High School Algebra Problem’: whether all identities between terms built from $+, x, \uparrow$, variables and constants are derivable from basic ‘high school equalities’, like $(xy)^z=x^zy^z$. The earliest publications related to this problem date from the 1940s, cf. Birkhoff (1940) – an extensive bibliography may be found in Burris and Yeats (2002).

This paper analyses the interpretation of mathematical entities in the formalisations of languages. Four case studies are considered, covering both denotational and axiomatic approaches. We argue that the usual interpretation consists of direct statements about the language concepts and, occasionally, about the real world; some problems of this approach are discussed. Applying results from philosophical studies into the structure of scientific theories, we propose an alternative interpretation of mathematical entities as statements defining constructed concepts, which can be employed in turn as theoretical models of the language concepts and the world. Though this approach requires us to write hypotheses claiming some similarity between the models and the represented subjects, we reason that it is more adequate for formalising certain languages.

We begin by reviewing the major results dealing with the structure of the cl-degrees, and then focus on the method of the Yu–Ding Theorem, which is an important result in this area. By strengthening the Yu–Ding procedure, we construct a cl-cuppable cl-degree of c.e. sets.

We propose a general theory of partial n-place operations based solely on the primitive notion of the application of a (possibly partial) operation to n objects. This theory is strongly selfdescriptive in that the fundamental manipulations of operations, that is, application, composition, abstraction, union, intersection and so on, are themselves internal operations. We give several applications of this theory, including implementations of partial n-ary λ-calculus, and other operation description languages. We investigate the issue of extensionality and give weakly extensional models of the theory.

There has been an increased interest in the decision problems for linear logic and its fragments. Here, we give a fully self-contained, easy-to-follow, but fully detailed, direct and constructive proof of the undecidability of a very simple Horn-like fragment of linear logic, which is accessible to a wide range of people. Namely, we show that there is a direct correspondence between terminated computations of a Minsky machine M and cut-free linear logic derivations for a Horn-like sequent of the form

\begin{equation*} \bang{\Phi_M},\ l_1 \vdash l_0, \end{equation*}

\begin{equation*} (l \llto l'),\ \ ((l\otimes r) \llto l'),\ \ (l\llto (r\otimes l')),\ \ and \ \ (l\llto (l'\oplus l'')), \end{equation*}

Neither negation, nor &, nor constants, nor embedded implications/bangs are used here.

Furthermore, our particular correspondence constructed above provides decidability for each of the Horn-like fragments whenever we confine ourselves to any two forms of the above Horn-like implications, along with the complexity bounds that come from the proof.

Given the complexity of cyber-physical systems (CPS), such as swarms of drones, often deviations, from a planned mission or protocol, occur which may in some cases lead to harm and losses. To increase the robustness of such systems, it is necessary to detect when deviations happen and diagnose the cause(s) for a deviation. We build on our previous work on soft agents, a formal framework based on using rewriting logic for specifying and reasoning about distributed CPS, to develop methods for diagnosis of CPS at design time. We accomplish this by (1) extending the soft agents framework with Fault Models; (2) proposing a protocol specification language and the definition of protocol deviations; and (3) development of workflows/algorithms for detection and diagnosis of protocol deviations. Our approach is partially inspired by existing work using counterfactual reasoning for fault ascription. We demonstrate our machinery with a collection of experiments.

A defining feature of quantum mechanics is that it allows systems to exist in a superposition of different eigenstates of certain observables such as position or spin. However, superpositions of other quantities such as mass or charge are not seen in nature. It is thought that this disparity is partly due to the fact that it is much easier to carry out interference experiments for certain observables than others. Here we present an interferometry scheme that should allow us to observe interference between the vacuum and a single photon or atom. We begin by presenting a scheme for a Hadamard gate that operates in the Fock state basis and then show how, by creating an interferometer from two such gates, interference between a single particle and the vacuum could indeed be observed. This would provide evidence of a superposition of different particle numbers.

This paper shows how PILLY (Polymorphic Intuitionistic/Linear Lambda calculus with a fixed point combinator Y) with parametric polymorphism can be used as a metalanguage for domain theory, as originally suggested by Plotkin more than a decade ago. Using Plotkin's encodings of recursive types in PILLY, we show how parametric models of PILLY give rise to models of FPC, which is a simply typed lambda calculus with recursive types and an operational call-by-value semantics, reflecting a classical result from domain theory. Essentially, this interpretation is an interpretation of intuitionistic logic into linear logic first discovered by Girard, which in this paper is extended to deal with recursive types. Of particular interest is a model based on ‘admissible’ pers over a reflexive domain, the theory of which can be seen as a domain theory for (impredicative) polymorphism. We show how this model gives rise to a parametric and computationally adequate model of PolyFPC, an extension of FPC with impredicative polymorphism. This is to the author's knowledge the first denotational model of a non-linear language with parametric polymorphism and recursive types.

Pick's Theorem relates the area of a simple polygon with vertices at integer lattice points to the number of lattice points in its inside and boundary. We describe a formal proof of this theorem using the HOL Light theorem prover. As sometimes happens for highly geometrical proofs, the formalisation turned out to be more work than initially expected. The difficulties arose mostly from formalising the triangulation process for an arbitrary polygon.

It is known that if K is a compact subset of the (separable complete) metric Urysohn space (${\mathbb U}$, d) and f is a Katětov function on the subspace K of (${\mathbb U}$, d), then there is z ∈ ${\mathbb U}$ such that d(z, x) = f(x) for all x ∈ K.

Answering a question of Normann, we show in this article that the supseparable bicomplete q-universal ultrahomogeneous T0-quasi-metric space (q${\mathbb U}$, D) recently discussed by the authors satisfies a similar property for Katětov function pairs on subsets that are compact in the associated metric space (q${\mathbb U}$, Ds).

This paper reports on an investigation into the role of shuffling and concatenation in the theory of graph drawing. A simple syntactic description of these and related operations is proved to be complete in the context of finite partial orders, and as general as possible. An explanation based on this result is given for a previously investigated collapse of the permutohedron into the associahedron, and for collapses into other less familiar polyhedra, including the cyclohedron. Such polyhedra have been considered recently in connection with the notion of tubing, which is closely related to tree-like finite partial orders, which are defined simply here and investigated in detail. Like the associahedron, some of these other polyhedra are involved in categorial coherence questions, which will be treated elsewhere.

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.

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.

In this paper we introduce relative formal topology so that we can deal constructively with the closed subsets of a topological space as well as with the open ones. In fact, within standard formal topology, the cover relation allows the definition of the formal opens, which are supposed to act as the formal counterparts of the open subsets, and within balanced formal topology, the binary positivity predicate allows the definition of the formal closed subsets, which are supposed to act as the formal counterparts of the closed subsets. However, these approaches are only fully satisfactory (according to the criterion introduced by the author in Valentini (2005)) if we can provide an adequate formalisation of the cover relation and the positivity predicate. But current formalisations fail in this respect since some intuitionistically valid relations between the open and closed subsets of a concrete topological space cannot be expressed. Our central result is that we can solve this problem through a generalisation of the standard cover relation together with a binary positivity predicate satisfying the positivity axiom.

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.

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.