Abstract
We characterise the polarised evaluation order through a categorical structure where the hypothesis that composition is associative is relaxed. Duploid is the name of the structure, as a reference to Jean-Louis Loday’s duplicial algebras. The main result is a reflection where is a category of duploids and duploid functors, and is the category of adjunctions and pseudo maps of adjunctions. The result suggests that the various biases in denotational semantics: indirect, call-by-value, call-by-name... are ways of hiding the fact that composition is not always associative.
This is a shortened version of Chapter II from the author’s PhD thesis [20, pp. 86-91,103-152].
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abramsky, S.: Sequentiality vs. concurrency in games and logic. Math. Struct. Comput. Sci. 13(4), 531–565 (2003)
Ariola, Z.M., Herbelin, H.: Control Reduction Theories: the Benefit of Structural Substitution. Journal of Functional Programming 18(3), 373–419 (2008)
Blass, A.: A game semantics for linear logic. Ann. Pure Appl. Logic 56(1-3), 183–220 (1992)
Curien, P.L., Herbelin, H.: The duality of computation. ACM SIGPLAN Notices 35, 233–243 (2000)
Danos, V., Joinet, J.B., Schellinx, H.: A New Deconstructive Logic: Linear Logic. Journal of Symbolic Logic 62(3), 755–807 (1997)
Führmann, C.: Direct Models for the Computational Lambda Calculus. Electr. Notes Theor. Comput. Sci. 20, 245–292 (1999)
Girard, J.Y.: A new constructive logic: Classical logic. Math. Struct. Comp. Sci. 1(3), 255–296 (1991)
Herbelin, H.: C’est maintenant qu’on calcule, au cœur de la dualité, Habilitation thesis (2005)
Jacobs, B.: Comprehension categories and the semantics of type dependency. Theor. Comput. Sci. 107(2), 169–207 (1993)
Lafont, Y., Reus, B., Streicher, T.: Continuation Semantics or Expressing Implication by Negation. Technical report, University of Munich (1993)
Laurent, O.: Etude de la polarisation en logique. Thèse de doctorat, Université Aix-Marseille II (March 2002)
Laurent, O., Quatrini, M., Tortora de Falco, L.: Polarized and focalized linear and classical proofs. Ann. Pure Appl. Logic 134(2-3), 217–264 (2005)
Levy, P.B.: Call-by-Push-Value: A Subsuming Paradigm. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 228–243. Springer, Heidelberg (1999)
Levy, P.B.: Adjunction models for call-by-push-value with stacks. In: Proc. Cat. Th. and Comp. Sci. ENTCS, vol. 69 (2005)
Loday, J.L.: Generalized bialgebras and triples of operads. arXiv preprint math/0611885 (2006)
Melliès, P.A.: Asynchronous Games 3 An Innocent Model of Linear Logic. Electr. Notes Theor. Comput. Sci. 122, 171–192 (2005)
Melliès, P.A., Tabareau, N.: Resource modalities in tensor logic. Ann. Pure Appl. Logic 161(5), 632–653 (2010)
Moggi, E.: Computational Lambda-Calculus and Monads. In: LICS (1989)
Munch-Maccagnoni, G.: Focalisation and classical realisability. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 409–423. Springer, Heidelberg (2009)
Munch-Maccagnoni, G.: Syntax and Models of a non-Associative Composition of Programs and Proofs. PhD thesis, Univ. Paris Diderot (2013)
Murthy, C.R.: A Computational Analysis of Girard’s Translation and LC. In: LICS, pp. 90–101. IEEE Computer Society (1992)
Selinger, P.: Re: co-exponential question. Message to the Category Theory mailing list (July 1999), http://permalink.gmane.org/gmane.science.mathematics.categories/1181
Selinger, P.: Control Categories and Duality: On the Categorical Semantics of the Lambda-Mu Calculus. Math. Struct in Comp. Sci. 11(2), 207–260 (2001)
Thielecke, H.: Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh (1997)
Zeilberger, N.: On the unity of duality. Ann. Pure and App. Logic 153(1) (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Munch-Maccagnoni, G. (2014). Models of a Non-associative Composition. In: Muscholl, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2014. Lecture Notes in Computer Science, vol 8412. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54830-7_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-54830-7_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54829-1
Online ISBN: 978-3-642-54830-7
eBook Packages: Computer ScienceComputer Science (R0)