| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 4662330 | Annals of Pure and Applied Logic | 2012 | 28 Pages |
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.
