Related papers: On Quantitative Algebraic Higher-Order Theories
Quantitative algebras are $\Sigma$-algebras acting on metric spaces, where operations are nonexpanding. Mardare, Panangaden and Plotkin introduced 1-basic varieties as categories of quantitative algebras presented by quantitative equations.…
Generalized metrics, arising from Lawvere's view of metric spaces as enriched categories, have been widely applied in denotational semantics as a way to measure to which extent two programs behave in a similar, although non equivalent, way.…
This paper proposes appropriate sound and complete proof systems for algebraic structures over metric spaces by combining the development of Quantitative Equational Theories (QET) with the Enriched Lawvere Theories. We extend QETs to Metric…
We develop universal algebra over an enriched category $\mathcal K$ and relate it to finitary enriched monads over $\mathcal K$. Using it, we deduce recent results about ordered universal algebra where inequations are used instead of…
We introduce the concept of compact quantitative equational theory. A quantitative equational theory is defined to be compact if all its consequences are derivable by means of finite proofs. We prove that the theory of interpolative…
Quantitative algebras are algebras enriched in the category $\mathsf{Met}$ of metric spaces so that all operations are nonexpanding. Mardare, Plotkin and Panangaden introduced varieties (aka $1$-basic varieties) as classes of quantitative…
In various subjects including mathematics, one can hope to use mathematical thinking well when the right kinds of algebraic structure to consider can be discovered or spotted. Therefore, it would help to understand kinds of algebraic…
Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the…
The framework of quantitative equational logic has been successfully applied to reason about algebras whose carriers are metric spaces and operations are nonexpansive. We extend this framework in two orthogonal directions: algebras endowed…
We provide graded extensions of algebraic theories and Lawvere theories that correspond to graded monads. We prove that graded algebraic theories, graded Lawvere theories, and finitary graded monads are equivalent via equivalence of…
We propose a categorical and algebraic study of quantale modules. The results and constructions presented are also applied to abstract algebraic logic and to image processing tasks.
Monads are of interest both in semantics and in higher dimensional algebra. It turns out that the idea behind usual notion finitary monads (whose values on all sets can be computed from their values on finite sets) extends to a more general…
We describe a type system for the linear-algebraic $\lambda$-calculus. The type system accounts for the linear-algebraic aspects of this extension of $\lambda$-calculus: it is able to statically describe the linear combinations of terms…
Algebraic logic studies algebraic theories related to proposition and first-order logic. A new algebraic approach to first-order logic is sketched in this paper. We introduce the notion of a quantifier theory, which is a functor from the…
Fiore and Hur recently introduced a conservative extension of universal algebra and equational logic from first to second order. Second-order universal algebra and second-order equational logic respectively provide a model theory and a…
A quantitative model of concurrent interaction is introduced. The basic objects are linear combinations of partial order relations, acted upon by a group of permutations that represents potential non-determinism in synchronisation. This…
Many important computational structures involve an intricate interplay between algebraic features (given by operations on the underlying set) and relational features (taking account of notions such as order or distance). This paper…
Finding a denotational semantics for higher order quantum computation is a long-standing problem in the semantics of quantum programming languages. Most past approaches to this problem fell short in one way or another, either limiting the…
We formalize the quantum arithmetic, i.e. a relationship between number theory and operator algebras. Namely, it is proved that rational projective varieties are dual to the $C^*$-algebras with real multiplication. Our construction fits all…
We present an explicit basis for orders of arbitrary level N>1 in definite rational quaternion algebras. These orders have applications to computations of spaces of elliptic and quaternionic modular forms.