Preservation of Equations by Monoidal Monads
Autor: | Parlant, L., Rot, J., Silva, A., Westerbaan, Bas., Esparza, J. |
---|---|
Přispěvatelé: | Esparza, J. |
Jazyk: | angličtina |
Rok vydání: | 2020 |
Předmět: |
FOS: Computer and information sciences
060201 languages & linguistics Computer Science - Logic in Computer Science preservation of equations Mathematics - Category Theory 06 humanities and the arts 02 engineering and technology monoidal monads Logic in Computer Science (cs.LO) Theory of computation → Categorical semantics algebraic theories Mathematics::Category Theory 0602 languages and literature Software Science FOS: Mathematics 0202 electrical engineering electronic engineering information engineering Category Theory (math.CT) 020201 artificial intelligence & image processing |
Zdroj: | Esparza, J. (ed.), 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020), 77:1-77:14. Dagstuhl : Schloss Dagstuhl STARTPAGE=77:1;ENDPAGE=77:14;ISSN=1868-8969;TITLE=Esparza, J. (ed.), 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020) Esparza, J. (ed.), 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020), pp. 77:1-77:14 |
ISSN: | 1868-8969 |
DOI: | 10.4230/lipics.mfcs.2020.77 |
Popis: | If a monad $T$ is monoidal, then operations on a set $X$ can be lifted canonically to operations on $TX$. In this paper we study structural properties under which $T$ preserves equations between those operations. It has already been shown that any monoidal monad preserves linear equations; affine monads preserve drop equations (where some variable appears only on one side, such as $x\cdot y = y$) and relevant monads preserve dup equations (where some variable is duplicated, such as $x \cdot x = x$). We start the paper by showing a converse: if the monad at hand preserves a drop equation, then it must be affine. From this, we show that the problem whether a given (drop) equation is preserved is undecidable. A converse for relevance turns out to be more subtle: preservation of certain dup equations implies a weaker notion which we call $n$-relevance. Finally, we identify the subclass of equations such that their preservation is equivalent to relevance. |
Databáze: | OpenAIRE |
Externí odkaz: |