一句话:刻画 Ludics 中 behaviour 的可访问路径集合,给出闭合与饱和条件,并用于显式构造由常量和乘法/加法连接词生成的行为。
本文研究 Girard 的 Ludics 中 behaviour 的构造与性质。Ludics 中 design 是形式证明的抽象,保留 cut elimination 的动态信息;behaviour 对应类型或逻辑公式,是 design 的闭集。论文把 design 视为相干路径集合,围绕 visitable path 展开:它可经由与正交集合交互而穿过。论文回答路径集合何时恰为某 behaviour 的全体 visitable paths:该集合及对偶需前缀闭合、daimon 闭合并满足两条饱和性质。由此无需显式计算正交或闭包即可定义给定 design 集合的全部 visitable paths。最后应用结果刻画出由常量和乘法/加法连接词生成的 behaviour,并提出 oriented tensor 及其基本性质。
Around 2000, J.-Y. Girard developed a logical theory, called Ludics. This theory was a step in his program of Geometry of Interaction, the aim of which being to account for the dynamics of logical proofs. In Ludics, objects called designs keep only what is relevant for the cut elimination process, hence the dynamics of a proof: a design is an abstraction of a formal proof. The notion of behaviour is the counterpart in Ludics of the notion of type or the logical notion of formula. Formally a behaviour is a closed set of designs. Our aim is to explore the constructions of behaviours and to analyse their properties. In this paper a design is viewed as a set of coherent paths. We recall or give variants of properties concerning visitable paths, where a visitable path is a path in a design or a set of designs that may be traversed by interaction with a design of the orthogonal of the set. We are then able to answer the following question: which properties should satisfy a set of paths for being exactly the set of visitable paths of a behaviour? Such a set and its dual should be prefix-closed, daimon-closed and satisfy two saturation properties. This allows us to have a means for defining the whole set of visitable paths of a given set of designs without closing it explicitly, that is without computing the orthogonal of this set of designs. We finally apply all these results for making explicit the structure of a behaviour generated by constants and multiplicative/additive connectives. We end by proposing an oriented tensor for which we give basic properties.