Affine logic
Affine logic is a substructural logic that denies the structural rule of contraction. It can also be characterized as linear logic with weakening. V. N. Grishin introduced it in 1974[1], after observing that Russell's paradox cannot be derived without contraction (e.g. in the naive set-theoretic sequent calculus).
Affine logic can be embedded into linear logic by rewriting the affine arrow as the linear arrow .
Whereas full linear logic (ie. linear logic with multiplicatives, additives and exponentials) is undecidable, full affine logic is decidable.
Affine logic forms the foundation of ludics.
References
- Gianluigi Bellin, 1991. 'affine logic'. Message to the TYPES mailing list.
- Jean-Yves Girard, 1997. 'Affine'. Message to the TYPES mailing list.
- ^ "A non standard logic and its application to set theory", Investigations in formalized language and non-classical logics. [ Ob odnoy njestandartnoy logike i ee primenjenii k tjeorii mnozhestv, Issledovania po formalizovannym jazykam i neklasitcheskim logikam, Izdavateljstvo Nauka (1974)]
See also
 | This logic-related article is a stub. You can help Wikipedia by expanding it. |
 |