{"id":589,"date":"2008-01-30T13:26:17","date_gmt":"2008-01-30T13:26:17","guid":{"rendered":"http:\/\/scientopia.org\/blogs\/goodmath\/2008\/01\/30\/what-makes-linear-logic-linear\/"},"modified":"2008-01-30T13:26:17","modified_gmt":"2008-01-30T13:26:17","slug":"what-makes-linear-logic-linear","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2008\/01\/30\/what-makes-linear-logic-linear\/","title":{"rendered":"What makes linear logic linear?"},"content":{"rendered":"

Sorry for the lack of posts this week. I’m traveling for work, and
\nI’m seriously jet-lagged, so I haven’t been able to find enough time
\nor energy to do the studying that I need to do to put together a solid
\npost.<\/p>\n

Fortunately, someone sent me a question that I can answer
\nrelatively easily, even in my jet-lagged state. (Feel free to ping me with more questions that can turn into easy but interesting posts. I appreciate it!)<\/p>\n

The question was about linear logic: specifically, what makes
\nlinear logic linear<\/em>?<\/p>\n

<\/p>\n

For those who haven’t ever seen it before, linear logic is based
\non the idea of resource consumption. Where the normal propositional or
\npredicate logics that most of us are familiar with are focused around an
\nidea of truth<\/em>, linear logic is focused on the idea of resource
\nposession and consumption. In standard propositional logic, if you’re given
\nthe proposition “A”, that means that A is true, and you can use the truth
\nof A in as many inferences as you want. In linear logic, if you’re given
\nthe proposition “A”, that means that you possess one instance of A,
\nand you can use it, once<\/em>, in an inference.<\/p>\n

Think of a conventional logic, like simple propositional
\nlogic. Imagine that you had the following statements:<\/p>\n

    \n
  1. A <\/li>\n
  2. A ⇒ B<\/li>\n
  3. A ⇒ C<\/li>\n<\/ol>\n

    If you’re working in normal propositional logic, then you can use
    \nthose statements to infer some more facts. Given “A”, and knowing “A
    \n⇒ B”, you can infer B; and given “A”, and knowing “A ⇒ C”,
    \nyou can infer C. So given those three statements, we can infer that A
    \nand B and C are all true.<\/p>\n

    In linear logic, if you start with the equivalent of those three
    \nstatements, you can infer either<\/em> B or C, but not both: using
    \n“A” in an inferences consumes<\/em> it. So once you use it, it’s
    \ngone, and you can’t use it again.<\/p>\n

    I’m not going to go into detail about linear logic here; I’ve written
    \nabout it before, and if you’re interested, you can go look at that post.<\/a> I’m just going
    \nto quickly walk through one simple example of how it’s used, and then go back to
    \nthe original question.<\/p>\n

    Pretty much every introduction to linear logic that I’ve ever seen uses the same
    \nfirst example: a vending machine. Suppose you want to describe how a vending machine
    \nworks. For example, if I put 6 quarters into a soda machine, I get a soda. The key thing
    \nthat I want to capture is when I get the soda, the quarters are gone<\/em>. I had
    \nto give them up to get back the soda. In linear logic, I can write that as an
    \nimplication:<\/p>\n

    Quarter ⊗ Quarter ⊗ Quarter ⊗ Quarter ⊗ Quarter ⊗ Quarter -o Soda<\/p>\n

    “⊗” means simultaneous possession: “A ⊗ B” means “I have an A and a B at the same time”; “-o” is linear implication, “A -o B” means “I can give up an A to get a B”. So the expression above means that if I have six quarters, I can give them up and get a soda.<\/p>\n

    Try to think about what you’d need to do in conventional predicate
    \nlogic to say that. You’d need to introduce a notion of counting, and addition and subtraction,
    \nand possession, and consumption. It would be quite difficult – and the result would be a lot
    \nharder to analyze, because it would rely on at least some amount of arithmetic. Linear logic makes things like that really easy.<\/p>\n

    It should also be pretty obvious why computer scientists – and in
    \nparticular, programming language designers – are so interested in
    \nlinear logic. In implementing software, managing resources is always a
    \nmajor issue. You can use linear logic in tools that analyze memory
    \nusage, or management of resources like files. You can use linear
    \nlogic-based analysis and inference in a functional language compiler
    \nto figure out when you can convert an allocation into an in-place
    \nupdate. It’s incredibly useful.<\/p>\n

    But getting back to the question: why is it linear?<\/p>\n

    There’s a bunch of different ways to explain it. I’m going to use
    \none that’s informal, but easy to understand. Most logicians would hate
    \nit as an explanation, but it’s easy.<\/p>\n

    In linear logic, simultaneous posession of resources is treated as a kind of
    \nmultiplication. If I have A and B at the same time, I can say that I have A*B.<\/p>\n

    Now, suppose that each distinct proposition that we can use in an
    \ninference has a unique label, so that we can distinguish them. Then
    \nfor any sequence of inferences, we can describe the inference cost –
    \nthat is, the set of resources consumed by those inferences via a
    \nmultiplicative expression. So for my example above with the vending
    \nmachine, I can say that the six quarters are named
    \nQuartera<\/sub>, Quarterb<\/sub>, Quarterc<\/sub>,
    \nQuarterd<\/sub>, Quartere<\/sub>, and Quarterf<\/sub>.<\/p>\n

    Then, to get a soda, I need to spend the six quarters. The inference cost
    \nwill be Quartera<\/sub>*Quarterb<\/sub>*Quarterc<\/sub>*Quarterd<\/sub>*
    \nQuartere<\/sub>*Quarterf<\/sub>.<\/p>\n

    In linear logic, the inference cost is always a linear equation.<\/p>\n

    Compare that to conventional propositional logic. In the example
    \nat the beginning of this post, I used A twice to infer B and C. So the
    \ninference cost there is A2<\/sup> – it’s quadratic. I can’t do that in
    \nlinear logic.<\/p>\n","protected":false},"excerpt":{"rendered":"

    Sorry for the lack of posts this week. I’m traveling for work, and I’m seriously jet-lagged, so I haven’t been able to find enough time or energy to do the studying that I need to do to put together a solid post. Fortunately, someone sent me a question that I can answer relatively easily, even […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[33],"tags":[],"class_list":["post-589","post","type-post","status-publish","format-standard","hentry","category-logic"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-9v","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/589","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=589"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/589\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=589"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=589"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=589"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}