TY - GEN
T1 - On Compositionality of Dinatural Transformations
AU - McCusker, Guy
AU - Santamaria, Alessio
PY - 2018/12/31
Y1 - 2018/12/31
N2 - Natural transformations are ubiquitous in mathematics, logic and computer science. For operations of mixed variance, such as currying and evaluation in the lambda-calculus, Eilenberg and Kelly's notion of extranatural transformation, and often the even more general dinatural transformation, is required. Unfortunately dinaturals are not closed under composition except in special circumstances. This paper presents a new sufficient condition for composability. We propose a generalised notion of dinatural transformation in many variables, and extend the Eilenberg-Kelly account of composition for extranaturals to these transformations. Our main result is that a composition of dinatural transformations which creates no cyclic connections between arguments yields a dinatural transformation. We also extend the classical notion of horizontal composition to our generalized dinaturals and demonstrate that it is associative and has identities.
AB - Natural transformations are ubiquitous in mathematics, logic and computer science. For operations of mixed variance, such as currying and evaluation in the lambda-calculus, Eilenberg and Kelly's notion of extranatural transformation, and often the even more general dinatural transformation, is required. Unfortunately dinaturals are not closed under composition except in special circumstances. This paper presents a new sufficient condition for composability. We propose a generalised notion of dinatural transformation in many variables, and extend the Eilenberg-Kelly account of composition for extranaturals to these transformations. Our main result is that a composition of dinatural transformations which creates no cyclic connections between arguments yields a dinatural transformation. We also extend the classical notion of horizontal composition to our generalized dinaturals and demonstrate that it is associative and has identities.
KW - Categorical logic
KW - Compositionality
KW - Dinatural transformation
UR - http://drops.dagstuhl.de/opus/portals/lipics/index.php?semnr=16086
UR - http://www.scopus.com/inward/record.url?scp=85053055453&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CSL.2018.33
DO - 10.4230/LIPIcs.CSL.2018.33
M3 - Chapter in a published conference proceeding
VL - 119
T3 - Leibniz International Proceedings in Informatics (LIPIcs)
SP - 33:1-33:22
BT - 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)
A2 - Ghica, Dan
A2 - Jung, Achim
PB - Leibniz International Proceedings in Informatics
CY - Dagstuhl, Germany
ER -