Formal proofs of operator identities by a single formal computation

A formal computation proving a new operator identity from known ones is, in principle, restricted by domains and codomains of linear operators involved, since not any two operators can be added or composed. Algebraically, identities can be modelled by noncommutative polynomials and such a formal computation proves that the polynomial corresponding to the new identity lies in the ideal generated by the polynomials corresponding to the known identities. In order to prove an operator identity, however, just proving membership of the polynomial in the ideal is not enough, since the ring of noncommutative polynomials ignores domains and codomains. We show that it suffices to additionally verify compatibility of this polynomial and of the generators of the ideal with the labelled quiver that encodes which polynomials can be realized as linear operators. Then, for every consistent representation of such a quiver in a linear category, there exists a computation in the category that proves the corresponding instance of the identity. Moreover, by assigning the same label to several edges of the quiver, the algebraic framework developed allows to model different versions of an operator by the same indeterminate in the noncommutative polynomials.     

基于线性规划的高温超导磁体线圈设计方法

电子真空回旋器件是一种对磁场精度要求较高的微波源装置, 一般采用超导磁体提供磁场环境. 超导磁体的应用中, 磁场分布的实现是超导磁体设计的核心问题. 提供回旋器件磁场的高温超导磁体包含较复杂的磁体绕组, 为了解决此类设计计算问题, 本文提出了一种包含设计区域约束的线性优化方法进行回旋器件高温超导绕组的设计优化, 通过分步的约束和线性优化计算, 可得到同时满足设计要求和绕组可实现的设计磁场电流分布设计. 计算实例的结果给出了一个提供磁场强度1 .3 Tesla, 长度285 mm 的均匀磁场区域, 同时满足多位置的磁场要求, 设计结果与要求一致度较好, 精度满足应用需求. 该计算方法是一种可适用于较复杂磁场要求和超导绕组结构的设计优化方法.     

曲面相机阵列多分辨成像方法

针对现有成像系统因数据冗余而无法兼顾大视场、高分辨、高效性的问题,结合人眼视网膜变分辨成像和并列式复眼成像原理,设计一种多分辨率成像的复合仿生成像系统.该成像系统按照球面和平面兼顾的曲面布局方式,利用11个相机镜头构建相机阵列,组成了四个等级分辨率的子眼拍摄模块.通过物距100 m的远景实验和物距10 m的近景实验发现,该系统在实现高分辨成像的同时,获得总视场达150.8°×37.8°.多分辨率成像实验结果表明,该系统获取的图像的分辨率从中心视场到边缘视场逐渐降低,并且相较于中心清晰全视场成像,四级分辨率成像的拼接图像数据量减少了17.2倍的数据冗余.     

用于SCA ASIC测试的数字读出模块设计

高速开关电容阵列(SCA)具有高速采样、低功耗的特点,基于SCA的高速波形数字化是目前高精度时间测量的一个重要研究方向。为此,我们开展SCA芯片的研究,目前已设计完成原型ASIC设计,并正在进行后续版本的改进设计。为便于未来多版本ASIC的测试和评估,需设计具有一定通用性的数字读出模块,本论文工作主要介绍此模块的设计工作以及相应的数据读出软件。数字读出模块基于FPGA实现对待测ASIC的控制、配置及数据读出,采用DDR3片外存储芯片,使用USB3.0等接口进行数据传输;上位机软件基于Python3.7设计,实现了数据采集与波形绘制等功能。目前已使用设计完成的数字读出模块对第2版SCA ASIC进行了初步的测试,测试结果表明,此读出模块工作正常,且SCA芯片输出结果符合预期。