Incarnation in ludics and maximal cliques of paths (Q2851674)

This paper is a contribution to ludics' computation of incarnation. More precisely, it provides a constructive method to calculate the incarnation of the behaviour generated by a set of designs, without the need to determine the behaviour itself.\newline Ludics is a framework proposed by \textit{J.-Y. Girard} [Math. Struct. Comput. Sci. 11, No. 3, 301--506 (2001; Zbl 1051.03045)] which allows to rebuild logic from the interaction between designs. We can think of a design as a kind of abstract cut-free proof. In ludics there is no distinction between syntax and semantics. A design represents not only an abstraction of a formal proof but also its semantics interpretation. When the interaction between two designs terminates (the result is a special action called daimon), the two designs are said to be orthogonal. A set of designs closed by bi-orthogonality is called a behaviour. Behaviours are the ludics counterpart of types/formulas. Proofs are designs with specific properties. One of these properties is being incarnated. Incarnation plays an important role in ludics. The incarnation of a design \(\mathfrak{D}\) in a behaviour \(\mathbf{G}\) is the smallest design \(\mathfrak{D'}\) in \(\mathbf{G}\) which is contained in \(\mathfrak{D}\). The incarnation of a behaviour is the set of its incarnated (also known as material) designs. Incarnation gives a minimal denotation for a behaviour and in particular for a type/formula. For more on ludics and its concepts see [\textit{J.-Y. Girard}, Proof and system-reliability. Dordrecht: Kluwer Academic Publishers. 167--211 (2002; Zbl 1056.03034); Bull. Symb. Log. 9, No 2, 131--168 (2003; Zbl 1056.03035)].\newline The present paper defines designs in an alternative (equivalent) way: instead of sets of chronicles, as in the original definition, designs are presented as sets of paths. With this reformulation, the unfolding of an interaction is a path common to two interacting designs. Given a set of designs \(E\), the authors managed to characterize the paths in \(E\) that are visitable by interaction. Moreover, they managed to directly compute the incarnation of the dual of \(E\) (particular maximal cliques of visitable paths). A two-step procedure (computing twice the incarnation of the dual) allows computing the incarnation of the behaviour generated by \(E\), without necessarily computing explicitly the behaviour itself.