Various physical constraints limit the number of qubits that can be implemented in a single quantum processor, and thus it is necessary to connect multiple quantum processors via quantum interconnects. While several compiler implementations for interconnected quantum computers have been proposed, there is no suitable representation as their compilation target. The lack of such representation impairs the reusability of compiled programs and makes it difficult to reason formally about the complicated behavior of distributed quantum programs. We propose InQuIR, an intermediate representation that can express communication and computation on distributed quantum systems. InQuIR has formal semantics that allows us to describe precisely the behaviors of distributed quantum programs. We give examples written in InQuIR to illustrate the problems arising in distributed programs, such as deadlock. We present a roadmap for static verification using type systems to deal with such a problem. We also provide software tools for InQuIR and evaluate the computational costs of quantum circuits under various conditions. Our tools are available at https://github.com/team-InQuIR/InQuIR.
翻译:各种物理限制限制了在单一量子处理器中可以执行的量子处理器数量,因此有必要通过量子互连将多个量子处理器连接起来。 虽然已经提出了数个相连量子计算机的编译器实施建议,但并没有适当的表述作为编译目标。 缺乏这种表述方式会损害编集的量子程序的可重复性,并使得难以正式解释分布量子程序的复杂行为。 我们建议InQuIR是一个中间代表,可以表达分布量子系统的通信和计算。 InQuIR有正式的语义,使我们能够准确地描述分布量子程序的行为。 我们用 InQIR 中写的例子来说明分布式程序中出现的问题,例如僵局。 我们提出了使用类型系统进行静态核查以解决这类问题的路线图。 我们还为InQIR提供软件工具,并在各种条件下评估量子电路的计算成本。我们的工具可在https://github.com/team-InQuIR/InuIR/InuIR上查阅。