Discussion: Taste of Linear Logic
Comment on Philip Wadler's paper "A Taste of Linear Logic", or raise a question.

How does this logic relate to memory management? Is there a relationship between linear logic and the way, say, Rust handles memory management? It seems like garbage collection at compiletime would be a great application of linear logic.

Is there a rule of thumb when to use intuitionistic logic and linear logic in real systems? Is it only when copying information is impossible/inefficient?

I went through most of the rules. I just curious about what's the difference between the assumption in different logic?

Why would somebody need Fixpoints? Is there a specific class of computable functions that can't be expressed in typed term calculus?

The argument that linear logic is strictly more expressive than intuitionistic logic is convincing. However, I don't fully understand what form that extra expressivity takes in the world of types; it seems to lie in the
!t
andcase s of !x → u
productions of section 5's term grammar, but I'm having trouble grokking it. 
"As we shall see, an assumption of the form ⟨!A⟩ is in a sense equivalent to an assumption of the form [A]. However, they differ in that a linear assumption – even one of the form ⟨!A⟩ – must be used exactly once in a proof, while an intuitionistic assumption may be used any number of times." I don't really understand this. How do you "use up" ⟨!A⟩

Please register or sign in to post a comment