有界图灵机的对称性与转移

我们考虑通过对称性考量反复推广有限状态自动机定义所给出的结构，并在每一步构造转移幺半群的类似物。该方法首先给出非确定自动机，然后是（非确定）双向自动机与有界图灵机——即读写头无法移过输入词末尾的图灵机。在双向自动机情形，转移幺半群推广为紧闭范畴中的自同态幺半群。这些利用 Girard 的分辨率公式（来自线性逻辑的博弈几何表示）来构造单例词的图像。在有界图灵机情形，转移同态推广为从自然数到由紧闭范畴的自同态幺半群之并连同适当复合所构造的幺半群的同态。这些利用 Girard 的执行公式（同样来自线性逻辑的博弈几何表示）来构造单例的图像。