题目：量子λ演算及其语义的研究

量子λ演算是一种函数式的量子程序设计语言。为了便于控制并使用量子计算机，必须通过量子程序设计语言来描述待解问题，因此量子程序设计语言将作为未来通用量子计算机上的一种重要软件系统。量子程序设计语言近年来发展非常迅速。这个领域的研究包括基于量子计算的程序语言的设计，分为命令式的和函数式的语言；量子语言语义的研究；编译量子程序设计语言等。本文研究量子λ演算及其语义，并且主要针对其范畴语义做了深入研究。目的是利用范畴给出量子语言的指称语义。对于量子λ演算，本文分析了其优点以及当前研究者所设计的量子λ演算；对于范畴语义，在总结了利用范畴结构为量子程序设计语言提供指称语义所取得的成果之后，文中首先研究了一个范畴量子逻辑，它是与带双积的强紧闭范畴对应的序列演算。这个演算解释在由给定的对合范畴所生成的自由的带双积的强紧闭范畴中。而且这样的语义关于cut elimination归约是可靠的，对带双积的强紧闭范畴是完备的。最后考虑了范畴结构的图解演算，并且利用图解演算表达了范畴量子逻辑的乘性部分。