功能编程语言的现代理论使用单子来编码计算侧面的ff ect和侧视上下文,而超越了骨头程序逻辑。即使量子计算本质上是侧面的ff ectful(如量子测量)和上下文依赖性的(如在混合辅助状态下),但以前几乎没有对量子编程语言的支持。在这里,我们在参数化模块光谱类别上系统地分析了(CO)单元,该类别是由Grothendieck的“动机瑜伽”诱导的 - 对于当前目的而言,专门针对H C模型,并在设置索引复杂的矢量空间中进行了进一步的目的,如在同伴文章[SS23-EOS]中所讨论的。将索引矢量空间解释为量子测量结果参数的替代量子状态空间的集合,正如原始词语 - 语义上所熟悉的那样,我们发现这些(CO)单子为具有经典测量结果的“动力提升”的“动力提升”的综合自然语言提供了一种综合的自然语言。我们通过指示特异性的量子编程语言(QS)来结束,该语言(QS)在透明的do中表达了这些单调的量子e ff ects,可嵌入到最近构建的线性同拷贝类型理论(LHOTT)中,该理论(LHOTT)将其解释为参数化模块光谱。一旦嵌入了Lhott,这应该使具有线性量子类型,经典控制,动态提升的正式可验证的通用量子编程,尤其是与拓扑e ff ects(如伴侣文章[TQP]中所述)。
主要关键词