P. 3 of Theorem List - Linear Logic Proof Explorer

Home	Linear Logic Proof Explorer Theorem List (p. 3 of 4)	< Previous  Next >
		Mirrors  >  Metamath Home Page  >  LLPE Home Page  >  Theorem List Contents       This page: Page List

Type

Label

Description

Statement

Theorem

lbtrimd 201

Linear biconditional is transitive. Intuitionistic deduction for lbtr 128.

⊦ (𝜑 → (𝜓 ⧟ 𝜒))    &   ⊦ (𝜑 → (𝜒 ⧟ 𝜃))    ⇒   ⊦ (𝜑 → (𝜓 ⧟ 𝜃))

Theorem

lbsymimd 202

Linear biconditional is transitive. Intuitionistic deduction for lbsym 127.

⊦ (𝜑 → (𝜓 ⧟ 𝜒))    ⇒   ⊦ (𝜑 → (𝜒 ⧟ 𝜓))

1.3  Message passing

So, y'know, I was thinking to myself one day. I was thinking, hey, linear logic is pretty cool. You know what else is cool? Pi calculus. So I thought, hey, they seem pretty simiar, and maybe two great flavors go great together. So I figured I would add message passing to linear logic, since a stateful process is a great example of a resource. So let's see what happens. In pi calculus, every object is a channel. Channels are given meaning by processes, which read from and write to them. Since processes are stateful, we can consider them to be the resources manipulated by linear logic. We will say that a process is valid, i.e. can appear in front of ⊦, if it always halts. Pi calculus introduces three new operators, which operate on channel variables. They are:

Name	Ref	Description
Input	wse 204: [X ≪ Y] 𝜑	Writes to a channel and blocks
Output	wre 205: [X ≫ y] 𝜑	Reads from a channel and blocks (binding a new name in the process)
Creation	wnu 206: νx𝜑	Creates a new channel

The remaining operators of pi calculus are directly implemented by the connectives of linear logic:

Name	Ref	Description
Concurrency	wmc 105: (𝜑 ⊗ 𝜓)	Run 𝜑 and 𝜓 in parallel, allowing communication over channels
Choice	wac 30: (𝜑 & 𝜓)	Nondeterministically run either 𝜑 or 𝜓
Replication	wpe 148: ! 𝜑	Run infinite copies of 𝜑 in parallel
Termination	wone 103: 1	Halt the current process

Note that some of the channel variables are pink and capital like X, while others are red and lowercase like y. The only difference is that the red ones must be a literal channel name (similar to setvar variables in set.mm), while the pink ones can also be compound expressions. These compound expressions are known as nilads, because they act like functions that are evaluated as soon as they are encountered.

I'm almost certain that some of the axioms are redundant (or at least can be weakened), and it's very likely that this system is inconsistent, but hopefully it'll all work out.

1.3.1  Axioms for message passing

Syntax

nvar 203

A variable can be used as a nilad.

nilad x

Syntax

wse 204

Sending operator. Writes Y to the channel X.

wff [X ≪ Y] 𝜑

Syntax

wre 205

Recieving operator. Reads from X and scopes the result to y.

wff [X ≫ y] 𝜑

Syntax

wnu 206

Creation operator. Creates and scopes a new channel x. It also has a dual ~ νx~ 𝜑, which has a meaning I don't quite understand.

wff νx𝜑

Syntax

wsub 207

Proper substitution of x with Y. Although used as a primitive token in the axioms, it can actually be treated as a defined symbol; see dfsub 233. See nsub 277 for proper substitution in nilads.

wff [x ≔ Y] 𝜑

1.3.1.1  Creation operator

These axioms characterize the channel creation operator, ν. Its behavior resembles that of the ∃ quantifier in predicate logic, but its actual semantics are quite different. ν essentially isolates variable scopes, forbidding communication along a specific variable. On its own, though, it pretty much acts like any run-of-the-mill quantifier.

Axiom

ax-int 208

Generalization. An "anti variable abstraction" can be removed from a "top-level" wff. What does that even mean?

⊦ 𝜑    ⇒   ⊦ ~ νx~ 𝜑

Axiom

ax-nue 209*

A variable abstraction can be eliminated if the expression is free in that variable.

⊦ (νx𝜑 ⊸ 𝜑)

Axiom

ax-nuf 210

x is free in νx.

⊦ (νxνx𝜑 ⊸ νx𝜑)

Axiom

ax-ref 211

x is free in [a ≫ x].

⊦ (νx[a ≫ x] 𝜑 ⊸ [a ≫ x] 𝜑)

Axiom

ax-nnuf 212

x is free in ~ νx𝜑. There's that weird "anti variable abstraction" again...

⊦ (νx~ νx𝜑 ⊸ ~ νx𝜑)

Axiom

ax-nui 213

A wff can be surrounded by a variable abstraction

⊦ (𝜑 ⊸ νx𝜑)

Axiom

ax-nur 214

Variables can be renamed without changing the meaning of an expression.

⊦ (νx[u ≪ x] 𝜑 ⊸ νy[u ≪ y] 𝜑)

Axiom

ax-nuse 215

Commutation of ν with ≪.

⊦ (νx[u ≪ v] 𝜑 ⧟ [u ≪ v] νx𝜑)

Axiom

ax-nure 216

Commutation of ν with ≫.

⊦ (νx[u ≫ v] 𝜑 ⧟ [u ≫ v] νx𝜑)

Axiom

ax-nuad 217

Distribution of ν over ⊕.

⊦ (νx(𝜑 ⊕ 𝜓) ⧟ (νx𝜑 ⊕ νx𝜓))

Axiom

ax-numc 218

Commutation of ν into ⊗. Note that x can only be bound in one factor.

⊦ (νx(𝜑 ⊗ νx𝜓) ⧟ (νx𝜑 ⊗ νx𝜓))

Axiom

ax-nunu 219

Commutation of ν with ν. There is no need for a distinct variable condition on x and y, since (νxνx𝜑 ⧟ νxνx𝜑) is a valid theorem.

⊦ (νxνy𝜑 ⧟ νyνx𝜑)

1.3.1.2  Communication

Axiom

ax-subse1 220

⊦ ([x ≔ y] [x ≪ a] 𝜑 ⧟ [x ≔ y] [y ≪ a] 𝜑)

Axiom

ax-subse2 221

⊦ ([x ≔ y] [a ≪ x] 𝜑 ⧟ [x ≔ y] [a ≪ y] 𝜑)

Axiom

ax-subse3 222*

⊦ ([x ≔ y] [u ≪ v] 𝜑 ⧟ [u ≪ v] [x ≔ y] 𝜑)

Axiom

ax-subre1 223

⊦ ([x ≔ y] [x ≫ a] 𝜑 ⧟ [x ≔ y] [y ≫ a] 𝜑)

Axiom

ax-subre2 224*

⊦ ([x ≔ y] [u ≫ v] 𝜑 ⧟ [u ≫ v] [x ≔ y] 𝜑)

Axiom

ax-subnu1 225

⊦ ([x ≔ y] νx𝜑 ⧟ νx𝜑)

Axiom

ax-subnu2 226*

⊦ ([x ≔ y] νu𝜑 ⧟ νu[x ≔ y] 𝜑)

Axiom

ax-subid 227

⊦ ([x ≔ x] 𝜑 ⧟ 𝜑)

Axiom

ax-send 228

Message passing.

⊦ (([z ≪ y] 𝜑 ⊗ [z ≫ x] 𝜓) ⊸ (𝜑 ⊗ [x ≔ y] 𝜓))

Axiom

ax-lock1 229

Reading from a channel with nothing writing to it causes a deadlock.

⊦ (νx? [x ≫ a] 1 ⊸ 0)

Axiom

ax-lock2 230

Writing to a channel with nothing reading from it causes a deadlock.

⊦ (νx? [x ≪ a] 1 ⊸ 0)

1.3.2  Message passing theorems

Theorem

sead 231

Distribution of sending over ⊕.

⊦ (([x ≪ y] 1 ⊗ (𝜑 ⊕ 𝜓)) ⧟ (([x ≪ y] 1 ⊗ 𝜑) ⊕ ([x ≪ y] 1 ⊗ 𝜓)))

Theorem

rech 232

Writing to a channel being read in multiple places causes a nondeterministic choice.

⊦ (([x ≪ x] 𝜑 ⊗ ([x ≫ x] 𝜓 ⊗ [x ≫ x] 𝜒)) ⧟ (𝜑 ⊗ (𝜓 ⊕ 𝜒)))

Theorem

dfsub 233*

"Definition" of proper substitution. Or at least it would be, if I implemented proper substitution as a defined operator...

This simply sends the desired value Y along a temporary channel a, and then reads it to the desired name x.

⊦ ([x ≔ Y] 𝜑 ⧟ νz([z ≪ Y] 1 ⊗ [z ≫ x] 𝜑))

Theorem

abse1 234*

Proper substitution into the left side of ≪.

⊦ ([x ≪ y] νa𝜑 ⧟ [a ≔ x] [a ≪ y] νa𝜑)

Theorem

abse2 235*

Proper substitution into the right side of ≪.

⊦ ([x ≫ y] νa𝜑 ⧟ [a ≔ y] [x ≫ a] νa𝜑)

Theorem

abre1 236*

Proper substitution into the left side of ≫.

⊦ ([x ≪ y] νa𝜑 ⧟ [a ≔ x] [a ≪ y] νa𝜑)

Theorem

abf 237*

Proper substitution into an expression free of that variable.

⊦ (νxνa𝜑 ⧟ [a ≔ x] νxνa𝜑)

Theorem

abre2 238*

Proper substitution into the right side of ≫ (which is free of that variable).

⊦ ([x ≫ y] νa𝜑 ⧟ [a ≔ y] [x ≫ y] νa𝜑)

Theorem

abid 239

Proper substitution of a variable for itself.

⊦ (𝜑 ⧟ [x ≔ x] 𝜑)

1.3.3  Message passing dual operators

One interesting consequence of adding pi calculus operators to linear logic is that the dualism of linear logic now applies to these operators. What even??? Wow this is crazy.

Syntax

wnse 240

Dual write operator.

wff [X ◁ Y] 𝜑

Syntax

wnre 241

Dual read operator.

wff [X ▷ y] 𝜑

Syntax

wnnu 242

Dual creation operator.

wff ∇x𝜑

Definition

df-nse 243

Definition of the dual write operator.

⊦ ([X ◁ Y] 𝜑 ⧟ ~ [X ≪ Y] ~ 𝜑)

Definition

df-nre 244

Definition of the dual read operator.

⊦ ([X ▷ y] 𝜑 ⧟ ~ [X ≫ y] ~ 𝜑)

Definition

df-nnu 245

Definition of the dual creation operator.

⊦ (∇x𝜑 ⧟ ~ νx~ 𝜑)

Syntax

weq 246

Nilad equality.

wff X = Y

Definition

df-eq 247

Definition of channel equality. Two nilads are equivalent if, when written to an arbitrary channel, that channel behaves the same way. We measure this by seeing if we can successfully read from it.

⊦ (X = Y ⧟ ∇a([a ≪ X] [a ≫ b] 1 ⧟ [a ≪ Y] [a ≫ b] 1))

Theorem

eqpe 248

Equality can be !-ified.

⊦ (X = Y ⊸ ! X = Y)

Theorem

eqeu 249

Equality is Euclidean.

⊦ ((X = Y ⊗ Y = Z) ⊸ X = Z)

Theorem

eqtr 250

Equality is transitive.

⊦ ((X = Y ⊗ Y = Z) ⊸ X = Z)

Theorem

eqsym 251

Equality is symmetric.

⊦ (X = Y ⊸ Y = X)

Theorem

eqeui 252

Equality is Euclidean. Inference for eqtr 250.

⊦ X = Y    &   ⊦ X = Z    ⇒   ⊦ Y = Z

Theorem

eqtri 253

Equality is transitive. Inference for eqtr 250.

⊦ X = Y    &   ⊦ Y = Z    ⇒   ⊦ X = Z

Theorem

eqsymi 254

Equality is symmetric. Inference for eqsym 251.

⊦ X = Y    ⇒   ⊦ Y = X

Theorem

eqeud 255

Equality is Euclidean. Deduction for eqeu 249.

⊦ (𝜑 ⊸ X = Y)    &   ⊦ (𝜑 ⊸ X = Z)    ⇒   ⊦ (𝜑 ⊸ Y = Z)

Theorem

eqtrd 256

Equality is transitive. Deduction for eqtr 250.

⊦ (𝜑 ⊸ X = Y)    &   ⊦ (𝜑 ⊸ Y = Z)    ⇒   ⊦ (𝜑 ⊸ X = Z)

Theorem

eqsymd 257

Equality is symmetric. Deduction for eqsym 251.

⊦ (𝜑 ⊸ X = Y)    ⇒   ⊦ (𝜑 ⊸ Y = X)

Theorem

eqeuimd 258

Equality is Euclidean. Intuitionistic deduction for eqeu 249.

⊦ (𝜑 → X = Y)    &   ⊦ (𝜑 → X = Z)    ⇒   ⊦ (𝜑 → Y = Z)

Theorem

eqtrimd 259

Equality is transitive. Intuitionistic deduction for eqtr 250.

⊦ (𝜑 → X = Y)    &   ⊦ (𝜑 → Y = Z)    ⇒   ⊦ (𝜑 → X = Z)

Theorem

eqsymimd 260

Equality is symmetric. Intuitionistic deduction for eqsym 251.

⊦ (𝜑 → X = Y)    ⇒   ⊦ (𝜑 → Y = X)

Theorem

eqse1 261

Sending is closed under equality (left side).

⊦ (X = Y ⊸ ([X ≪ a] 𝜑 ⧟ [Y ≪ a] 𝜑))

Theorem

eqse2 262

Sending is closed under equality (right side).

⊦ (X = Y ⊸ ([a ≪ X] 𝜑 ⧟ [a ≪ Y] 𝜑))

Theorem

eqre 263

Recieving is closed under equality.

⊦ (X = Y ⊸ ([X ≫ a] 𝜑 ⧟ [Y ≫ a] 𝜑))

Theorem

dfsub1 264

Restatement of dfsub 233 with nilad equality.

⊦ ([x ≔ Y] 𝜑 ⧟ ∇x(x = Y ⊸ 𝜑))

Theorem

test 265

⊦ (νb[a ≪ b] 1 ⊗ ([a ≫ c] 1 ⊗ [c ≪ a] 1))

1.3.4  Nilad abstractions

Syntax

nnab 266

A nilad abstraction. When used where a variable would normally belong, the variable used is instead the first one written by 𝜑 to x. (Any other operations on x will block indefinitely, as they would on a fresh channel.) This is a very useful concept, since this allows us to reason about expressions which carry values.

Keep in mind that these must be treated linearly like everything else, so using nilad variables multiple times may carry unintended consequences. Use ≔ as necessary to avoid this.

The nilad abstraction is characterized by df-nab 267.

nilad {x | 𝜑}

Definition

df-nab 267*

Using a nilad abstraction is the same as running the associated process 𝜑 and using its "return value" instead. Since the input to all other operators can be modeled using ≪, this is enough to fully describe nilad abstractions.

Unlike most defined operators, the nilad abstraction cannot directly be expanded to primitive symbols. Despite this, it is always possible to mechanically eliminate nilads from any expression that contains them by simply moving the process 𝜑 to before the variable y is used.

⊦ ([x ≪ {y | 𝜑}] 𝜓 ⧟ (𝜑 ⊗ [y ≫ a] [x ≪ a] 𝜓))

Theorem

dfnab1 268*

df-nab 267 also works on nilads.

⊦ ([X ≪ {y | 𝜑}] 𝜓 ⧟ (𝜑 ⊗ [y ≫ a] [X ≪ a] 𝜓))

Theorem

dfnab2 269*

Read from a nilad.

⊦ ([{x | 𝜑} ≫ y] 𝜓 ⧟ (𝜑 ⊗ [x ≫ a] [a ≫ y] 𝜓))

Theorem

dfnab3 270*

Write to a nilad.

⊦ ([{x | 𝜑} ≪ Y] 𝜓 ⧟ (𝜑 ⊗ [x ≫ a] [a ≪ Y] 𝜓))

Syntax

nvnab 271

A simple nilad abstraction. Ordinary nilad abstractions use the bound channel as a sort of return channel, while this version immediately returns a fresh channel.

nilad {νx | 𝜑}

Definition

df-vnab 272

Definition of simple nilads.

⊦ {νx | 𝜑} = {r | νx[r ≪ x] 𝜑}

Theorem

vnab1 273

Write a simple nilad abstraction along a channel.

⊦ ([X ≪ {νy | 𝜑}] 𝜓 ⧟ νy(𝜑 ⊗ [X ≪ y] 𝜓))

Theorem

vnab2 274

Read from a simple nilad abstraction.

⊦ ([{νx | 𝜑} ≫ y] 𝜓 ⧟ νx(𝜑 ⊗ [x ≫ y] 𝜓))

Theorem

vnab3 275

Write to a simple nilad abstraction.

⊦ ([{νx | 𝜑} ≪ Y] 𝜓 ⧟ νx(𝜑 ⊗ [x ≪ Y] 𝜓))

Theorem

nvarjust 276*

A variable is equivalent to a nilad which always returns that variable.

⊦ x = {r | [r ≪ x] 1}

Syntax

nsub 277

Proper substitution of x with Y in the nilad A. See also wsub 207.

nilad [x ≔ Y] A

Definition

df-nsub 278*

The proper substitution of x with Y in F.

⊦ [x ≔ Y] F = {r | νa[x ≔ y] [F ≫ f] [r ≪ f] 1}

1.4  Lambda calculus

Syntax

nla 279

Lambda abstraction.

nilad λxY

Definition

df-la 280*

Definition of lambda abstraction. The lambda exposes a "handle" f which reads a temporary communication channel a. The resulting function's input x and output Y are passed along a. The ! exponential creates infinite instances of this function "provider", which can all run in parallel. Compare with df-fv 282 to see how this function is called.

⊦ λxY = {νf | ! [f ≫ a] [a ≫ x] [a ≪ Y] 1}

Syntax

nfv 281

Function application.

nilad (F' X)

Definition

df-fv 282*

Definition of function application. This sends a temporary communication channel a to F, and communicates the input X and output y. Compare with df-la 280 to see how functions are defined.

⊦ (F' X) = {r | νa[F ≪ a] [a ≪ X] [a ≫ y] [r ≪ y] 1}

Theorem

lav 283

Lambda evaluation theorem.

⊦ (λxF' Y) = [x ≔ Y] F

Syntax

nov 284

Operator application.

nilad (AFB)

Definition

df-ov 285

Definition of operator application. It's simply two curried function applications.

⊦ (AFB) = ((F' A)' B)

Syntax

nss 286

S combinator, the input distributor.

nilad S

Syntax

nkk 287

K combinator, the constant generator.

nilad K

Syntax

nii 288

I combinator, the identity function.

nilad I

Syntax

niota 289

Iota combinator, from which the S, K, and I combinators can be derived.

nilad ι

Definition

df-ss 290*

Definition of the S combinator.

⊦ S = λaλbλc((b' a)' (c' a))

Definition

df-kk 291*

Definition of the K combinator.

⊦ K = λaλba

Definition

df-ii 292

Definition of the I combinator.

⊦ I = λaa

Definition

df-iota 293

Definition of the iota combinator in terms of S and K.

⊦ ι = λf((f' S)' K)

Theorem

iiiota 294

Construction of I from ι.

⊦ I = (ι' ι)

Theorem

kkiota 295

Construction of K from ι.

⊦ K = (ι' (ι' (ι' ι)))

Theorem

ssiota 296

Construction of S from ι.

⊦ S = (ι' (ι' (ι' (ι' ι))))

1.4.1  Intuitionistic logic but with lambda calculus

Syntax

ntru 297

Function representing truth.

nilad True

Syntax

nfal 298

Function representing falsity.

nilad False

Definition

df-tru 299*

Church-encoding of truth. It takes two (curried) arguments and returns the first. Happens to be identical to nkk 287.

⊦ True = λxλyx

Definition

df-fal 300*

Church-encoding of falsity. It takes two (curried) arguments and returns the second.

⊦ False = λxλyy