We describe quantum circuits generating four-qubit maximally entangled states, the amount of entanglement being quantified by using the absolute value of the Cayley hyperdeterminant as an entanglement monotone. More precisely we show that this type of four-qubit entangled states can be obtained by the action of a family of $\mathtt{CNOT}$ circuits on some special states of the LU orbit of the state $|0000\rangle$ .

We introduce a new concept of continuity of posets, called θ-continuity. Topological characterizations of θ-continuous posets are put forward. We also present two types of dcpo-completion of posets which are Dθ-completion and Ds2-completion. Connections between these notions of continuity and dcpo-completions of posets are investigated. The main results are (1) a poset P is θ-continuous iff its θ-topology lattice is completely distributive iff it is a quasi θ-continuous and meet θ-continuous poset iff its Dθ-completion is a domain; (2) the Dθ-completion of a poset B is isomorphic to a domain L iff B is a θ-embedded basis of L; (3) if a poset P is θ-continuous, then the Dθ-completion Dθ(P) is isomorphic to the round ideal completion RI(P, ≪θ).

We show that a measurement $\mu$ on a continuous dcpo $D$ extends to a measurement $\skew3\bar{\mu}$ on the convex powerdomain ${\mathbf C} D$ iff it is a Lebesgue measurement. In particular, $\ker\mu$ must be metrisable in its relative Scott topology. Moreover, the space $\ker\skew3\bar{\mu}$ in its relative Scott topology is homeomorphic to the Vietoris hyperspace of $\ker\mu$, that is, the space of non-empty compact subsets of $\ker\mu$ in its Vietoris topology – the topology induced by any Hausdorff metric. This enables one to show that Hutchinson's theorem holds for any finite set of contractions on a domain with a Lebesgue measurement. Finally, after resolving the existence question for Lebesgue measurements on countably based domains, we uncover the following relationship between classical analysis and domain theory: for an $\omega$-continuous dcpo $D$ with $\max(D)$ regular, the Vietoris hyperspace of $\max(D)$ embeds in $\max({\mathbf C} D)$ as the kernel of a measurement on ${\mathbf C} D$.

The three body Coulomb problem is one of the oldest unsolved problems of theoretical physics, and holds a variety of puzzling problems, on both the classical and quantum levels. It is of paradigmatic importance since it bears dynamical and spectral features that establish a link between single and many-particle dynamics, with the absolute minimum of ingredients. When additionally exposed to a time-periodic external perturbation, the effective dimension of the classical phase space as well as of Hilbert space increases dramatically. This gives rise to new phenomena, which stimulate research in such remote areas as mathematical physics, semiclassics and intense-field laser–matter interactions. In the present review, we illustrate how these different areas are interconnected by three interacting particles.

We propose an abstract notion of a type theory to unify the semantics of various type theories including Martin–Löf type theory, two-level type theory, and cubical type theory. We establish basic results in the semantics of type theory: every type theory has a bi-initial model; every model of a type theory has its internal language; the category of theories over a type theory is bi-equivalent to a full sub-2-category of the 2-category of models of the type theory.

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).

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.

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.

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.

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.

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.

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.

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.

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 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.

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).