Youtube video Frank Pfenning (2012) - Linear Logic
Lecture 03 - harmony
Lecture 04 - cut reduction as computation
Lecture 05 - choice and replication
Lecture 06 Lecture 07 Lecture 08 Lecture x Lecture x
Use for computing:
Linear Logic changes structural rules so that they do not allow Weakening Rule or Contraction Rule. This means that resources are conserved (we cannot duplicate them when we want). This maintains some sort of state.
Structural rules
Structural rules define how variables can be substituted, reordered, and ignored in appropriate ways.
Rule |
|||||||
|---|---|---|---|---|---|---|---|
Weakening Rule Hypotheses may be extended with additional members |
|
||||||
Contraction Rule Two equal (or unifiable) members on the same side of a sequent may be replaced by a single member. Hypotheses contains two proofs of of A that is x:A y:A which we can replace with one proof z:A . Also known as:
|
|
||||||
Exchange Rule variables in the context can be reordered. (for dependent types B cannot depend on a.) |
|
||||||
Cut Rule This has a different status in sequent calculus since it is a primative built into the mechinism. |
|
||||||
Information about type theories/logics which do not have some of these rules:
| exchange | weakening | contraction | use | |
|---|---|---|---|---|
| linear logic | yes | =1 Girard's linear logic does not allow the copying and destruction of terms so they must be used once. However they are still transferable. (transferring a resource from one owner to another can be done even when the resource cannot be copied.) |
||
| affine logic | yes | yes | ≤1 | |
| relevent | yes | yes | ≥1 | |
| ordered | once in order |
Linear Logic
| we change from meaning of sequent from: | assumptions proof |
|
| to | resourcesgoal |
Quantitative Type Theory
QTT = Linear types + Dependent types
π calculus
Represents interactions between independent processes as communication (message-passing), rather than as modification of shared variables.
Describes concurrent communication language in which we can describe communicating processes which interact.
Each channel can operate in parallel and both the channels (different endpoints) and the state of the channels can change during the computation.
In π calculus we have:
- channels
- channels have a state (what event are they expecting)
we pass around names of channels. Names of channels can be passed along other channels.
channels names may be used only once but new instances of names (that is, reuse existing name) may be created for changes in state of the channel.
