ترغب بنشر مسار تعليمي؟ اضغط هنا

Monads, partial evaluations, and rewriting

115   0   0.0 ( 0 )
 نشر من قبل Paolo Perrone
 تاريخ النشر 2018
  مجال البحث الهندسة المعلوماتية
والبحث باللغة English




اسأل ChatGPT حول البحث

Monads can be interpreted as encoding formal expressions, or formal operations in the sense of universal algebra. We give a construction which formalizes the idea of evaluating an expression partially: for example, 2+3 can be obtained as a partial evaluation of 2+2+1. This construction can be given for any monad, and it is linked to the famous bar construction, of which it gives an operational interpretation: the bar construction induces a simplicial set, and its 1-cells are partial evaluations. We study the properties of partial evaluations for general monads. We prove that whenever the monad is weakly cartesian, partial evaluations can be composed via the usual Kan filler property of simplicial sets, of which we give an interpretation in terms of substitution of terms. In terms of rewritings, partial evaluations give an abstract reduction system which is reflexive, confluent, and transitive whenever the monad is weakly cartesian. For the case of probability monads, partial evaluations correspond to what probabilists call conditional expectation of random variables. This manuscript is part of a work in progress on a general rewriting interpretation of the bar construction.



قيم البحث

اقرأ أيضاً

110 - Richard Garner 2018
We provide new categorical perspectives on Jacobs notion of hypernormalisation of sub-probability distributions. In particular, we show that a suitable general framework for notions of hypernormalisation is that of a symmetric monoidal category endow ed with a linear exponential monad---a notion arising in the categorical semantics of Girards linear logic. We show that Jacobs original notion of hypernormalisation arises in this way from the finitely supported probability measure monad on the category of sets, which can be seen as a linear exponential monad with respect to a monoidal structure on sets arising from a quantum-algebraic object which we term the Giry tricocycloid. We give many other examples of hypernormalisation arising from other linear exponential monads.
The algebraic expression $3 + 2 + 6$ can be evaluated to $11$, but it can also be partially evaluated to $5 + 6$. In categorical algebra, such partial evaluations can be defined in terms of the $1$-skeleton of the bar construction for algebras of a m onad. We show that this partial evaluation relation can be seen as the relation internal to the category of algebras generated by relating a formal expression to its total evaluation. The relation is transitive for many monads which describe commonly encountered algebraic structures, and more generally for BC monads on $mathsf{Set}$ (which are those monads for which the underlying functor and the multiplication are weakly cartesian). We find that this is not true for all monads: we describe a finitary monad on $mathsf{Set}$ for which the partial evaluation relation on the terminal algebra is not transitive. With the perspective of higher algebraic rewriting in mind, we then investigate the compositional structure of the bar construction in all dimensions. We show that for algebras of BC monads, the bar construction has fillers for all directed acyclic configurations in $Delta^n$, but generally not all inner horns.
We describe an abstract 2-categorical setting to study various notions of polynomial and analytic functors and monads.
We characterize the category of monads on $Set$ and the category of Lawvere theories that are equivalent to the category of regular equational theories.
This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about (abstract) programming languages or calculi. Generalising the reduction monads of Ahrens et al., we introduce transition monads, th us covering new applications such as lambda-bar-mu-calculus, pi-calculus, Positive GSOS specifications, differential lambda-calculus, and the big-step, simply-typed, call-by-value lambda-calculus. Moreover, we design a suitable notion of signature for transition monads.
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا