Cartesian closed categories CCC

(1)

Cartesian closed categories CCC

'

&

$

% '

&

$

% typed

functional

programming catego vs.

ry theo

ry '

&

$

% '

&

$

%

typed lamb

da-calculi vs.

catego

ry theo ry

Andrzej Tarlecki: Category Theory, 2021 - 130 -

(2)

Cartesian closed categories CCC

'

&

$

% '

&

$

% typed

functional

ry theo

ry '

&

$

% '

&

$

%

typed lamb

da-calculi vs.

catego

ry theo ry

(3)

Cartesian closed categories CCC

'

&

$

% '

&

$

% typed

functional

ry theo

ry '

&

$

% '

&

$

% typed lamb

da-calculi vs.

catego

ry theo ry

(4)

Cartesian categories

Definition: A category K is Cartesian if it comes equipped with finite products.

Equivalently:

• 1 ∈ |K| — a terminal object

• A × B — a product of A and B, for every A, B ∈ |K|

Examples: Set, Pfn, Cpo, semilattices, Cat, T_Σ,Φ^op , . . .

Recall the definitions of these categories and the constructions of products in each of them

(5)

Cartesian categories

Equivalently:

(6)

Cartesian categories

Equivalently:

(7)

Cartesian categories

Equivalently:

(8)

Cartesian categories

Equivalently:

(9)

Cartesian closed categories

Definition: A Cartesian category K is closed if for all B, C ∈ |K| we indicate [B→C] ∈ |K| and ε_B,C : [B→C] × B → C such that for all A ∈ |K| and

f : A × B → C there is a unique Λ(f ) : A → [B→C] satisfying (Λ(f ) × id_B);ε_B,C = f

[B→C] [B→C] × B -

ε_B,C

A A × B *

f

C 6

∃! Λ(f )

6 Λ(f ) × id_B

× B -

K K

(10)

Cartesian closed categories

[B→C] [B→C] × B -

ε_B,C

A A × B *

f

C 6

∃! Λ(f )

6 Λ(f ) × id_B

× B -

K K

(11)

Cartesian closed categories

[B→C] [B→C] × B -

ε_B,C

A A × B *

f

C 6

∃! Λ(f )

6 Λ(f ) × id_B

× B -

K K

(12)

Cartesian closed categories

[B→C] [B→C] × B -

ε_B,C

A A × B *

f

C 6

∃! Λ(f )

6 Λ(f ) × id_B

× B -

K K

(13)

Cartesian closed categories

[B→C] [B→C] × B -

ε_B,C

A A × B *

f

C 6

∃! Λ(f )

6 Λ(f ) × id_B

× B -

K K

(14)

Cartesian closed categories

[B→C] [B→C] × B -

ε_B,C

A A × B *

f

C 6

∃! Λ(f )

6 Λ(f ) × id_B

× B -

K K

(15)

Cartesian closed categories

[B→C] [B→C] × B -

ε_B,C

A A × B *

f

C 6

∃! Λ(f )

6 Λ(f ) × id_B

× B -

K K

(16)

Cartesian closed categories

[B→C] [B→C] × B -

ε_B,C

A A × B *

f

C 6

∃! Λ(f )

6 Λ(f ) × id_B

× B -

K K

BTW: for g : A → A⁰ and h : B → B⁰

g × h = hπ_A,B;g, π_A,B⁰ ;hi : A × B → A⁰ × B⁰

(17)

Cartesian closed categories

[B→C] [B→C] × B -

ε_B,C

A A × B *

f

C 6

∃! Λ(f )

6 Λ(f ) × id_B

× B -

K K

Examples: Set, Cpo, Cat, . . .

Heyting semilattices (b ⇐ c is such that for all a, a ∧ b ≤ c iff a ≤ (b ⇐ c)) Non-examples: Pfn, T_Σ,Φ^op .

(18)

Cartesian closed categories

[B→C] [B→C] × B -

ε_B,C

A A × B *

f

C 6

∃! Λ(f )

6 Λ(f ) × id_B

× B -

K K

(19)

Cartesian closed categories

[B→C] [B→C] × B -

ε_B,C

A A × B *

f

C 6

∃! Λ(f )

6 Λ(f ) × id_B

× B -

K K

(20)

Summing up

A category K is a Cartesian closed category (CCC ) if:

• C : K → 1 has a right adjoint C₁: 1 → K, yielding 1 ∈ |K|.

• ∆ : K → K × K has a right adjoint × : K × K → K with counit given by π_A,B : A × B → A and π_A,B⁰ : A × B → B for A, B ∈ |K|.

• for each B ∈ |K|, × B : K → K has right adjoint [B→ ] : K → K, with counit given by ε_B,C : [B→C] × B → C, for C ∈ |K|.

(21)

Summing up

A category K is a Cartesian closed category (CCC) if:

(22)

Summing up

(23)

Summing up

(24)

Summing up

(25)

Spelling this out

• 1 ∈ |K|

− for A ∈ |K|: hi_A: A → 1 such that hi_A = f for all f : A → 1.

• for A, B ∈ |K|, A × B ∈ |K|, π_A,B : A × B → A, π_A,B⁰ : A × B → B:

− for C ∈ |K|, for f : C → A, g : C → B: hf, gi : C → A × B such that

− hf, gi;π_A,B = f and hf, gi;π_A,B⁰ = g

− for h : C → A × B, h = hh;π_A,B, h;π_A,B⁰ i

• for B, C ∈ |K|, [B→C] ∈ |K|, ε_B,C : [B→C] × B → C:

− for A ∈ |K|, for f : A × B → C: Λ(f ) : A → [B→C] such that

− (Λ(f ) × id_B);ε_B,C = f

− for h : A → [B→C], Λ((h × id_B);ε_B,C) = h.

(26)

Spelling this out

• 1 ∈ |K|

− (Λ(f ) × id_B);ε_B,C = f

(27)

Spelling this out

• 1 ∈ |K|

− (Λ(f ) × id_B);ε_B,C = f

(28)

Spelling this out

• 1 ∈ |K|

− (Λ(f ) × id_B);ε_B,C = f

(29)

Spelling this out

• 1 ∈ |K|

− (Λ(f ) × id_B);ε_B,C = f

(30)

Spelling this out

• 1 ∈ |K|

− (Λ(f ) × id_B);ε_B,C = f

(31)

Spelling this out

• 1 ∈ |K|

− (Λ(f ) × id_B);ε_B,C = f

(32)

Spelling this out

• 1 ∈ |K|

− (Λ(f ) × id_B);ε_B,C = f

(33)

Spelling this out

• 1 ∈ |K|

− (Λ(f ) × id_B);ε_B,C = f

(34)

Spelling this out

• 1 ∈ |K|

− (Λ(f ) × id_B);ε_B,C = f

(35)

Spelling this out

• 1 ∈ |K|

− (Λ(f ) × id_B);ε_B,C = f

(36)

Typed λ-calculus with products

Types The set T of types τ ∈ T is such that

• 1 ∈ T

• τ ×τ⁰ ∈ T , for all τ, τ⁰ ∈ T

• τ →τ⁰ ∈ T , for all τ, τ⁰ ∈ T Note:

T need

not be the least such that.. .

Contexts Contexts Γ are of the form:

• x₁:τ₁, . . . , x_n:τ_n,

where n ≥ 0, x₁, . . . , x_n are distinct variables, and τ₁, . . . , τ_n ∈ T

(37)

Typed λ-calculus with products

• 1 ∈ T

• τ ×τ⁰ ∈ T , for all τ, τ⁰ ∈ T

T need

• x₁:τ₁, . . . , x_n:τ_n,

(38)

Typed λ-calculus with products

• 1 ∈ T

• τ ×τ⁰ ∈ T , for all τ, τ⁰ ∈ T

T need

• x₁:τ₁, . . . , x_n:τ_n,

(39)

Typed λ-calculus with products

• 1 ∈ T

• τ ×τ⁰ ∈ T , for all τ, τ⁰ ∈ T

T need

• x₁:τ₁, . . . , x_n:τ_n,

(40)

Typed λ-calculus with products

• 1 ∈ T

• τ ×τ⁰ ∈ T , for all τ, τ⁰ ∈ T

T need

• x₁:τ₁, . . . , x_n:τ_n,

(41)

Typed λ-calculus with products

• 1 ∈ T

• τ ×τ⁰ ∈ T , for all τ, τ⁰ ∈ T

T need

• x₁:τ₁, . . . , x_n:τ_n,

(42)

Typed λ-calculus with products

• 1 ∈ T

• τ ×τ⁰ ∈ T , for all τ, τ⁰ ∈ T

T need

• x₁:τ₁, . . . , x_n:τ_n,

(43)

Typed λ-calculus with products

• 1 ∈ T

• τ ×τ⁰ ∈ T , for all τ, τ⁰ ∈ T

T need

• x₁:τ₁, . . . , x_n:τ_n,

(44)

Typed terms in contexts

Γ ` t : τ

Typing/formation rules coming next Omitting the usual definitions, like:

• free variables FV (M ),

• substitution M [N/x], etc. Same for the usual simple properties, like:

• weakening — context extension;

• subject reduction;

• uniqueness of types;

• removing unused variables from contexts;

etc

(45)

Typed terms in contexts

Γ ` t : τ

etc

(46)

Typed terms in contexts

Γ ` t : τ

etc

(47)

Typed terms in contexts

Γ ` t : τ

Typing/formation rules coming next

Omitting the usual definitions, like:

etc

(48)

Typed terms in contexts

Γ ` t : τ

etc

(49)

Typed terms in contexts

Γ ` t : τ

etc

(50)

Typed terms in contexts

Γ ` t : τ

etc

(51)

Typed terms in contexts

Γ ` t : τ

etc

(52)

Typed terms in contexts

Γ ` t : τ

etc

(53)

Typed terms in contexts

Γ ` t : τ

etc

(54)

Typed terms in contexts

Γ ` t : τ

etc

(55)

Typing rules

x₁:τ₁, . . . , x_n:τ_n ` x_i: τ_i x₁:τ₁, . . . , x_n:τ_n ` M : τ

x₁:τ₁, . . . , x_i−1:τ_i−1, x_i+1:τ_i+1, . . . , x_n:τ_n ` λx_i:τ_i.M : τ_i→τ Γ ` M : τ →τ⁰ Γ ` N : τ

Γ ` M N : τ⁰

Γ ` hi : 1

Γ ` M : τ Γ ` N : τ⁰ Γ ` hM, N i : τ ×τ⁰

Γ ` π_τ,τ⁰ : τ ×τ⁰→τ Γ ` π_τ,τ⁰ ⁰ : τ ×τ⁰→τ⁰

(56)

Typing rules

Γ ` M N : τ⁰

Γ ` hi : 1

Γ ` M : τ Γ ` N : τ⁰ Γ ` hM, N i : τ ×τ⁰

Γ ` π_τ,τ⁰ : τ ×τ⁰→τ Γ ` π_τ,τ⁰ ⁰ : τ ×τ⁰→τ⁰

(57)

Typing rules

Γ ` M N : τ⁰

Γ ` hi : 1

Γ ` M : τ Γ ` N : τ⁰ Γ ` hM, N i : τ ×τ⁰

Γ ` π_τ,τ⁰ : τ ×τ⁰→τ Γ ` π_τ,τ⁰ ⁰ : τ ×τ⁰→τ⁰

(58)

Typing rules

Γ ` M N : τ⁰

Γ ` hi : 1

Γ ` M : τ Γ ` N : τ⁰ Γ ` hM, N i : τ ×τ⁰

Γ ` π_τ,τ⁰ : τ ×τ⁰→τ Γ ` π_τ,τ⁰ ⁰ : τ ×τ⁰→τ⁰

(59)

Typing rules

Γ ` M N : τ⁰

Γ ` hi : 1

Γ ` M : τ Γ ` N : τ⁰ Γ ` hM, N i : τ ×τ⁰

Γ ` π_τ,τ⁰ : τ ×τ⁰→τ Γ ` π_τ,τ⁰ ⁰ : τ ×τ⁰→τ⁰

(60)

Typing rules

Γ ` M N : τ⁰

Γ ` hi : 1

Γ ` M : τ Γ ` N : τ⁰ Γ ` hM, N i : τ ×τ⁰

Γ ` π_τ,τ⁰ : τ ×τ⁰→τ Γ ` π_τ,τ⁰ ⁰ : τ ×τ⁰→τ⁰

(61)

Semantics

Let K be an arbitrary but fixed CCC.

• Types denote objects, [[τ ]] ∈ |K|, where:

− [[1]] = 1

− [[τ ×τ⁰]] = [[τ ]] × [[τ⁰]]

− [[τ →τ⁰]] = [[[τ ]]→[[τ⁰]]]

• So do contexts:

− [[x₁:τ₁, . . . , x_n:τ_n]] = [[τ₁]] × . . . × [[τ_n]]

• Terms denote morphisms:

Weakening – context extension:

If Γ ` M : τ then Γ, Γ⁰ ` M : τ

− [[M ]]^Γ: [[Γ]] → [[τ ]],

− [[M ]]^Γ,Γ⁰ : [[Γ, Γ⁰]] → [[τ ]], and [[M ]]^Γ,Γ⁰ = ρ;π_[[Γ]],[[Γ⁰_]];[[M ]]^Γ where ρ : [[Γ, Γ⁰]] → [[Γ]] × [[Γ⁰]]

is the obvious isomorphism.

defined by induction on the derivation of Γ ` M : τ (coming next).

(62)

Semantics

− [[1]] = 1

− [[τ ×τ⁰]] = [[τ ]] × [[τ⁰]]

− [[τ →τ⁰]] = [[[τ ]]→[[τ⁰]]]

• So do contexts:

− [[x₁:τ₁, . . . , x_n:τ_n]] = [[τ₁]] × . . . × [[τ_n]]

− [[M ]]^Γ: [[Γ]] → [[τ ]],

(63)

Semantics

− [[1]] = 1

− [[τ ×τ⁰]] = [[τ ]] × [[τ⁰]]

− [[τ →τ⁰]] = [[[τ ]]→[[τ⁰]]]

• So do contexts:

− [[x₁:τ₁, . . . , x_n:τ_n]] = [[τ₁]] × . . . × [[τ_n]]

− [[M ]]^Γ: [[Γ]] → [[τ ]],

(64)

Semantics

− [[1]] = 1

− [[τ ×τ⁰]] = [[τ ]] × [[τ⁰]]

− [[τ →τ⁰]] = [[[τ ]]→[[τ⁰]]]

• So do contexts:

− [[x₁:τ₁, . . . , x_n:τ_n]] = [[τ₁]] × . . . × [[τ_n]]

− [[M ]]^Γ: [[Γ]] → [[τ ]],

(65)

Semantics

− [[1]] = 1

− [[τ ×τ⁰]] = [[τ ]] × [[τ⁰]]

− [[τ →τ⁰]] = [[[τ ]]→[[τ⁰]]]

• So do contexts:

− [[x₁:τ₁, . . . , x_n:τ_n]] = [[τ₁]] × . . . × [[τ_n]]

− [[M ]]^Γ: [[Γ]] → [[τ ]],

(66)

Semantics

− [[1]] = 1

− [[τ ×τ⁰]] = [[τ ]] × [[τ⁰]]

− [[τ →τ⁰]] = [[[τ ]]→[[τ⁰]]]

• So do contexts:

− [[x₁:τ₁, . . . , x_n:τ_n]] = [[τ₁]] × . . . × [[τ_n]]

− [[M ]]^Γ: [[Γ]] → [[τ ]],

(67)

Semantics

− [[1]] = 1

− [[τ ×τ⁰]] = [[τ ]] × [[τ⁰]]

− [[τ →τ⁰]] = [[[τ ]]→[[τ⁰]]]

• So do contexts:

− [[x₁:τ₁, . . . , x_n:τ_n]] = [[τ₁]] × . . . × [[τ_n]]

− [[M ]]^Γ: [[Γ]] → [[τ ]],

(68)

Semantics

− [[1]] = 1

− [[τ ×τ⁰]] = [[τ ]] × [[τ⁰]]

− [[τ →τ⁰]] = [[[τ ]]→[[τ⁰]]]

• So do contexts:

− [[x₁:τ₁, . . . , x_n:τ_n]] = [[τ₁]] × . . . × [[τ_n]]

− [[M ]]^Γ: [[Γ]] → [[τ ]],

[[M ]] : [[Γ]] → [[τ ]]

(69)

Semantics

− [[1]] = 1

− [[τ ×τ⁰]] = [[τ ]] × [[τ⁰]]

− [[τ →τ⁰]] = [[[τ ]]→[[τ⁰]]]

• So do contexts:

− [[x₁:τ₁, . . . , x_n:τ_n]] = [[τ₁]] × . . . × [[τ_n]]

− [[M ]]^Γ: [[Γ]] → [[τ ]],

[[M ]] : [[Γ]] → [[τ ]]

(70)

Semantics

− [[1]] = 1

− [[τ ×τ⁰]] = [[τ ]] × [[τ⁰]]

− [[τ →τ⁰]] = [[[τ ]]→[[τ⁰]]]

• So do contexts:

− [[x₁:τ₁, . . . , x_n:τ_n]] = [[τ₁]] × . . . × [[τ_n]]

− [[M ]]^Γ: [[Γ]] → [[τ ]],

[[M ]]^Γ: [[Γ]] → [[τ ]]

(71)

Semantics

− [[1]] = 1

− [[τ ×τ⁰]] = [[τ ]] × [[τ⁰]]

− [[τ →τ⁰]] = [[[τ ]]→[[τ⁰]]]

• So do contexts:

− [[x₁:τ₁, . . . , x_n:τ_n]] = [[τ₁]] × . . . × [[τ_n]]

− [[M ]]^Γ: [[Γ]] → [[τ ]],

[[M ]]^Γ: [[Γ]] → [[τ ]]

(72)

Semantics of λ-terms

− [[x_i]] = π_i: [[Γ]] → [[τ_i]] for Γ = x₁:τ₁, . . . , x_n:τ_n, π_i is the obvious projection.

(73)

Semantics of λ-terms

x₁:τ₁, . . . , x_n:τ_n ` x_i: τ_i

(74)

Semantics of λ-terms

x₁:τ₁, . . . , x_n:τ_n ` x_i: τ_i

(75)

Semantics of λ-terms

− [[λx_i:τ_i.M ]] = Λ(ρ;[[M ]]) : [[Γ⁰]] → [[τ_i→τ ]] for Γ = x₁:τ₁, . . . , x_n:τ_n, Γ⁰ = x₁:τ₁, . . . , x_i−1:τ_i−1, x_i+1:τ_i+1, . . . , x_n:τ_n, and Γ ` M : τ , where ρ : [[Γ⁰]] × [[τ_i]] → [[Γ]] is the obvious isomorphism.

(76)

Semantics of λ-terms

− [[λx_i:τ_i.M ]] = Λ(ρ;[[M ]]) : [[Γ⁰]] → [[τ_i→τ ]] for Γ = x₁:τ₁, . . . , x_n:τ_n, Γ⁰ = x₁:τ₁, . . . , x_i−1:τ_i−1, x_i+1:τ_i+1, . . . , x_n:τ_n, and Γ ` M : τ , where ρ : [[Γ⁰]] × [[τ_i]] → [[Γ]] is the obvious isomorphism.

x₁:τ₁, . . . , x_n:τ_n ` M : τ

x₁:τ₁, . . . , x_i−1:τ_i−1, x_i+1:τ_i+1, . . . , x_n:τ_n ` λx_i:τ_i.M : τ_i→τ Given [[M ]] : [[Γ]] → [[τ ]], define [[λx_i:τ_i.M ]] : [[Γ⁰]] → [[τ_i→τ ]].

Easy: ρ;[[M ]] : [[Γ⁰]] × [[τ_i]] → [[τ ]], hence Λ(ρ;[[M ]]) : [[Γ⁰]] → [[[τ_i]]→[[τ ]]].