Visible acyclic differential nets, Part I: Semantics

We give a geometric condition that characterizes the differential nets having a finitary interpretation in finiteness spaces: visible acyclicity. This is based on visible paths, an extension to differential nets of a class of paths we introduced in the framework of linear logic nets. The characterization is then carried out as follows: the differential nets having no visible cycles are exactly those whose interpretation is a finitary relation. Visible acyclicity discloses a new kind of correctness for the promotion rule of linear logic, which goes beyond sequent calculus correctness.

► We give a geometric condition that characterizes the differential nets having a finitary interpretation in finiteness spaces.
► This condition is based on visible paths, an extension to differential nets of a class of paths we introduced in the framework of linear logic nets.
► We prove that the differential nets having no visible cycles are exactly those whose interpretation is a finitary relation.