Examples - ComputerAidedLL/click-and-collect GitHub Wiki

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

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

Double Negation Translations

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

⚠️ GitHub.com Fallback ⚠️