Examples

Basic Properties

Multiplicatives

• A⊗B ⊢ B⊗A ≈ A⅋B ⊢ B⅋A (commutativity)
• (A⊗B)⊗C ⊢ A⊗(B⊗C) ≈ A⅋(B⅋C) ⊢ (A⅋B)⅋C ≈ A⊸B⊸C ⊢ A⊗B⊸C (associativity)
• A⊗(B⊗C) ⊢ (A⊗B)⊗C ≈ (A⅋B)⅋C ⊢ A⅋(B⅋C) ≈ A⊗B⊸C ⊢ A⊸B⊸C (associativity)
• A ⊢ A⊗1 ≈ A⅋⊥ ⊢ A ≈ 1⊸A ⊢ A (unit)
• A⊗1 ⊢ A ≈ A ⊢ A⅋⊥ ≈ A ⊢ 1⊸A (unit)
• (A⊸B)⊗C ⊢ A⊸(B⊗C) ≈ (A⅋B)⊗C ⊢ A⅋(B⊗C) (linear distributivity)
• A⊸A ≈ A^⊥⅋A (identity)
• A⊸B, B⊸C ⊢ A⊸C (composition)
• A⊗(A⊸B) ⊢ B (evaluation)

Additives

• A&B ⊢ B&A ≈ A⊕B ⊢ B⊕A (commutativity)
• (A&B)&C ⊢ A&(B&C) ≈ A⊕(B⊕C) ⊢ (A⊕B)⊕C (associativity)
• A&(B&C) ⊢ (A&B)&C ≈ (A⊕B)⊕C ⊢ A⊕(B⊕C) (associativity)
• A ⊢ A&⊤ ≈ A⊕0 ⊢ A (unit)
• A&⊤ ⊢ A ≈ A ⊢ A⊕0 (unit)
• A ⊢ A&A ≈ A⊕A ⊢ A (idempotency)
• A&B ⊢ A ≈ A ⊢ A⊕B (projection / injection)
• A ⊢ ⊤ ≈ 0 ⊢ A (terminal / initial)
• A⊕(B&C) ⊢ (A⊕B)&(A⊕C) ≈ (A&B)⊕(A&C) ⊢ A&(B⊕C)

Exponentials

• !A ⊢ A ≈ A ⊢ ?A (dereliction)
• !A ⊢ !!A ≈ ??A ⊢ ?A (digging)
• !A ⊢ !?!A ≈ ?!?A ⊢ ?A
• !?!?A ⊢ !?A ≈ ?!A ⊢ ?!?!A
• !?!A ⊢ !?A ≈ ?!A ⊢ ?!?A
• !?!A ⊢ ?!A ≈ !?A ⊢ ?!?A

Multiplicative-Additive Interactions

• A⊗(B⊕C) ⊢ (A⊗B)⊕(A⊗C) ≈ (A⅋B)&(A⅋C) ⊢ A⅋(B&C) ≈ (A⊸B)&(A⊸C) ⊢ A⊸(B&C) ≈ (A⊸C)&(B⊸C) ⊢ A⊕B⊸C (distributivity)
• (A⊗B)⊕(A⊗C) ⊢ A⊗(B⊕C) ≈ A⅋(B&C) ⊢ (A⅋B)&(A⅋C) ≈ A⊸(B&C) ⊢ (A⊸B)&(A⊸C) ≈ A⊕B⊸C ⊢ (A⊸C)&(B⊸C) (distributivity)
• A⊗0 ⊢ 0 ≈ ⊤ ⊢ A⅋⊤ ≈ ⊤ ⊢ A⊸⊤ ≈ ⊤ ⊢ 0⊸A (absorption)
• 0 ⊢ A⊗0 ≈ A⅋⊤ ⊢ ⊤ ≈ A⊸⊤ ⊢ ⊤ ≈ 0⊸A ⊢ ⊤ (absorption)
• A⊗(B&C) ⊢ (A⊗B)&(A⊗C) ≈ (A⅋B)⊕(A⅋C) ⊢ A⅋(B⊕C)

Exponential-Multiplicative Interactions

• !A ⊢ !A⊗!A ≈ ?A⅋?A ⊢ ?A (contraction)
• !A ⊢ 1 ≈ ⊥ ⊢ ?A (weakening)
• !(A⊸B) ⊢ !A⊸!B (promotion)
• !A⊗!B ⊢ !(A⊗B) ≈ ?(A⅋B) ⊢ ?A⅋?B (monoidality)
• 1 ⊢ !1 ≈ ?⊥ ⊢ ⊥ (unit monoidality)
• ?(!A⊗!B) ⊢ ?!(A⊗B) ≈ !?(A⅋B) ⊢ !(?A⅋?B)
• !?!A⊗!?!B ⊢ !?!(A⊗B) ≈ ?!?(A⅋B) ⊢ ?!?A⅋?!?B
• 1 ⊢ !?1 ≈ ?!⊥ ⊢ ⊥
• 1 ⊢ !(X^⅋X) ≈ ?(X⊗X^) ⊢ ⊥ (pseudo second-order encoding)
• !(X^⅋X) ⊢ 1 ≈ ⊥ ⊢ ?(X⊗X^) (pseudo second-order encoding)

Exponential-Additive Interactions

• !A⊕!B ⊢ !(A⊕B) ≈ ?(A&B) ⊢ ?A&?B (monoidality)
• ?A⊕?B ⊢ ?(A⊕B) ≈ !(A&B) ⊢ !A&!B (monoidality)
• ?(!A⊕!B) ⊢ ?!(A⊕B) ≈ !?(A&B) ⊢ !(?A&?B)
• ?!(?A⊕?B) ⊢ ?(!?A⊕!?B) ≈ !(?!A&?!B) ⊢ !?(!A&!B)

Exponential-Multiplicative-Additive Interactions

• !(A&B) ⊢ !A⊗!B ≈ ?A⅋?B ⊢ ?(A⊕B) (exponential isomorphism)
• !A⊗!B ⊢ !(A&B) ≈ ?(A⊕B) ⊢ ?A⅋?B (exponential isomorphism)
• !⊤ ⊢ 1 ≈ ⊥ ⊢ ?0 (unit exponential isomorphism)
• 1 ⊢ !⊤ ≈ ?0 ⊢ ⊥ (unit exponential isomorphism)
• !A⊗!B ⊢ !(!A&!B) (Seely condition)
• A⊕B ⊢ !(A⊸X)⊸!(B⊸X)⊸X (pseudo second-order encoding)
• !(A⊸A⊕B)⊸!(B⊸A⊕B)⊸A⊕B ⊢ A⊕B (pseudo second-order encoding)

Datatypes

Booleans

• A⊗A⊸A⊗A (multiplicative Booleans)
  • true
  • false
• 1⊕1 (additive Booleans)
  • true
  • false

Church Natural Numbers

• !(A⊸A)⊸!(A⊸A)
  • 3 + 2

Binary Lists

• !(A⊸A)⊸!(A⊸A)⊸!(A⊸A)

Translations

Decorations

• A⊸!B⊸A (K combinator)
• (A⊸B⊸C)⊸(A⊸B)⊸!A⊸C (S combinator)
• ((A⊸?B)⊸A)⊸?A (Peirce's law)

Girard's Encodings

• !A⊸!B⊸A (K combinator)
• !(!A⊸!B⊸C)⊸!(!A⊸B)⊸!A⊸C (S combinator)
• !(!A⊸B), !(!B⊸C) ⊢ !A⊸C (composition)

Double Negation Translations

• A ⊢ (A⊸R)⊸R
• ((A⊸R)⊸R)⊸R ⊢ A⊸R
• ((A⊸R)⊸R)⊗((B⊸R)⊸R) ⊢ ((A⊗B)⊸R)⊸R
• ((A⊸R)⊸R)⊕((B⊸R)⊸R) ⊢ ((A⊕B)⊸R)⊸R

Intuitionistic vs. Classical Linear Provabilities

• (A⊸(0⊸B)⊸A')⊸((A⊸A')⊸0)⊸B' (Schellinx' formula)
• ((A⊸A')⊸0)⊸A⊗⊤ (Lafont's formula)
• ((((0⊸1)⊸1)⊸0)⊸0)⊸1 (Wu's formula)
• (((A⊗⊤)&(B⊗⊤))⊸0)⊸((A⊸A')⊕(B⊸B')) (Laurent's formula)

Miscellaneous

• A⊗(A⊸A) ⊢ A⊗!(A⊸A) (variant on Beffara's formula)
• ⊢ ?A, ?(B⅋B), ?(A^⊥⅋B^⊥), ?(⊥⊗⊥) (lcm of 1 and 2)
• ⊢ ?(A⅋A), ?(B⅋B⅋B), ?(A^⊥⅋B^⊥), ?(⊥⊗⊥) (lcm of 2 and 3)
• ?(A^⊥⊕A)
• ⊢ (1⅋1)⊗⊥, ?(?1⊗?1)
• A⊗!(A⊸A⊗A)⊗!(A⊸1) ⊢ 1
• A⊗!(A⊸A⊗A)⊗!(A⊸1) ⊢ (A⊗!(A⊸A⊗A)⊗!(A⊸1))⊗(A⊗!(A⊸A⊗A)⊗!(A⊸1))
• ?((A⊕A^⊥)⊗(((B⊗B)⊕B^⊥)⅋((B⊗B)⊕B^⊥)))

Recursive Types

• o with o ::= !o⊸o (untyped λ-calculus)
  • identity
  • Ω
  • Y
• a with a ::= ?a^
  • a
  • Ω
  • Y
• N with N ::= 1⊕N (Peano natural numbers)
  • 0
  • 1
  • succ
  • pred
  • pred 1