透过可访问路径研究行为
摘要：在2000年左右，J.-Y. Girard开发了一种名为Ludics的逻辑理论。该理论是他的Geometry of Interaction计划的一步，其目标是解释逻辑证明的动态。在Ludics中，称为设计的对象只保留了削减过程以及证明的动力学所需的内容，因此设计是形式证明的抽象。行为的概念在Ludics中相当于类型的概念或逻辑公式的概念。形式上，行为是一组闭合的设计。我们的目标是探索行为的构造并分析其属性。在本文中，设计被视为一组一致的路径。我们回顾或提供了关于可访问路径的性质的变体，其中可访问路径是设计或一组可通过与一组的正交设计交互而遍历的路径。然后，我们能够回答以下问题：为了恰好成为一个行为的可访问路径集，一组路径应该满足哪些性质？这样的一组路径及其对偶应该是前缀闭合的、Daimon闭合的，并满足两个饱和性质。这使我们能够定义给定设计集合的全部可访问路径集，而无需显式地关闭它，即无需计算该设计集合的正交集。最后，我们将所有这些结果应用于明确生成由常量和乘法/加法连接词产生的行为的结构。我们最后提出了一个有向张量，并给出了其基本属性。
作者：Christophe Fouquer''e and Myriam Quatrini
论文ID：1403.3772
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22