重写上下文无关的弦图族

弦图提供了一个方便的图形框架，可用于对幺半范畴的态射进行等式推理。然而，与项重写不同，重写弦图可以得到更短的等式证明，因为弦图的图形表示允许我们在模掉任何由幺半结构导出的重写步骤后正式建立等式。手动操作弦图是一个耗时且容易出错的过程，尤其是对于大型弦图。这可以通过使用诸如 Quantomatic 之类的软件证明助手来改善。然而，对具体弦图进行推理可能具有局限性，并且在某些情况下，有必要对整个（无限）弦图族进行推理。这样做时，我们面临着与操作具体弦图相同的问题，但此外，如果我们在表示（无限）弦图族的方式上不够精确，就有可能犯更多错误。本论文的主要目标是设计一个适用于计算机自动化的、用于对无限弦图族进行等式推理的数学框架。我们将处理上下文无关的弦图族，并使用上下文无关图文法来表示它们。我们将使用上下文无关文法之间的重写规则来建模无限图族之间的等式。我们的框架分别使用图上的双推出重写和上下文无关图文法来表示关于具体弦图和上下文无关弦图族的等式推理。我们将通过证明它尊重弦图推理的具体语义来证明我们的表示是可靠的，并且我们将通过证明重要的可判定性性质来证明我们的框架适合软件实现。