Abstract Whether the upper F upper S F S $FS$ -domain of closed discs in the plane is a retract of a bifinite domain is a long-standing open problem in domain theory, which has been stated in textbooks and several other references. In this paper, we give a positive answer to this question. As preparation, we present some rules for the inductive construction of a Plotkin-poset. Then, we inductively construct a bottomed Plotkin-poset based on closed circular rings in the plane with rational radii and rational centers. Since every element in this bottomed Plotkin-poset is compact, it follows that the ideal completion of this Plotkin-poset is a bifinite domain. Furthermore, an embedding-retraction pair is established between the domain of closed discs in the plane and this bifinite domain.
We will place Zawadowski's work on linguistic semantics in the historical context of the development of the field. Central to his linguistic work is the combination of model theoretic techniques in set theory with type theoretic techniques combined with a continuation semantics. This leads to elegant general treatments of well-known puzzles in the analysis of meaning in natural languages.
We introduce in this paper a definition of (non-necessarily positive) opetopes where faces are organised in a poset. Then, we show that this description is equivalent to that given in terms of constellations by Kock et al. (2010).
Davidsonian event semantics (Davidson 1967) is widely accepted as a powerful framework for formal semantics. It has brought about many benefits in semantic construction, which may be summarised into two categories: one is to provide a satisfactory solution to a seemingly intractable problem of variable polyadicity, and the other consists of those benefits that come from the availability of the entities called events that correspond to verb actions. This paper provides an analysis of event semantics from a general viewpoint of dependent type theory. First, it is shown that the problem of variable polyadicity can be solved by means of dependent typing, without the employment of events. To do this, we only extend the simple type theory with two type constructors and the resulting semantic definitions not only allow variable polyadicity as desired but also obtain logical inferences as expected. We shall discuss why the solution is natural from a type-theoretical point of view (as compared with that in set theory). We then discuss that most (if not all) of the other benefits of event semantics may already be obtained by alternative means without introducing events as ontological entities. To this end, we consider the evidence for event semantics discussed by Parsons (1990), focusing on two particular aspects: event talks and perception words, showing that the former is mostly concerned with timing, and the latter can be dealt with a special case without introducing events in general.
It is well known that over Heyting arithmetic with finite types, the effective principle of the formal Church thesis, stating that all number-theoretic functional relations are computable, is inconsistent with Brouwer's intuitionistic principles on the continuum, in particular, the fan theorem. Here, we build two arithmetic quasi-toposes, validating on the one hand Brouwer's continuity principles, including the Fan theorem, and on the other hand, a restricted form of Church's Thesis, called the Type-theoretic Church Thesis and written $ extsf{TCT}$ , expressing that all morphisms of the considered quasi-topos are computable. One quasi-topos is constructed by formalizing the category of assemblies $\mathbf{Asm}$ within Hyland's effective topos using intuitionistic Zermelo-Fraenkel set theory $\mathbf{IZF}$ extended with Brouwer's continuity principles as our meta-theory. The other quasi-topos is obtained as an elementary quotient completion in the same intuitionistic meta-theory. While in previous work by the first author with F. Pasquali and G. Rosolini, it has been shown that these two quasi-toposes are equivalent when working within the classical $\mathbf{ZFC}$ set theory; here, we show that this is no longer the case when working within $\mathbf{IZF}$ . We also observe that the aforementioned inconsistency is resolved in such quasi-toposes by the non-validity of the axiom of unique choice on the natural numbers and that no non-trivial topos can validate the effective principle $ extsf{TCT}$ together with Brouwer's continuity principles altogether.
This paper studies two approaches to relativizing the notions of complete and precomplete numbering. The first one was introduced by Selivanov in the late 1980s, and it strengthens the standard definitions of complete and precomplete numbering. The second one was introduced by Badaev, Goncharov, and Sorbi in the early 2000s, and it is the full relativization of these two concepts. In the first part of the paper, we study how these two approaches differ from each other. In the second part, we study Mal'cev's object uniquely for the relativized complete numberings.
Manes (1998). Implementing Collection Classes with Monads. Mathematical Structures in Computer Science 8 (231-276) introduced the notion of a collection monad on the category of sets as a suitable semantics for collection types. The canonical example of collection monad is the finite powerset monad. In order to account for the algorithmic aspects, the category of sets should be replaced with categories whose arrows are maps computable by low-complexity algorithms. Inspired by realizability, we give a systematic way for constructing categories of small sets and low-complexity functions and define an analogue of collection monads on such categories.
We introduce semiframes (an algebraic structure) and investigate their duality with semitopologies (a topological one). Both semitopologies and semiframes are relatively recent developments, arising from a novel application of topological ideas to study decentralised computing systems. Semitopologies generalise topology by removing the condition that intersections of open sets are necessarily open. The motivation comes from identifying the notion of an actionable coalition in a distributed system - a set of participants with sufficient resources for its members to collaborate to take some action - with an open set, since just because two sets are actionable (have the resources to act) does not necessarily mean that their intersection is. We define notions of category and morphism and prove a categorical duality between (sober) semiframes and (spatial) semitopologies, and we investigate how key well-behavedness properties that are relevant to understanding decentralised systems transfer (or do not transfer) across the duality.
Domains exhibit a variety of different aspects, some are order theoretical, some are topological, some belong to topological algebra. In this paper, we introduce two kinds of congruence relations on domains: I-congruence relation and II-congruence relation on domains. We obtain that there is a bijection from the set of all kernel operators of domain $P$ preserving directed sups onto the set of all I-congruence relations on $P$ which exclude $P\times P$ . There is also a bijection from the set of all closure operators of domain $P$ preserving directed sups onto the set of all II-congruence relations on $P$ which exclude $P\times P$ . Furthermore, between two domains, we propose a new homomorphism called I-homomorphism and II-homomorphism, respectively. We conclude that the kernels of I-homomorphisms and II-homomorphisms between domains are I-congruence relations and II-congruence relations on domains, respectively. Therefore, we obtain the I-homomorphism and I-isomorphism theorems, as well as II-homomorphism and II-isomorphism theorems for domains. Besides, we give a positive answer to an open problem on homomorphisms and quotients of continuous semilattices posed by G. Gierz, et al.
We first introduce and investigate a new class of $T_0$ -spaces - strong $R$ -spaces, which are stronger than both $R$ -spaces and strongly well-filtered spaces. It is proved that any sup-complete poset equipped with the upper topology is a strong $R$ -space, and the Hoare power space of a $T_0$ -space is a strong $R$ -space. Hence, the upper topology on a sup-complete poset is strongly well-filtered, and the Hoare power space of a $T_0$ -space is strongly well-filtered, which answers two problems recently posed by Xu.
We present a dependently-typed cross-linguistic framework for analyzing the telicity and culminativity of events, accompanied by examples of using our framework to model English sentences. Our framework consists of two parts. In the nominal domain, we model the boundedness of noun phrases and its relationship to subtyping, delimited quantities, and adjectival modification. In the verbal domain, we define a dependent event calculus, modeling telic events as those whose undergoer is bounded, culminating events as telic events that achieve their inherent endpoint, and consider adverbial modification. In both domains, we pay particular attention to associated entailments. Our framework is defined as an extension of intensional Martin-L & ouml;f dependent type theory, and the rules and examples in this paper have been formalized in the Agda proof assistant.
Traditional category theory is typically based on set-theoretic principles and ideas, which are often non-constructive. An alternative approach to formalizing category theory is to use E-category theory, where hom sets become setoids. Our work reconsiders a third approach - P-category theory - from \v{C}ubri\'c et al. (1998) emphasizing a computational standpoint. We formalize in Rocq a modest library of P-category theory - where homs become subsetoids - and apply it to formalizing algorithms for normalization by evaluation which are purely categorical but, surprisingly, do not use neutral and normal terms. \v{C}ubri\'c et al. (1998) establish only a soundness correctness property by categorical means; here, we extend their work by providing a categorical proof also for a strong completeness property. For this we formalize the full universal property of the free Cartesian-closed category, which is not known to have been performed before. We further formalize a novel universal property of unquotiented simply typed lambda-calculus syntax and apply this to a proof of correctness of a categorical normalization by evaluation algorithm. We pair the overall mathematical development with a formalization in the Rocq proof assistant, following the principle that the formalization exists for practical computation. Indeed, it permits extraction of synthesized normalization programs that compute (long) beta-eta-normal forms of simply typed lambda-terms together with a derivation of beta-eta-conversion.
In this paper we show that the Day monoidal product generalises in a straightforward way to other algebraic constructions and partial algebraic constructions on categories. This generalisation was motivated by its applications in logic, for example in hybrid and separation logic. We use the description of the Day monoidal product using profunctors to show that the definition generalises to an extension of an arbitrary algebraic structure on a category to a pseudo-algebraic structure on a functor category. We provide two further extensions. First we consider the case where some of the operations on the category are partial, and second we show that the resulting operations on the functor category have adjoints (they are residuated).
Traced monoidal categories are used to model processes that can feed their outputs back to their own inputs, abstracting iteration. The category of finite dimensional Hilbert spaces with the direct sum tensor is not traced. But surprisingly, in 2014, Bartha showed that the monoidal subcategory of isometries is traced. The same holds for coisometries, unitary maps, and contractions. This suggests the possibility of feeding outputs of quantum processes back to their own inputs, analogous to iteration. In this paper, we show that Bartha's result is not specifically tied to Hilbert spaces, but works in any dagger additive category with Moore-Penrose pseudoinverses (a natural dagger-categorical generalization of inverses).
We introduce a geometric model of shallow multiplicative exponential linear logic (MELL) using the Hilbert scheme. Building on previous work interpreting multiplicative linear logic proofs as systems of linear equations, we show that shallow MELL proofs can be modeled by locally projective schemes. The key insight is that while multiplicative linear logic proofs correspond to equations between formulas, the exponential fragment of shallow proofs corresponds to equations between these equations. We prove that the model is invariant under cut-elimination by constructing explicit isomorphisms between the schemes associated to proofs related by cut-reduction steps. A key technical tool is the interpretation of the exponential modality using the Hilbert scheme, which parameterizes closed subschemes of projective space. We demonstrate the model through detailed examples, including an analysis of Church numerals that reveals how the Hilbert scheme captures the geometric content of promoted formulas. This work establishes new connections between proof theory and algebraic geometry, suggesting broader relationships between computation and scheme theory.
We show that, under certain assumptions, strongly finitary enriched monads are given by discrete enriched Lawvere theories. On the other hand, monads given by discrete enriched Lawvere theories preserve surjections.
Partial difference operators for a large class of functors between presheaf categories are introduced, extending our previous work on the difference operator to the multivariable case. These combine into the Jacobian profunctor that provides the setting for a lax chain rule. We introduce a functorial version of multivariable Newton series whose aim is to recover a functor from its iterated differences. Not all functors are recovered; however, we get a best approximation in the form of a left adjoint, and the induced comonad is idempotent. Its fixed points are what we call soft analytic functors, a generalization of the well-studied multivariable analytic functors.
This paper unites two research lines. The first involves finding categorical models of quantum programming languages with recursion and their type systems. The second line concerns the program of quantization of mathematical structures, which amounts to finding noncommutative generalizations (also called quantum generalizations) of these structures. Using a quantization method called discrete quantization, which essentially amounts to the internalization of structures in a category of von Neumann algebras and quantum relations, we find a noncommutative generalization of $\omega$ -complete partial orders (cpos), called quantum cpos. Cpos are central in domain theory and are widely used to construct categorical models of programming languages with recursion. We show that quantum cpos have similar categorical properties to cpos and are therefore suitable for the construction of categorical models for quantum programming languages, which is illustrated with some examples. Because of their noncommutative character, quantum cpos may form the backbone of a future quantum domain theory that provides structural methods for the denotational semantics of recursive quantum programming languages.
Martin-L & ouml;f's identity types provide a generic (albeit opaque) notion of identification or "equality" between any two elements of the same type, embodied in a canonical reflexive graph structure left parenthesis equals Subscript upper A Baseline comma bold r bold e bold f bold l right parenthesis ( = A , r e f l ) $(=_A, \mathbf{refl})$ on any type A. The miracle of Voevodsky's univalence principle is that it ensures, for essentially any naturally occurring structure in mathematics, that the resultant notion of identification is equivalent to the type of isomorphisms in the category of such structures. Characterisations of this kind are not automatic and must be established one-by-one; to this end, several authors have employed reflexive graphs and displayed reflexive graphs to organise the characterisation of identity types. We contribute reflexive graph lenses, a new family of intermediate abstractions lying between families of reflexive graphs and displayed reflexive graphs that simplifies the characterisation of identity types for complex structures. Every reflexive graph lens gives rise to a (more complicated) displayed reflexive graph, and our experience suggests that many naturally occurring displayed reflexive graphs arise in this way. Evidence for the utility of reflexive graph lenses is given by means of several case studies, including the theory of reflexive graphs itself as well as that of polynomial type operators. Finally, we exhibit an equivalence between the type of reflexive graph fibrations and the type of univalent reflexive graph lenses.
In this survey, we present in a unified way the categorical and syntactical settings of coherent differentiation introduced recently, which shows that the basic ideas of differential linear logic and of the differential lambda-calculus are compatible with determinism. Indeed, due to the Leibniz rule of the differential calculus, differential linear logic and the differential lambda-calculus feature an operation of addition of proofs or terms operationally interpreted as a strong form of nondeterminism. The main idea of coherent differentiation is that these sums can be controlled and kept in the realm of determinism by means of a notion of summability, upon enforcing summability restrictions on the derivatives which can be written in the models and in the syntax.
