Agda 中的名义集——一项新颖且不成熟的机械化

在本文中，我们展示了当前关于 Agda 中名义集新形式化的发展。我们再次进行形式化的首要动机是更好地理解名义集，并拥有一个用于测试基于名义逻辑的类型系统的试验场。不出所料，我们独立构建了通向名义集的同一类型层级。我们在有限置换的构想上与其他形式化不同：在我们的形式化中，有限置换是一个定义域有限的置换（即双射）。有限置换有不同的表示方式，例如作为对换的复合（其他形式化中的主流方式）或不相交循环的复合。我们证明了这些表示是等价的，并用它们来规范化（直至独立对换复合顺序）对换的复合。