Qué significa ⊸
Se gasta el recurso A para obtener B.
La lógica lineal es una forma de razonar que lleva la cuenta de los recursos: una premisa no se puede reutilizar ni descartar sin más. En A ⊸ B, aplicar la implicación consume A para producir B.
Jean-Yves Girard introdujo la lógica lineal en 1987; en su notación, ⊸ representa la implicación lineal.
Notación especializada de lógica lineal y de sistemas de tipos de programación que controlan el uso de recursos.
No lo leas como un simple «si A, entonces B»: al usarlo, se gasta A.
Preguntas frecuentes
1¿⊸ es lo mismo que →?
No. En la lógica lineal, ⊸ lleva la cuenta del uso de un recurso; → por sí solo no incluye esa regla. Fuera de un contexto claramente definido de lógica lineal, sigue las definiciones del autor.
Cómo escribir ⊸
⊸\22B8Códigos y codificaciónPuntos de código: 1
Un símbolo visible puede contener varios puntos de código. JS .length cuenta unidades UTF-16; UTF-8 cuenta bytes.