Affine logic: Difference between revisions
Content deleted Content added
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
A [[substructural logic]] that denies the [[structural rule]] of [[contraction]]. It can also be characterized as [[linear logic]] with [[weakening]]. |
A [[substructural logic]] that denies the [[structural rule]] of [[contraction]]. It can also be characterized as [[linear logic]] with [[weakening]]. |
||
Affine logic can be embedded into linear logic |
Affine logic can be embedded into linear logic by rewriting the affine arrow <math>A \rightarrow B</math> as the linear arrow <math>A {-\!\circ} B \otimes \top</math>. |
||
* globally, by rewriting the affine arrow ''A → B'' as ''A ⊸ B ⊗ ⊤''. |
|||
* locally, by rewriting ''A → B'' as ''A & 1 ⊸ B''. |
|||
Affine logic forms the foundation of [[ludics]]. |
Affine logic forms the foundation of [[ludics]]. |
||
Revision as of 21:12, 31 May 2004
A substructural logic that denies the structural rule of contraction. It can also be characterized as linear logic with weakening.
Affine logic can be embedded into linear logic by rewriting the affine arrow as the linear arrow .
Affine logic forms the foundation of ludics.