一句话：在 Weihrauch 类型二效应性下，为量子力学基本数据结构建立可计算性，并证明有效版 von Neumann 谱定理。
本文研究量子力学基本概念在可计算性意义下的可表示性。量子态与可观测量通常定义在可分无限维 Hilbert 空间 ℋ 及其闭线性子空间格 ℒ 上，可表述为某种测度。作者采用 Weihrauch 的类型二效应性（TTE）框架，不直接构造可容许表示，而是证明相关数据类型都位于范畴 QCB0 中；该范畴与可容许表示及连续可实现映射构成的范畴 AdmRep 等价，从而获得可计算性。对可观测量，作者以 valuation 替代 measure，并证明 von Neumann 谱定理的有效版本。结果表明这些量子力学数据结构具有良好可计算性。
The basic notions of quantum mechanics are formulated in terms of separable infinite dimensional Hilbert space $\mathcal{H}$. In terms of the Hilbert lattice $\mathcal{L}$ of closed linear subspaces of $\mathcal{H}$ the notions of state and observable can be formulated as kinds of measures as in [21]. The aim of this paper is to show that there is a good notion of computability for these data structures in the sense of Weihrauch's Type Two Effectivity (TTE) [26]. Instead of explicitly exhibiting admissible representations for the data types under consideration we show that they do live within the category $\mathbf{QCB}_0$ which is equivalent to the category $\mathbf{AdmRep}$ of admissible representations and continuously realizable maps between them. For this purpose in case of observables we have to replace measures by valuations which allows us to prove an effective version of von Neumann's Spectral Theorem.
@article{paperbot401,
title = {Computability in Basic Quantum Mechanics},
author = {Eike Neumann and Martin Pape and Thomas Streicher},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 2},
year = {2018},
doi = {10.23638/lmcs-14(2:14)2018}
}