{"id":93,"date":"2006-07-31T14:25:10","date_gmt":"2006-07-31T14:25:10","guid":{"rendered":"http:\/\/scientopia.org\/blogs\/goodmath\/2006\/07\/31\/the-categorical-model-of-linear-logic\/"},"modified":"2006-07-31T14:25:10","modified_gmt":"2006-07-31T14:25:10","slug":"the-categorical-model-of-linear-logic","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2006\/07\/31\/the-categorical-model-of-linear-logic\/","title":{"rendered":"The Categorical Model of Linear Logic"},"content":{"rendered":"

Today we’ll finally get to building the categories that provide the model for
\nthe multiplicative linear logic. Before we jump into that, I want to explain why it is that we separate out the multiplicative part.
\nRemember from the simply typed lambda calculus, that [we showed that the type system was precisely a subset of intuitionistic logic][lambda-type], and that programs in the lambda calculus corresponded to proofs in the type system. In particular, it was propositional intuitionistic logic using only the “→” operation. Similarly, if you build up a more interesting typed lambda calculus like [System-F][systemf], the type system is intuitionist logic *with* the “∀” quantifer and the “∧” operator, but without “∨”, negation, or “∃”. Why do we eliminate the existentials and friends? Because if we left them in, then the *type system* becomes Turing complete and undecidable. If we’re careful, we can analyze a program using universal types, logical and (composition in lambda), and implication and infer the types if it’s a valid program. (Actually, even System-F is undecidable without any type annotations, but HMF – the Hindley-Milner subset, *is* decidable. NP-hard, but decidable.)
\nThe main reason that people like me really care about linear logic is because there is a variant of lambda calculus that includes *linear types*. Linear types are types where referencing the value corresponding to the type *consumes* it. For dealing with the semantics of real programming languages, there are many things that make sense as linear types. For example, the values of an input stream behave in a linear way: read something from an input stream, and it’s not there anymore: unless you copied it, to put it someplace safe, it’s gone.
\nFor typing linear lambda calculus, we use *intuitionistic linear logic* with the *multiplicative* operators. They give us a *decidable* type system with the capability to express linear type constraints.
\nEnough side-tracking; back to the categories.
\nWe can now finally define a *linear category*. A category C is a linear category if it is both a [cartesian category][cartesian] and a [monoidal][monoidal] [closed category][monclose] with a *dualizing functor*. A dualizing functor is a *contravariant* closed functor defining properties of the categorical exponential, written (-)*<\/sup> : C → C. (That should be read with “-” as a placeholder for an object; and * as a placeholder for an exponent.) (-)*<\/sup> has the property that there is a natural isomorphism d : Id ≡ (-)**<\/sup> (That is, d is an identity natural isomorphism, and it’s equivalent to applying (-)*<\/sup> to the result of applying (-)*<\/sup> ) such that the following commutes:<\/p>\n

\"linear-dual.jpg\"<\/p>\n

So, what does this mean? Take the linear implication operator; mix it with the categorical exponent; and what you get *still* behaves *linearly*: that is, if “X -o Y”; that is, one X can be consumed to produce one Y, then 2 Xs can be consumed to produce 2 Ys; and N Xs can be consumed to produce N Ys.
\nSo a linear category behaves cleanly with exponents; t has a linear implication; it has an *eval* operator (from the fact that it’s a cartesian category) to perform the linear implications; it has tensor for producing groups of resources. That’s it; that’s everything we need from categories for a model of linear logic.
\nNow, there’s just one more question: are there any real linear categories that make sense as a model for linear logic? And obviously, the answer is yes. There are two of them, called **CPO** and **Lin**.
\n**CPO** is the category with continuous partial orders as objects, and monotonic functions as morphisms. Think about that, and it makes a whole lot of sense for linear logic; the equivalence classes of the partial order are resources of the same “value” (that is, that can be exchanged for one another); and you can’t climb *upwards* in the partial order without adding something.
\nThe other one, **Lin**, is a lot more complicated. I’m not going to explain it in detail; that would lead into another two-month-long series! But to put it briefly, **Lin** is the category with *coherent domains* as objects, and linear maps as morphisms. To make that make sense, I would have to explain domain theory, which (to put it mildly) is complicated; the short version is that a domain is a kind of CPO. But the reason we care about **Lin** is that programming language semantics are generally described using [*denotational semantics*][denote]; and denotational semantics are built using a kind of domain, called a Scott domain. So this gives us a domain that we can use in programming language semantics with exactly the properties we need to explain how linear types work.
\n[lambda-type]: http:\/\/goodmath.blogspot.com\/2006\/06\/finally-modeling-lambda-calculus.html
\n[systemf]: http:\/\/en.wikipedia.org\/wiki\/System_F
\n[cartesian]: http:\/\/scienceblogs.com\/goodmath\/2006\/06\/categories_products_exponentia_1.php
\n[monclose]: http:\/\/scienceblogs.com\/goodmath\/2006\/07\/towards_a_model_for_linear_log_1.php
\n[monoidal]: http:\/\/scienceblogs.com\/goodmath\/2006\/07\/the_category_structure_for_lin_1.php
\n[denote]: http:\/\/en.wikipedia.org\/wiki\/Denotational_semantics<\/p>\n","protected":false},"excerpt":{"rendered":"

Today we’ll finally get to building the categories that provide the model for the multiplicative linear logic. Before we jump into that, I want to explain why it is that we separate out the multiplicative part. Remember from the simply typed lambda calculus, that [we showed that the type system was precisely a subset of […]<\/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":[76,24],"tags":[],"class_list":["post-93","post","type-post","status-publish","format-standard","hentry","category-category-theory","category-goodmath"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-1v","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/93","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=93"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/93\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=93"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=93"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=93"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}