Littérature scientifique sur le sujet « Semiring Monads »

Weighted search is an essential component of many fundamental and useful algorithms. Despite this, it is relatively under explored as a computational effect, receiving not nearly as much attention as either depth- or breadth-first search. This paper explores the algebraic underpinning of weighted search, and demonstrates how to implement it as a monad transformer. The development first explores breadth-first search, which can be expressed as a polynomial over semirings. These polynomials are generalised to the free semimodule monad to capture a wide range of applications, including probability monads, polynomial monads, and monads for weighted search. Finally, a monad transformer based on the free semimodule monad is introduced. Applying optimisations to this type yields an implementation of pairing heaps, which is then used to implement Dijkstra's algorithm and efficient probabilistic sampling. The construction is formalised in Cubical Agda and implemented in Haskell.

AbstractThis paper contributes to the techniques of topo-algebraic recognition for languages beyond the regular setting as they relate to logic on words. In particular, we provide a general construction on recognisers corresponding to adding one layer of various kinds of quantifiers and prove a corresponding Reutenauer-type theorem. Our main tools are codensity monads and duality theory. Our construction hinges on a measure-theoretic characterisation of the profinite monad of the free S-semimodule monad for finite and commutative semirings S, which generalises our earlier insight that the Vietoris monad on Boolean spaces is the codensity monad of the finite powerset functor.

We study the canonical weak distributive law $\delta$ of the powerset monad over the semimodule monad for a certain class of semirings containing, in particular, positive semifields. For this subclass we characterise $\delta$ as a convex closure in the free semimodule of a set. Using the abstract theory of weak distributive laws, we compose the powerset and the semimodule monads via $\delta$, obtaining the monad of convex subsets of the free semimodule.

AbstractWe exhibit a monoidal structure on the category of finite sets indexed by P-trees for a finitary polynomial endofunctor P. This structure categorifies the monoid scheme (over Spec ℕ) whose semiring of functions is (a P-version of) the Connes-Kreimer bialgebra H of rooted trees (a Hopf algebra after base change to ℤ and collapsing H 0). The monoidal structure is itself given by a polynomial functor, represented by three easily described set maps; we show that these maps are the same as those occurring in the polynomial representation of the free monad on P.

International audience Connection matrices for graph parameters with values in a field have been introduced by M. Freedman, L. Lovász and A. Schrijver (2007). Graph parameters with connection matrices of finite rank can be computed in polynomial time on graph classes of bounded tree-width. We introduce join matrices, a generalization of connection matrices, and allow graph parameters to take values in the tropical rings (max-plus algebras) over the real numbers. We show that rank-finiteness of join matrices implies that these graph parameters can be computed in polynomial time on graph classes of bounded clique-width. In the case of graph parameters with values in arbitrary commutative semirings, this remains true for graph classes of bounded linear clique-width. B. Godlin, T. Kotek and J.A. Makowsky (2008) showed that definability of a graph parameter in Monadic Second Order Logic implies rank finiteness. We also show that there are uncountably many integer valued graph parameters with connection matrices or join matricesof fixed finite rank. This shows that rank finiteness is a much weaker assumption than any definability assumption. Les matrices de connexion pour des fonctions sur les graphes à valeurs dans un corps ont été introduites par M. Freedman, L. Lovász and A. Schrijver (2007). Une fonctions sur les graphes ayant des matrices de connexion de rang fini peut être calculée en temps polynomial sur toute famille de graphes de largeur arborescente (”tree-width”) bornée. Nous introduisons des matrices de jointure (”join matrices”) qui généralisent les matrices deconnexion, et nous permettons aux fonctions sur les graphes de prendre leurs valeurs dans des semianneaux tropicaux réels. Nous montrons qu’une fonction sur les graphes ayant des matrices de jointure de rang fini peut être calculée en temps polynomial sur des graphes de largeur de clique (”clique-width”) bornée. Dans le cas des semi-anneaux commutatifs, cela reste vrai pour les graphes de largeur de clique linéaire bornée. B. Godlin, T. Kotek and J.A. Makowsky (2008) ont montré que certaines hypothèses de definissabilité en Logique du Second Ordre Monadique concernant desopérations sur les graphes entraine la finitude des rangs. Nous exhibons un ensemble non dénombrable d’opérations ayant une matrice de connexion et des matrices de jointure de rang fini. Cela démontre que l’hypothèse de rang fini est beaucoup plus faible que l’hypothèse de definissabilité.

Bien qu'elle ait été introduite il y a plus de 60 ans, PCF reste intéressante. Bien que la quête d'un modèle satisfaisant et totalement abstrait de PCF ait été résolue au tournant du millénaire, de nouveaux modèles de PCF apparaissent encore fréquemment dans la littérature, explorant des voies inexplorées ou utilisant PCF comme une lentille ou un outil pour étudier une autre construction mathématique. Dans cette thèse, nous nous appuyons sur notre connaissance des modèles de PCF de deux manières distinctes : En construisant un tout nouveau modèle, et en s'appuyant sur les modèles existants. Les machines d'adressage sont un type relativement nouveau de machine abstraite qui s'inspire des machines de Turing. Il a déjà été démontré que ces machines peuvent modéliser l'ensemble du ?-calcul non typé. Nous nous appuyons sur ces machines pour construire des machinesd'adressage étendues (EAM) et les doter d'un système de type. Nous montrons ensuite que ces machines peuvent être utilisées pour obtenir un nouveau modèle entièrement abstrait et distinct de PCF : Nous montrons que les machines simulent fidèlement PCF de telle sorte qu'un terme PCF se termine par un chiffre exactement lorsque la machine d'adressage étendue correspondante se termine par le même chiffre. De même, nous montrons que chaque machine d'adressage étendue typée peut être transformée en un programme PCF avec le même comportement d'observation. De ces deux résultats, il découle que le modèle de PCF obtenu en quotientant les EAM typables par une relation logique appropriée est totalement abstrait. Il existe une pléthore de modèles catégoriels solides de PCF, en raison de sa relation étroite avec le ?-calcul. Nous considérons deux modèles similaires (qui sont aussi des modèles de logique linéaire) qui sont basés sur des sémirings : Les modèles pondérés, qui utilisent les sémirations pour quantifier une valeur interne, et les modèles de multiplicité, qui utilisent les sémirations pour modéliser linéairement des fonctions (modèle de l'exponentielle !). Nous étudionsl'intersection entre ces deux modèles en examinant les conditions sous lesquelles deux monades dérivées de sémirings spécifiques se distribuent. Nous découvrons que le fait qu'un semi-anneau ait ou non une somme idempotente fait une grande différence dans sa capacité à distribuer. Notre étude nous conduit à découvrir la notion de distribution non naturelle, qui forme une monade sur une catégorie de Kleisli. Enfin, nous présentons des conditions précises sous lesquelles une distribution particulière peut se former entre deux semis
Despite being introduced over 60 years ago, PCF remains of interest. Though the quest for a satisfactory fully abstract model of PCF was resolved around the turn of the millennium, new models of PCF still frequently appear in the literature, investigating unexplored avenues or using PCF as a lens or tool to investigate some other mathematical construct. In this thesis, we build upon our knowledge of models of PCF in two distinct ways: Constructing a brand new model, and building upon existing models. Addressing Machines are a relatively new type of abstract machine taking inspiration from Turing Machines. These machines have been previously shown to model the full untyped ?- calculus. We build upon these machines to construct Extended Addressing Machines (EAMs) and endow them with a type system. We then show that these machines can be used to obtain a new and distinct fully abstract model of PCF: We show that the machines faithfully simulatePCF in such a way that a PCF term terminates in a numeral exactly when the corresponding Extended Addressing Machine terminates in the same numeral. Likewise, we show that every typed Extended Addressing Machine can be transformed into a PCF program with the same observational behaviour. From these two results, it follows that the model of PCF obtained by quotienting typable EAMs by a suitable logical relation is fully abstract. There exist a plethora of sound categorical models of PCF, due to its close relationship with the ?-calculus. We consider two similar models (which are also models of Linear Logic) that are based on semirings: Weighted models, using semirings to quantify some internal value, and Multiplicity models, using semirings to linearly model functions (model the exponential !). We investigate the intersection between these two models by investigating the conditions under which two monads derived from specific semirings distribute. We discover that whether or not a semiring has an idempotent sum makes a large difference in its ability to distribute. Our investigation leads us to discover the notion of an unnatural distribution, which forms a monad on a Kleislicategory. Finally, we present precise conditions under which a particular distribution can form between two semirings

Le thème central de la présente thèse est le contenu sémantique des quantificateurs logiques. Dans leur forme la plus simple, les quantificateurs permettent d’établir l’existence, ou la non-existence, d’individus répondant à une propriété. En tant que tels, ils incarnent la richesse et la complexité de la logique du premier ordre, par delà la logique propositionnelle. Nous contribuons à l’analyse sémantique des quantificateurs, du point de vue de la théorie de la dualité, dans trois domaines différents des mathématiques et de l’informatique théorique. D’une part, dans la théorie des langages formels à travers la logique sur les mots. D’autre part, dans la logique intuitionniste propositionnelle et dans l’étude de l’interpolation uniforme. Enfin, dans la topologie catégorique et dans la sémantique catégorique de la logique du premier ordre
The unifying theme of the thesis is the semantic meaning of logical quantifiers. In their basic form quantifiers allow to state theexistence, or non-existence, of individuals satisfying a property. As such, they encode the richness and the complexity of predicate logic, as opposed to propositional logic. We contribute to the semantic understanding of quantifiers, from the viewpoint of duality theory, in three different areas of mathematics and theoretical computer science. First, in formal language theory through the syntactic approach provided by logic on words. Second, in intuitionistic propositional logic and in the study of uniform interpolation. Third, in categorical topology and categorical semantics for predicate logic

AbstractWe describe the canonical weak distributive law $$\delta :\mathcal S\mathcal P\rightarrow \mathcal P\mathcal S$$ δ : S P → P S of the powerset monad $$\mathcal P$$ P over the S-left-semimodule monad $$\mathcal S$$ S , for a class of semirings S. We show that the composition of $$\mathcal P$$ P with $$\mathcal S$$ S by means of such $$\delta $$ δ yields almost the monad of convex subsets previously introduced by Jacobs: the only difference consists in the absence in Jacobs’s monad of the empty convex set. We provide a handy characterisation of the canonical weak lifting of $$\mathcal P$$ P to $$\mathbb {EM}(\mathcal S)$$ EM ( S ) as well as an algebraic theory for the resulting composed monad. Finally, we restrict the composed monad to finitely generated convex subsets and we show that it is presented by an algebraic theory combining semimodules and semilattices with bottom, which are the algebras for the finite powerset monad $$\mathcal P_f$$ P f .

This chapter examines conjunction fallacies. This phenomenon is a topic in the psychology of reasoning and is not strictly linguistic, but it is related to pragmatics. Monads are shown to capture conjunction fallacies compositionally, which has eluded prominent prior theories. The chapter contrasts a monad built around the probability semiring with one built around a simpler semiring, the one semiring. The choice between the probability and one semirings partially predicts experimental participants’ behaviour. This points to an explanation in terms of the satisficing heuristic, rather than the representativeness heuristic. The chapter explores two options for fully predicting the results. The first is to use Gricean pragmatics in addition to the one semiring. The second is to use alternative underlying semirings for the monad: tropical semirings. This alternative compositional solution achieves a highly satisfying fit with aggregate psychological data and preserves an interesting duality between the logical operations of conjunction and disjunction. Some exercises are provided to aid understanding.