-
Cauchy-completions and the rule of unique choice in relational doctrines
Authors:
Francesco Dagnino,
Fabio Pasquali
Abstract:
Lawvere's generalised the notion of complete metric space to the field of enriched categories: an enriched category is said to be Cauchy-complete if every left adjoint bimodule into it is represented by an enriched functor. Looking at this definition from a logical standpoint, regarding bimodules as an abstraction of relations and functors as an abstraction of functions, Cauchy-completeness resemb…
▽ More
Lawvere's generalised the notion of complete metric space to the field of enriched categories: an enriched category is said to be Cauchy-complete if every left adjoint bimodule into it is represented by an enriched functor. Looking at this definition from a logical standpoint, regarding bimodules as an abstraction of relations and functors as an abstraction of functions, Cauchy-completeness resembles a formulation of the rule of unique choice. In this paper, we make this analogy precise, using the language of relational doctrines, a categorical tool that provides a functorial description of the calculus of relations, in the same way Lawvere's hyperdoctrines give a functorial description of predicate logic. Given a relational doctrine, we define Cauchy-complete objects as those objects of the domain category satisfying the rule of unique choice. Then, we present a universal construction that completes a relational doctrine with the rule of unique choice, that is, producing a new relational doctrine where all objects are Cauchy-complete. We also introduce relational doctrines with singleton objects and show that these have the minimal structure needed to build the reflector of the full subcategory of its domain on Cauchy-complete objects. The main result is that this reflector exists if and only if the relational doctrine has singleton objects and this happens if and only if its restriction to Cauchy-complete objects is equivalent to its completion with the rule of unique choice. We support our results with many examples, also falling outside the scope of standard doctrines, such as complete metric spaces, Banach spaces and compact Hausdorff spaces in the general context of monoidal topology, which are all shown to be Cauchy-complete objects for appropriate relational doctrines.
△ Less
Submitted 29 February, 2024;
originally announced February 2024.
-
Quantitative Equality in Substructural Logic via Lipschitz Doctrines
Authors:
Francesco Dagnino,
Fabio Pasquali
Abstract:
Substructural logics naturally support a quantitative interpretation of formulas, as they are seen as consumable resources. Distances are the quantitative counterpart of equivalence relations: they measure how much two objects are similar, rather than just saying whether they are equivalent or not. Hence, they provide the natural choice for modelling equality in a substructural setting. In this pa…
▽ More
Substructural logics naturally support a quantitative interpretation of formulas, as they are seen as consumable resources. Distances are the quantitative counterpart of equivalence relations: they measure how much two objects are similar, rather than just saying whether they are equivalent or not. Hence, they provide the natural choice for modelling equality in a substructural setting. In this paper, we develop this idea, using the categorical language of Lawvere's doctrines. We work in a minimal fragment of Linear Logic enriched by graded modalities, which are needed to write a resource sensitive substitution rule for equality, enabling its quantitative interpretation as a distance. We introduce both a deductive calculus and the notion of Lipschitz doctrine to give it a sound and complete categorical semantics. The study of 2-categorical properties of Lipschitz doctrines provides us with a universal construction, which generates examples based for instance on metric spaces and quantitative realisability. Finally, we show how to smoothly extend our results to richer substructural logics, up to full Linear Logic with quantifiers.
△ Less
Submitted 29 April, 2024; v1 submitted 11 October, 2021;
originally announced October 2021.
-
iProStruct2D: Identifying protein structural classes by deep learning via 2D representations
Authors:
Loris Nanni,
Alessandra Lumini,
Federica Pasquali,
Sheryl Brahnam
Abstract:
In this paper we address the problem of protein classification starting from a multi-view 2D representation of proteins. From each 3D protein structure, a large set of 2D projections is generated using the protein visualization software Jmol. This set of multi-view 2D representations includes 13 different types of protein visualizations that emphasize specific properties of protein structure (e.g.…
▽ More
In this paper we address the problem of protein classification starting from a multi-view 2D representation of proteins. From each 3D protein structure, a large set of 2D projections is generated using the protein visualization software Jmol. This set of multi-view 2D representations includes 13 different types of protein visualizations that emphasize specific properties of protein structure (e.g., a backbone visualization that displays the backbone structure of the protein as a trace of the Cα atom). Each type of representation is used to train a different Convolutional Neural Network (CNN), and the fusion of these CNNs is shown to be able to exploit the diversity of different types of representations to improve classification performance. In addition, several multi-view projections are obtained by uniformly rotating the protein structure around its central X, Y, and Z viewing axes to produce 125 images. This approach can be considered a data augmentation method for improving the performance of the classifier and can be used in both the training and the testing phases. Experimental evaluation of the proposed approach on two datasets demonstrates the strength of the proposed method with respect to the other state-of-the-art approaches. The MATLAB code used in this paper is available at https://github.com/LorisNanni.
△ Less
Submitted 11 June, 2019;
originally announced June 2019.
