Same. I’m also not understanding how the two parts are supposed to relate. But the first part seems very good. The WP article is giving me the impression that it’s like boolean logic with an imaginary unit??? (You might recall from general Rust exposure that conservation of mass should somehow play a role as well.) Wikipedia, and Girard’s paper, have proven unhelpful to me; I am hoping that the lecture notes of this course will get me somewhere.
In intuitionistic logic you describe propositions as what is a proof for a proposition. We can apply this to type theory. For example: proof for proposition ‘Nat’ would be 0, or 1, or 2. Linear logic further distinguishes propositions by describing what is a refutation for a proposition.
A better explanation for LL might deserve its own post. Still I improved the example proof a bit. I even found a bug in the definition of the palindrome.
So you’re saying… we don’t know where to GOTO unless we know where we’ve COMEFROM?
(apologies to R. Lawrence Clark)
Shouldn’t it be
if i = 10 then goto A3 else goto A2?I specifically did take caution to not do this and still got it wrong. Thanks for pointing it out.
I was following it up until the linear logic part; I think the first principles of LL could be explained better here.
Same. I’m also not understanding how the two parts are supposed to relate. But the first part seems very good. The WP article is giving me the impression that it’s like boolean logic with an imaginary unit??? (You might recall from general Rust exposure that conservation of mass should somehow play a role as well.) Wikipedia, and Girard’s paper, have proven unhelpful to me; I am hoping that the lecture notes of this course will get me somewhere.
While ago I learnt from Pfenning’s course notes. There’s this constructive logic course.
In intuitionistic logic you describe propositions as what is a proof for a proposition. We can apply this to type theory. For example: proof for proposition ‘Nat’ would be 0, or 1, or 2. Linear logic further distinguishes propositions by describing what is a refutation for a proposition.
A better explanation for LL might deserve its own post. Still I improved the example proof a bit. I even found a bug in the definition of the palindrome.