一句话：为 opetopes 与 opetopic 集提出纯语法的矢列演算，并证明良类型 opetope 与传统定义一一对应。
Opetopes 是刻画高维复合的代数形状，为弱 ω-范畴等高等代数结构提供基础。传统定义通过自由 operad 或 zoom complex 等抽象构造归纳给出，难以在计算机中直接操作。本文为 opetopes 与 opetopic 集引入一种纯语法的矢列演算，用类型规则描述其构造与组合。主要结果是：该演算中良类型的 opetopes 与传统方式定义的 opetopes 之间存在双射，从而在语法层面忠实刻画原有结构。作者期望这一结构可作为基于 opetopes 的机器化工具的自然基础。
Opetopes are algebraic descriptions of shapes corresponding to compositions in higher dimensions. As such, they offer an approach to higher-dimensional algebraic structures, and in particular, to the definition of weak ω-categories, which was the original motivation for their introduction by Baez and Dolan. They are classically defined inductively (as free operads in Leinster's approach, or as zoom complexes in the formalism of Kock et al.), using abstract constructions making them difficult to manipulate with a computer. Here, we present a purely syntactic description of opetopes and opetopic sets as a sequent calculus. Our main result is that well-typed opetopes in our sense are in bijection with opetopes as defined in the more traditional approaches. We expect that the resulting structures can serve as natural foundations for mechanized tools based on opetopes.