Maths - Linear Logic

Youtube video Frank Pfenning (2012) - Linear Logic

Lecture 01 Lecture 02

Lecture 03 - harmony

Lecture 04 - cut reduction as computation

Lecture 05 - choice and replication

Lecture 06 Lecture 07 Lecture 08 Lecture x Lecture x

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

Γright adjointa:A
Γ, b:Bright adjointa: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:Aright adjointb:B
Γ,z:Aright adjointb[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:Bright adjointc:C
Γ,b:B,a:Aright adjointc:C

Cut Rule

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

Γright adjointA   A,Δright adjointB
Γ,Δright adjointB

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: assumptionsright adjointproof
to   resourcesright adjointgoal

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:

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.


metadata block
see also:

Correspondence about this page

Book Shop - Further reading.

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.

flag flag flag flag flag flag 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.

 

Terminology and Notation

Specific to this page here:

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2021 Martin John Baker - All rights reserved - privacy policy.