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

[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

[sassa_nf]

That's one guy with untapped skill of explaining things.

But in this case I don't understand "consumer"/"producer" notion.

[juan_gandhi]

I agree, pretty weird and unexpected. Maybe we should ask him?

I especially enjoyed explanation of ! andc ? via free and cofree(?).

[sassa_nf]

here we go, the answer is: this is linear logic, so A&B is decided whether it is A or B at the time the value is accessed, and A+B - it is decided whether it is A or B at the time it is constructed.