# Maths - Linear Logic

Lecture 03 - harmony

Lecture 04 - cut reduction as computation

Lecture 05 - choice and replication

Lecture 24

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

 Γa:A Γ, b:Ba:A

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:

• factoring in automated theorem proving systems using resolution.
• 'idempotency of entailment' in classical logic.
 Γ,x:A,y:Ab:B Γ,z:Ab[z/x,z/y]:B

Exchange Rule

variables in the context can be reordered. (for dependent types B cannot depend on a.)

 Γ,a:A,b:Bc:C Γ,b:B,a:Ac:C

Cut Rule

This has a different status in sequent calculus since it is a primative built into the mechinism.

 ΓA A,ΔB Γ,ΔB

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: assumptionsproof to resourcesgoal

## Quantitative Type Theory

QTT = Linear types + Dependent types

ref

## π calculus

wiki

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.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

 Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.