Affine logic

Affine logic is a substructural logic whose proof theory rejects the structural rule of contraction. It can also be characterized as linear logic with weakening.

The name "affine logic" is associated with linear logic, to which it differs by allowing the weakening rule. Jean-Yves Girard introduced the name as part of the geometry of interaction semantics of linear logic, which characterises linear logic in terms of linear algebra; here he alludes to affine transformations on vector spaces.[1]

Affine logic predated linear logic. V. N. Grishin used this logic in 1974,[2] after observing that Russell's paradox cannot be derived in a set theory without contraction, even with an unbounded comprehension axiom.[3] Likewise, the logic formed the basis of a decidable subtheory of predicate logic, called 'Direct logic' (Ketonen & Wehrauch, 1984; Ketonen & Bellin, 1989).

Affine logic can be embedded into linear logic by rewriting the affine arrow as the linear arrow .

Whereas full linear logic (i.e. propositional linear logic with multiplicatives, additives and exponentials) is undecidable, full affine logic is decidable.

Affine logic forms the foundation of ludics.

Notes
  1. Jean-Yves Girard, 1997. 'Affine'. Message to the TYPES mailing list.
  2. Grishin, 1974, and later, Grishin, 1981.
  3. Cf. Frederic Fitch's demonstrably consistent set theory
gollark: > In the early 1990s, O'Sullivan led a team at the CSIRO which patented, in 1996, the use of a related technique for reducing multipath interference of radio signals transmitted for computer networking. This technology is a part of all recent WiFi implementationsAh, so they contributed somewhat to WiFi.
gollark: CSIRO, that is.
gollark: It says that they came up with some sort of Fourier-transform-based thing used in the signalling?
gollark: I'm trying to confirm what you said about WiFi there.
gollark: I think that's America-based?

References
  • V.N. Grishin, 1974. “A nonstandard logic and its application to set theory,” (Russian). Studies in Formalized Languages and Nonclassical Logics (Russian), 135–171. Izdat, “Nauka,” Moskow. .
  • V.N. Grishin, 1981. “Predicate and set-theoretic calculi based on logic without contraction rules,” (Russian). Izvestiya Akademii Nauk SSSR Seriya Matematicheskaya 45(1):47-68. 239. Math. USSR Izv., 18, no.1, Moscow.
  • Ketonen and Weyhrauch, 1984, A decidable fragment of predicate calculus. Theoretical Computer Science 32:297-307.
  • Ketonen and Bellin, 1989. A decision procedure revisited: notes on Direct Logic. In Linear Logic and its Implementation.

See also


This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.