Abstract
We give a categorical semantics for a call-by-value linear lambda calculus. Such a lambda calculus was used by Selinger and Valiron as the backbone of a functional programming language for quantum computation. One feature of this lambda calculus is its linear type system, which includes a duplicability operator “!” as in linear logic. Another main feature is its call-by-value reduction strategy, together with a side-effect to model probabilistic measurements. The “!” operator gives rise to a comonad, as in the linear logic models of Seely, Bierman, and Benton. The side-effects give rise to a monad, as in Moggi’s computational lambda calculus. It is this combination of a monad and a comonad that makes the present paper interesting. We show that our categorical semantics is sound and complete.
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.: Computational interpretations of linear logic. Theoretical Computer Science 111, 3–57 (1993)
Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In: Proceedings of LICS 2004, pp. 415–425 (2004)
Barendregt, H.P.: The Lambda-Calculus, its Syntax and Semantics. North Holland, Amsterdam (1984)
Benton, N.: A mixed linear and non-linear logic: Proofs, terms and models (extended abstract). In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 121–135. Springer, Heidelberg (1995)
Benton, N., Bierman, G., de Paiva, V.C.V., Hyland, M.: A term calculus for intuitionistic linear logic. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 75–90. Springer, Heidelberg (1993)
Benton, N., Bierman, G., Hyland, M., de Paiva, V.C.V.: Linear lambda-calculus and categorical models revisited. In: Martini, S., Börger, E., Kleine Büning, H., Jäger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, Springer, Heidelberg (1993)
Benton, N., Wadler, P.: Linear logic, monads and the lambda calculus. In: Proceedings of LICS 1996, pp. 420–431 (1996)
Bierman, G.: On Intuitionistic Linear Logic. PhD thesis, Computer Science Department, Cambridge University, Cambridge (1993)
Coecke, B.: Quantum information-flow, concretely, abstractly. In: Selinger, P., (ed.) Proceedings of QPL 2004. TUCS General Publication No. 33, Turku Centre for Computer Science pp. 57–73 (2004)
Coecke, B., Pavlovic, D.: Quantum measurements without sums. In: Chen, G., Kauffman, L., Lomonaco, S.J. (eds.) Mathematics of Quantum Computation and Technology, pp. 559–596. Chapman & Hall, Boca Raton (2007)
Gay, S.J., Nagarajan, R.: Communicating quantum processes. In: Proceedings of POPL 2005, ACM Press, New York (2005)
Lalire, M., Jorrand, P.: A process algebraic approach to concurrent and distributed computation: Operational semantics. In: Selinger, P. (ed.) Proceedings of QPL 2004. TUCS General Publication No. 33, Turku Centre for Computer Science, pp. 109–126 (2004)
Mac Lane, S.: Categories for the Working Mathematician. Springer, Heidelberg (1998)
Moggi, E.: Notions of computation and monads. Information and Computation 93, 55–92 (1991)
Schalk, A.: What is a model for linear logic. Manuscript (2004)
Seely, R.A.G.: *-autonomous categories and cofree coalgebras. Contemporary Mathematics 92 (1989)
Selinger, P. (ed.): Proceedings of QPL 2004. TUCS General Publication No. 33, Turku Centre for Computer Science (2004)
Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science 14, 527–586 (2004)
Selinger, P., Valiron, B.: A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science 16, 527–552 (2006)
Selinger, P., Valiron, B.: On a fully abstract model for a quantum linear functional language. In: Preliminary proceedings of QPL 2006, pp. 103–115 (2006)
van Tonder, A.: A lambda calculus for quantum computation. SIAM Journal of Computing 33, 1109–1135 (2004)
Wadler, P.: There’s no substitute for linear logic. Manuscript, presented at MFPS 1992 (1992)
Wootters, W.K., Zurek, W.H.: A single quantum cannot be cloned. Nature 299, 802–803 (1982)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Selinger, P., Valiron, B. (2008). A Linear-non-Linear Model for a Computational Call-by-Value Lambda Calculus (Extended Abstract). In: Amadio, R. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2008. Lecture Notes in Computer Science, vol 4962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78499-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-78499-9_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78497-5
Online ISBN: 978-3-540-78499-9
eBook Packages: Computer ScienceComputer Science (R0)