Monads and their composition via distributive laws have many applications in program semantics and functional programming. For many interesting monads, distributive laws fail to exist, and this has motivated investiga...
详细信息
ISBN:
(数字)9783031107368
ISBN:
(纸本)9783031107368;9783031107351
Monads and their composition via distributive laws have many applications in program semantics and functional programming. For many interesting monads, distributive laws fail to exist, and this has motivated investigations into weaker notions. In this line of research, Petrisan and Sarkis recently introduced a construction called the semifree monad in order to study semialgebras for a monad and weak distributive laws. In this paper, we prove that an algebraic presentation of the semifree monad M-s on a monad M can be obtained uniformly from an algebraic presentation of M. This result was conjectured by Petrisan and Sarkis. We also show that semifree monads are ideal monads, that the semifree construction is not a monad transformer, and that the semifree construction is a comonad on the category of monads.
We propose another interpretation of well-known derivatives computations from regular expressions, due to Brzozowski, Antimirov or Lombardy and Sakarovitch, in order to abstract the underlying data structures (e.g. se...
详细信息
We propose another interpretation of well-known derivatives computations from regular expressions, due to Brzozowski, Antimirov or Lombardy and Sakarovitch, in order to abstract the underlying data structures (e.g. sets or linear combinations) using the notion of monad. As an example of this generalization advantage, we introduce a new derivation technique based on the graded module monad. We also extend operators defining expressions to any n-ary functions over value sets, such as classical operations (like negation or intersection for Boolean weights) or more exotic ones (like algebraic mean for rational weights). Moreover, we present how to compute a (non-necessarily finite) automaton from such an extended expression, using the Colcombet and Petrisan categorical definition of automata. These categorytheory concepts allow us to perform this construction in a unified way, whatever the underlying monad. Finally, to illustrate our work, we present a Haskell implementation of these notions using advanced techniques of functional programming, and we provide a web interface to manipulate concrete examples.
The proceedings contain 13 papers. The special focus in this conference is on Coalgebraic Methods in computer Science. The topics include: Fixed points of functors;compositional coinduction with sized types;lawvere ca...
ISBN:
(纸本)9783319403694
The proceedings contain 13 papers. The special focus in this conference is on Coalgebraic Methods in computer Science. The topics include: Fixed points of functors;compositional coinduction with sized types;lawvere categories as composed props;transitivity and difunctionality of bisimulations;affine monads and side-effect-freeness;duality of equations and coequations via contravariant adjunctions;category theoretic semantics for theorem proving in logic programming;product rules and distributive laws;on the logic of generalised metric spaces;a complete logic for behavioural equivalence in coalgebras of finitary set functors;coalgebraic completeness-via-canonicity;relational lattices via duality and on local characterization of global timed bisimulation for abstract continuous-time systems.
This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guarded recursive types, which are useful ...
详细信息
Contemporary simulation technology for neuronal networks enables the simulation of brain-scale networks using neuron models with a single or a few compartments. However, distributed simulations at full cell density ar...
详细信息
The security literature offers a multitude of calculi, languages, and systems for information-flow control, each with some set of labels encoding security policies that can be attached to data and computations. The ex...
详细信息
ISBN:
(纸本)9780769550312
The security literature offers a multitude of calculi, languages, and systems for information-flow control, each with some set of labels encoding security policies that can be attached to data and computations. The exact form of these labels varies widely, with different systems offering many different combinations of features addressing issues such as confidentiality, integrity, and policy ownership. This variation makes it difficult to compare the expressive power of different information-flow frameworks. To enable such comparisons, we introduce label algebras, an abstract interface for information-flow labels equipped with a notion of authority, and study several notions of embedding between them. The simplest is a straightforward notion of injection between label algebras, but this lacks a clear computational motivation and rejects some reasonable encodings between label models. We obtain a more refined account by defining a space of encodings parameterized by an interpretation of labels and authorities, thus giving a semantic flavor to the definition of encoding. We study the theory of semantic encodings and consider two specific instances, one based on the possible observations of boolean values and one based on the behavior of programs in a small lambda-calculus parameterized over an arbitrary label algebra. We use this framework to define and compare a number of concrete label algebras, including realizations of the familiar taint, endorsement, readers, and distrust models, as well as label algebras based on several existing programming languages and operating systems.
This paper describes basic concepts from categorytheory, which are commonly used in functional programming. These concepts are applied to shader programming and to the rendering pipeline and the whole rendering pipel...
详细信息
ISBN:
(纸本)9788086943855
This paper describes basic concepts from categorytheory, which are commonly used in functional programming. These concepts are applied to shader programming and to the rendering pipeline and the whole rendering pipeline is formally modelled using categorytheory. This model can be used for more abstract and formal approach to shader programming. Mathematical formalization of the rendering pipeline and its stages can be helpful in shader compiler design, for proving algorithms, complexity analysis, and other tasks.
Bent functions were first introduced by Rothaus in 1976 as an interesting combinatorial object with the important property of having the maximum distance to all affine functions. Bent functions have many applications ...
详细信息
ISBN:
(纸本)9781424470143
Bent functions were first introduced by Rothaus in 1976 as an interesting combinatorial object with the important property of having the maximum distance to all affine functions. Bent functions have many applications to coding theory, cryptography and sequence designs. For many years the focus was on the construction of binary bent functions. There are several known examples of binary monomial and binomial bent functions. In 1985, Kumar, Scholtz and Welch generalized bent functions to the case of an arbitrary finite field. In the recent years, new results on nonbinary bent functions have appeared. This paper gives an updated overview of some of the recent results and open problems on generalized bent functions. This includes some recent constructions of weakly regular monomial and binomial bent functions and examples of non-weakly regular bent functions.
Moggi's computational Monads and Power et al.'s equivalent notion of Freyd category have captured a large range of computational effects present in programming languages. Examples include non-termination, non-...
详细信息
Moggi's computational Monads and Power et al.'s equivalent notion of Freyd category have captured a large range of computational effects present in programming languages. Examples include non-termination, non-determinism, exceptions, continuations, side effects and input/output. We present generalisations of both computational monads and Freyd categories, which we call parameterised monads and parameterised Freyd categories, that also capture computational effects with para meters. Examples of such are composable continuations, side effects where the type of the state varies and input/output where the range of inputs and outputs varies. By considering structured parameterisation also, we extend the range of effects to cover separated side effects and Multiple independent streams of I/O. We also present two typed lambda-calculi that Soundly and completely model out categorical definitions - with and without symmetric monoidal parameterisation - and act as prototypical languages with parameterised effects.
A Freyd-category is a subtle generalisation of the notion of a category with finite products. It is suitable for modelling environments in call-by-value programming languages, such as the computational lambda-calculus...
详细信息
A Freyd-category is a subtle generalisation of the notion of a category with finite products. It is suitable for modelling environments in call-by-value programming languages, such as the computational lambda-calculus, with computational effects. We develop the theory of Freyd-categories with that in mind. We first show that any countable Lawvere theory, hence any signature of operations with countable arity subject to equations, directly generates a Freyd-category. We then give canonical, universal embeddings of Freyd-categories into closed Freyd-categories, characterised by being free cocompletions. The combination of the two constructions sends a signature of operations and equations to the Kleisli category for the monad on the category Set generated by it, thus refining the analysis of computational effects given by monads. That in turn allows a more structural analysis of the lambda(c)-calculus. Our leading examples of signatures arise from side-effects, interactive input/output and exceptions. We extend our analysis to an enriched setting in order to account for recursion and for computational effects and signatures that inherently involve it, such as partiality, nondeterminism and probabilistic nondeterminism. (C) 2006 Elsevier B.V. All rights reserved.
暂无评论