Куклев пишет на фесбуке про линейную логику

[juan_gandhi]

src

After many years I finally have an intuitive understanding of linear logic operators.

The λλ̃-calculus by V. Choudhury et al. shows how to understand the multiplicative disjunction A ⅋ B, while the Verse calculus by SPJ et al. shows how to understand the multiplicative exponential ?A.

A × B — tuple

A ⅋ B — junction (employing terminology by Larry Wall)

A + B — producer-controlled alternative

A & B — consumer-controlled alternative

!A — factory producing A's, in particular

!A = 𝟘 & A & A × A & A × A & ···

?A — junction of any number of A's, in particular

?A = ⊥ + A + A ⅋ A + A ⅋ A ⅋ A + ···

All variables in Verse calculus are secretly of the kind ?T, where T is a cartesian type. So, one can even assume they are ?!X.

Comments

[juan_gandhi]

Sounds reasonable.