Models of a Non-associative Composition

详细信息    查看全文

• 作者：Guillaume Munch-Maccagnoni (17)
  
• 刊名：Lecture Notes in Computer Science
• 出版年：2014
• 出版时间：2014
• 年：2014
• 卷：8412
• 期：1
• 页码：396-410
• 全文大小：313 KB
• 参考文献：1. Abramsky, S.: Sequentiality vs. concurrency in games and logic. Math. Struct. Comput. Sci.?13(4), 531-65 (2003) CrossRef
  2. Ariola, Z.M., Herbelin, H.: Control Reduction Theories: the Benefit of Structural Substitution. Journal of Functional Programming?18(3), 373-19 (2008) CrossRef
  3. Blass, A.: A game semantics for linear logic. Ann. Pure Appl. Logic?56(1-3), 183-20 (1992) CrossRef
  4. Curien, P.L., Herbelin, H.: The duality of computation. ACM SIGPLAN Notices?35, 233-43 (2000) CrossRef
  5. Danos, V., Joinet, J.B., Schellinx, H.: A New Deconstructive Logic: Linear Logic. Journal of Symbolic Logic?62(3), 755-07 (1997) CrossRef
  6. Führmann, C.: Direct Models for the Computational Lambda Calculus. Electr. Notes Theor. Comput. Sci.?20, 245-92 (1999) CrossRef
  7. Girard, J.Y.: A new constructive logic: Classical logic. Math. Struct. Comp. Sci.?1(3), 255-96 (1991) CrossRef
  8. Herbelin, H.: C’est maintenant qu’on calcule, au c?ur de la dualité, Habilitation thesis (2005)
  9. Jacobs, B.: Comprehension categories and the semantics of type dependency. Theor. Comput. Sci.?107(2), 169-07 (1993) CrossRef
  10. Lafont, Y., Reus, B., Streicher, T.: Continuation Semantics or Expressing Implication by Negation. Technical report, University of Munich (1993)
  11. Laurent, O.: Etude de la polarisation en logique. Thèse de doctorat, Université Aix-Marseille?II (March 2002)
  12. Laurent, O., Quatrini, M., Tortora de Falco, L.: Polarized and focalized linear and classical proofs. Ann. Pure Appl. Logic?134(2-3), 217-64 (2005) CrossRef
  13. Levy, P.B.: Call-by-Push-Value: A Subsuming Paradigm. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol.?1581, pp. 228-43. Springer, Heidelberg (1999) CrossRef
  14. Levy, P.B.: Adjunction models for call-by-push-value with stacks. In: Proc. Cat. Th. and Comp. Sci. ENTCS, vol.?69 (2005)
  15. Loday, J.L.: Generalized bialgebras and triples of operads. arXiv preprint math/0611885 (2006)
  16. Melliès, P.A.: Asynchronous Games 3 An Innocent Model of Linear Logic. Electr. Notes Theor. Comput. Sci.?122, 171-92 (2005) CrossRef
  17. Melliès, P.A., Tabareau, N.: Resource modalities in tensor logic. Ann. Pure Appl. Logic?161(5), 632-53 (2010) CrossRef
  18. Moggi, E.: Computational Lambda-Calculus and Monads. In: LICS (1989)
  19. Munch-Maccagnoni, G.: Focalisation and classical realisability. In: Gr?del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol.?5771, pp. 409-23. Springer, Heidelberg (2009) CrossRef
  20. Munch-Maccagnoni, G.: Syntax and Models of a non-Associative Composition of Programs and Proofs. PhD thesis, Univ. Paris Diderot (2013)
  21. Murthy, C.R.: A Computational Analysis of Girard’s Translation and LC. In: LICS, pp. 90-01. IEEE Computer Society (1992)
  22. Selinger, P.: Re: co-exponential question. Message to the Category Theory mailing list (July 1999), http://permalink.gmane.org/gmane.science.mathematics.categories/1181
  23. Selinger, P.: Control Categories and Duality: On the Categorical Semantics of the Lambda-Mu Calculus. Math. Struct in Comp. Sci.?11(2), 207-60 (2001) CrossRef
  24. Thielecke, H.: Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh (1997)
  25. Zeilberger, N.: On the unity of duality. Ann. Pure and App. Logic?153(1) (2008)
  
• 作者单位：Guillaume Munch-Maccagnoni (17)
  
  17. Sorbonne Paris Cité, PPS, UMR 7126 CNRS, PiR2, INRIA Paris-Rocquencourt, Univ Paris Diderot, F-75205, Paris, France
  
• ISSN：1611-3349

文摘

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.