发表机构
Imperial College London; Lancaster University（帝国理工学院; 兰卡斯特大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文在Lean证明助手中形式化微波模拟计算网络，证明其充要条件及任意2的幂次DFT的可实现性。
AI 中文摘要
利用微波信号进行模拟计算，可以在信号通过微波网络传播时，直接在模拟域执行线性变换。一个基本问题是，给定一组微波组件，能够计算哪些变换。在我们之前的工作中，我们通过推导这些网络能够计算的变换的充要条件，回答了关于由混合耦合器和移相器组成的网络的问题，并证明了离散傅里叶变换（DFT）满足该条件。在本文中，我们迈出了在Lean中形式化微波模拟计算的第一步，Lean是一种编程语言和证明助手，在数学领域日益被采用。我们形式化了所考虑的组件、它们的串联和并联连接，以及它们能够实现的网络类别。然后，我们正式证明了表征这些网络的充要条件，以及任意大小为2的幂的DFT的可实现性。所有证明均由Lean内核检查，代码公开于：此https URL。
英文摘要
Analog computing with microwave signals can perform linear transformations directly in the analog domain, as the signals propagate through a microwave network. A fundamental question is which transformations can be computed with a given set of microwave components. In our previous work, we answered this question for networks of hybrid couplers and phase shifters by deriving a necessary and sufficient condition on the transformations these networks can compute, and we showed that the discrete Fourier transform (DFT) satisfies it. In this paper, we take a first step toward the formalization of analog computing with microwaves in Lean, a programming language and proof assistant that is increasingly adopted in mathematics. We formalize the considered components, their series and parallel connections, and the class of networks they can implement. Then, we formally prove the necessary and sufficient condition characterizing these networks, as well as the implementability of the DFT of any size power of two. All proofs are checked by the Lean kernel, and the code is openly available at: https://github.com/matteonerini/formalizing-analog-computing.
CommentsSubmitted to IEEE for publication
