ludics 中的具现化与路径的最大团

Ludics 是以交互为原始概念对逻辑的重构，其意义在于主要的逻辑概念不再是公式和证明，而是被解释为称为设计 (designs) 的对象之间交互的割消去 (cut-elimination)。当两个设计之间的交互顺利进行时，称这两个设计是正交的。行为 (behaviour) 是在双正交下封闭的设计集合。逻辑公式随后由行为表示。最后，证明被解释为满足特定性质的设计。通过这种方式，设计比证明更通用，我们特别注意到它们不是有类型的对象。Girard 在 Ludics 中引入了具现化 (incarnation)，作为对行为中“有用”设计的刻画。设计的具现化定义为该设计中在包含序下行为中最小的子设计。它特别有用，因为成为“具现化的”是设计表示公式证明的条件之一。具现化的计算也很重要，因为它为公式乃至更一般的行为提供了最小指称。我们在此给出了一种构造性方法来捕捉一组设计的行为的具现化，而无需计算行为本身。我们采用的方法使用了设计的替代定义：我们将设计视为路径集合，而不是年表 (chronicles) 集合；这一概念非常接近博弈语义中的对弈 (play)，使得交互的处理更加容易：交互的展开是两个交互设计共有的路径。