A Concrete Introduction to Abstract (Co)Inductive Datatypes TABLEAUX 2015

167  Download (0)

Pełen tekst

(1)

A Concrete Introduction to Abstract (Co)Inductive Datatypes

TABLEAUX 2015

Andrei Popescu

Middlesex University

School of Science and Technology

Foundations of Computing Group

(2)

Constructions and results

ˆ

Classical

ˆ

Obtained in the past 4 years in joint work with

λ

Isabelle

=

β

α

Jasmin Blanchette Isabelle Dmitriy Traytel

(3)

Overview

Part I: Datatypes

Part II: Codatatypes

(4)

Part I: Datatypes

(5)

Preliminariers: It’s All About Shape and Content

Shapes

− −

− −

− − −

● a

▲ a

1

a

2

♠ a

1

a

2

♣ a

1

a

2

a

3

Shapes filled with content from a set A = {a

1

, a

2

, . . . }

(6)

Preliminariers: It’s All About Shape and Content

Shapes

− −

− −

− − −

● a

▲ a

1

a

2

♠ a

1

a

2

a

1

a

2

a

3

Shapes filled with content from a set A = {a

1

, a

2

, . . . }

(7)

Natural Functors on Set

Set = the class of all sets

It comes with a set of shapes, say

Each element x ∈ F A consists of: a choice of a shape, say

− − −

a filling with content from A, say

(8)

Natural Functors on Set

F ∶ Set → Set is a natural functor if:

It comes with a set of shapes, say

Each element x ∈ F A consists of: a choice of a shape, say

− − −

a filling with content from A, say

(9)

Natural Functors on Set

F ∶ Set → Set is a natural functor if:

It comes with a set of shapes

, say

Each element x ∈ F A consists of: a choice of a shape, say

− − −

a filling with content from A, say

(10)

Natural Functors on Set

F ∶ Set → Set is a natural functor if:

It comes with a set of shapes, say

Each element x ∈ F A consists of: a choice of a shape, say

− − −

a filling with content from A, say

(11)

Natural Functors on Set

F ∶ Set → Set is a natural functor if:

It comes with a set of shapes, say

Each element x ∈ F A consists of:

a choice of a shape

, say

− − −

a filling with content from A, say

(12)

Natural Functors on Set

F ∶ Set → Set is a natural functor if:

It comes with a set of shapes, say

Each element x ∈ F A consists of:

a choice of a shape, say

− − −

a filling with content from A, say

(13)

Natural Functors on Set

F ∶ Set → Set is a natural functor if:

It comes with a set of shapes, say

Each element x ∈ F A consists of:

a choice of a shape, say

− − −

a filling with content from A

, say

(14)

Natural Functors on Set

F ∶ Set → Set is a natural functor if:

It comes with a set of shapes, say

Each element x ∈ F A consists of:

a choice of a shape, say

a1 a2 a3

a filling with content from A, say

(15)

Examples of Natural Functors

F A = N × A

0

1

2

− . . . F A = N + A ●

− ∎

0

1

. . .

F A = List A ●

0

1

2

− −

3

− − − . . .

F A = Stream A ?

(16)

Examples of Natural Functors

F A = N × A ●

0

1

2

− . . .

F A = N + A ●

− ∎

0

1

. . .

F A = List A ●

0

1

2

− −

3

− − − . . .

F A = Stream A ?

(17)

Examples of Natural Functors

F A = N × A ●

0

a

1

a

2

a

. . .

F A = N + A ●

− ∎

0

1

. . .

F A = List A ●

0

1

2

− −

3

− − − . . .

F A = Stream A ?

(18)

Examples of Natural Functors

F A = N × A ●

0

a

1

a

2

a

. . .

F A = N + A

− ∎

0

1

. . .

F A = List A ●

0

1

2

− −

3

− − − . . .

F A = Stream A ?

(19)

Examples of Natural Functors

F A = N × A ●

0

a

1

a

2

a

. . .

F A = N + A ●

− ∎

0

1

. . .

F A = List A ●

0

1

2

− −

3

− − − . . .

F A = Stream A ?

(20)

Examples of Natural Functors

F A = N × A ●

0

a

1

a

2

a

. . .

F A = N + A ● a

0

1

. . .

F A = List A ●

0

1

2

− −

3

− − −

. . .

F A = Stream A ?

(21)

Examples of Natural Functors

F A = N × A ●

0

a

1

a

2

a

. . .

F A = N + A ● a

0

1

. . .

F A = List A

0

1

2

− −

3

− − −

. . .

F A = Stream A ?

(22)

Examples of Natural Functors

F A = N × A ●

0

a

1

a

2

a

. . .

F A = N + A ● a

0

1

. . .

F A = List A ●

0

1

2

− −

3

− − −

. . .

F A = Stream A ?

(23)

Examples of Natural Functors

F A = N × A ●

0

a

1

a

2

a

. . .

F A = N + A ● a

0

1

. . .

F A = List A ●

0

1

a

2

a

1

a

2

3

a

1

a

2

a

3

. . .

F A = Stream A ?

(24)

Examples of Natural Functors

F A = N × A ●

0

a

1

a

2

a

. . .

F A = N + A ● a

0

1

. . .

F A = List A ●

0

1

a

2

a

1

a

2

3

a

1

a

2

a

3

. . .

F A = Stream A ?

(25)

Examples of Natural Functors

F A = N × A ●

0

a

1

a

2

a

. . .

F A = N + A ● a

0

1

. . .

F A = List A ●

0

1

a

2

a

1

a

2

3

a

1

a

2

a

3

. . .

F A = Stream A ●

− − − − . . .

(26)

Examples of Natural Functors

F A = N × A ●

0

a

1

a

2

a

. . .

F A = N + A ● a

0

1

. . .

F A = List A ●

0

1

a

2

a

1

a

2

3

a

1

a

2

a

3

. . .

F A = Stream A

a

1

a

2

a

3

a

4

. . .

(27)

Examples of Natural Functors

F A = Lazy List A ?

0

1

2

− −

3

− − −

. . .

− − − − . . .

(28)

Examples of Natural Functors

F A = Lazy List A = List A

∪ Stream A

0

1

2

− −

3

− − − . . .

− − − − . . .

(29)

Examples of Natural Functors

F A = Lazy List A = List A ∪ Stream A

0

1

2

− −

3

− − − . . .

− − − − . . .

(30)

Examples of Natural Functors

F A = Lazy List A = List A ∪ Stream A

0

1

a

2

a

1

a

2

3

a

1

a

2

a

3

. . .

a

1

a

2

a

3

a

4

. . .

(31)

Examples of Natural Functors

F A = BTree A (Full Binary Trees with leaves in A)

▲ ▲

− −

▲ −

− −

▲ ▲

− − − −

. . .

(32)

Examples of Natural Functors

F A = BTree A (Full Binary Trees with leaves in A)

▲ ▲

− −

▲ −

− −

▲ ▲

− − − −

. . .

(33)

Examples of Natural Functors

F A = BTree A (Full Binary Trees with leaves in A)

▲ ▲

a

1

a

2

▲ a

3

a

1

a

2

▲ ▲

a

1

a

2

a

3

a

4

. . .

(34)

Examples of Natural Functors

F A = BTree A (Full Binary Trees with leaves in A)

▲ ▲

− −

▲ −

− −

▲ ▲

− − − −

. . .

(35)

Examples of Natural Functors

F A = BTree A (Full Binary Trees with leaves in A)

▲ ▲

− −

▲ ▲

− − −

▲▲ ▲

− − − −

. . .

(36)

Examples of Natural Functors

F A = BTree A (Full Binary Trees with leaves in A)

▲ ▲

a

1

a

2

▲ ▲

a

1

a

2

a

3

▲▲ ▲

a

1

a

2

a

3

a

4

. . .

(37)

Functorial Action (Mapper)

A

f



B

F A

F f



F B

♣ a1 a2 a3

− − −

Keep the same shape

Apply f to the content

(38)

Functorial Action (Mapper)

A

f



B

F A

F f



F B

♣ a1 a2 a3

− − −

Keep the same shape

Apply f to the content

(39)

Functorial Action (Mapper)

A

f



B

F A

F f



F B

♣ a1 a2 a3

− − −

Keep the same shape

Apply f to the content

(40)

Functorial Action (Mapper)

A

f



B

F A

F f



F B

♣ a1 a2 a3

− − −

Keep the same shape

Apply f to the content

(41)

Functorial Action (Mapper)

A

f



B

F A

F f



F B

♣ a1 a2 a3

f a1 f a2 f a3

Keep the same shape

Apply f to the content

(42)

Commutation with the Identity Function

A

id



A

F A

F id

=id



F A

a1 a2 a3

id a1 id a2 id a3

(43)

Commutation with the Identity Function

A

id



A

F A

F id = id



F A

a1 a2 a3

id a1 id a2 id a3

(44)

Commutation with Function Composition

A

f



B

g



C

F A

F f



F (g○f )



F B

F g



F C

a1 a2 a3

f a1 f a2 f a3

g(f a1)

(g ○ f) a∣∣ 1

g(f a2) (g ○ f) a∣∣ 2

g(f a3) (g ○ f) a∣∣ 3

(45)

Bottom Line

F ∶ Set → Set

For all A → B, we have F A

f F f

→ F B such that:

F id

A

= id

FA

F (g ○ f) = F g ○ F f

Functoriality

(46)

Bottom Line

F ∶ Set → Set

For all A → B, we have F A

f F f

→ F B such that:

F id

A

= id

FA

F (g ○ f) = F g ○ F f Functoriality

(47)

Atoms

a1 a2 a3 {a1, a2, a3}

F A

FatomsA //

P A

F B P B

(48)

Atoms

a1 a2 a3

{a1, a2, a3}

F A

FatomsA //

P A

F B P B

(49)

Atoms

a1 a2 a3 {a1, a2, a3}

F A

FatomsA //

P A

F B P B

(50)

Atoms

a1 a2 a3 {a1, a2, a3}

F A

FatomsA //

F f



P A

image f



F B

FatomsB //

P B

f a1 f a2 f a3 {f a1, f a2, f a3}

(51)

Atoms

a1 a2 a3

{a1, a2, a3}

F A

FatomsA //

F f



P A

image f



F B

FatomsB //

P B

f a1 f a2 f a3 {f a1, f a2, f a3}

(52)

Atoms

a1 a2 a3 {a1, a2, a3}

F A

FatomsA //

F f



P A

image f



F B

FatomsB //

P B

f a1 f a2 f a3 {f a1, f a2, f a3}

(53)

Atoms

a1 a2 a3 {a1, a2, a3}

F A

FatomsA //

F f



P A

image f



F B

FatomsB //

P B

f a1 f a2 f a3

{f a1, f a2, f a3}

(54)

Atoms

a1 a2 a3 {a1, a2, a3}

F A

FatomsA //

F f



P A

image f



F B

FatomsB //

P B

f a1 f a2 f a3 {f a1, f a2, f a3}

(55)

Atoms

a1 a2 a3 {a1, a2, a3}

F A

FatomsA //

F f



P A

image f



F B

FatomsB //

P B

f a1 f a2 f a3 {f a1, f a2, f a3}

(56)

Bottom Line

: Natural Functors

F ∶ Set → Set

For all A → B, we have F A

f

Ð→ F B such that:

F f

F id

A

= id

FA

F (g ○ f) = F g ○ F f Functoriality

For all A, we have F A

Fatoms

Ð→ P A such that, for all

A

A → B:

f

image f ○ Fatoms

A

= Fatoms

B

○ image f Naturality

(57)

Bottom Line

: Natural Functors

F ∶ Set → Set

For all A → B, we have F A

f

Ð→ F B such that:

F f

F id

A

= id

FA

F (g ○ f) = F g ○ F f Functoriality

For all A, we have F A

Fatoms

Ð→ P A such that, for all

A

A → B:

f

image f ○ Fatoms

A

= Fatoms

B

○ image f

Naturality

(58)

Bottom Line

: Natural Functors

F ∶ Set → Set

For all A → B, we have F A

f

Ð→ F B such that:

F f

F id

A

= id

FA

F (g ○ f) = F g ○ F f Functoriality

For all A, we have F A

Fatoms

Ð→ P A such that, for all

A

A → B:

f

image f ○ Fatoms

A

= Fatoms

B

○ image f Naturality

(59)

Bottom Line: Natural Functors

F ∶ Set → Set

For all A → B, we have F A

f

Ð→ F B such that:

F f

F id

A

= id

FA

F (g ○ f) = F g ○ F f Functoriality

For all A, we have F A

Fatoms

Ð→ P A such that, for all

A

A → B:

f

image f ○ Fatoms

A

= Fatoms

B

○ image f Naturality

(60)

Examples of Natural Functors

A Ð→

f

B

F A Ð→ F

F f

B F A

Fatoms

Ð→ P A

FA= N ×A Ff(n,a) = (n,f a) Fatoms(n,a) = {a}

FA= N +A Ff(Left n) = Left n Ff(Righta) = Right (f a) Fatoms(Left n) = ∅ Fatoms(Righta) = {a}

FA= ListA Ff(a1⋅a2⋅ . . . ⋅an) =f a1⋅f a2. . .⋅f an Fatoms(a1⋅a2⋅ . . . ⋅an) = {a1,a2, . . . ,an}

FA= StreamA Ff((ai)i∈N) = (f ai)i∈N

Fatoms((ai)i∈N) = {ai ∣ i ∈ N}

(61)

Examples of Natural Functors

A Ð→

f

B F A Ð→ F

F f

B

F A

Fatoms

Ð→ P A

FA= N ×A Ff(n,a) = (n,f a) Fatoms(n,a) = {a}

FA= N +A Ff(Left n) = Left n Ff(Righta) = Right (f a) Fatoms(Left n) = ∅ Fatoms(Righta) = {a}

FA= ListA Ff(a1⋅a2⋅ . . . ⋅an) =f a1⋅f a2. . .⋅f an Fatoms(a1⋅a2⋅ . . . ⋅an) = {a1,a2, . . . ,an}

FA= StreamA Ff((ai)i∈N) = (f ai)i∈N

Fatoms((ai)i∈N) = {ai ∣ i ∈ N}

(62)

Examples of Natural Functors

A Ð→

f

B F A Ð→ F

F f

B F A

Fatoms

Ð→ P A

FA= N ×A Ff(n,a) = (n,f a) Fatoms(n,a) = {a}

FA= N +A Ff(Left n) = Left n Ff(Righta) = Right (f a) Fatoms(Left n) = ∅ Fatoms(Righta) = {a}

FA= ListA Ff(a1⋅a2⋅ . . . ⋅an) =f a1⋅f a2. . .⋅f an Fatoms(a1⋅a2⋅ . . . ⋅an) = {a1,a2, . . . ,an}

FA= StreamA Ff((ai)i∈N) = (f ai)i∈N

Fatoms((ai)i∈N) = {ai ∣ i ∈ N}

(63)

Examples of Natural Functors

A Ð→

f

B F A Ð→ F

F f

B F A

Fatoms

Ð→ P A

FA= N ×A

Ff(n,a) = (n,f a) Fatoms(n,a) = {a}

FA= N +A Ff(Left n) = Left n Ff(Righta) = Right (f a) Fatoms(Left n) = ∅ Fatoms(Righta) = {a}

FA= ListA Ff(a1⋅a2⋅ . . . ⋅an) =f a1⋅f a2. . .⋅f an Fatoms(a1⋅a2⋅ . . . ⋅an) = {a1,a2, . . . ,an}

FA= StreamA Ff((ai)i∈N) = (f ai)i∈N

Fatoms((ai)i∈N) = {ai ∣ i ∈ N}

(64)

Examples of Natural Functors

A Ð→

f

B F A Ð→ F

F f

B F A

Fatoms

Ð→ P A

FA= N ×A Ff(n,a) = (n,f a)

Fatoms(n,a) = {a}

FA= N +A Ff(Left n) = Left n Ff(Righta) = Right (f a) Fatoms(Left n) = ∅ Fatoms(Righta) = {a}

FA= ListA Ff(a1⋅a2⋅ . . . ⋅an) =f a1⋅f a2. . .⋅f an Fatoms(a1⋅a2⋅ . . . ⋅an) = {a1,a2, . . . ,an}

FA= StreamA Ff((ai)i∈N) = (f ai)i∈N

Fatoms((ai)i∈N) = {ai ∣ i ∈ N}

(65)

Examples of Natural Functors

A Ð→

f

B F A Ð→ F

F f

B F A

Fatoms

Ð→ P A

FA= N ×A Ff(n,a) = (n,f a) Fatoms(n,a) = {a}

FA= N +A Ff(Left n) = Left n Ff(Righta) = Right (f a) Fatoms(Left n) = ∅ Fatoms(Righta) = {a}

FA= ListA Ff(a1⋅a2⋅ . . . ⋅an) =f a1⋅f a2. . .⋅f an Fatoms(a1⋅a2⋅ . . . ⋅an) = {a1,a2, . . . ,an}

FA= StreamA Ff((ai)i∈N) = (f ai)i∈N

Fatoms((ai)i∈N) = {ai ∣ i ∈ N}

(66)

Examples of Natural Functors

A Ð→

f

B F A Ð→ F

F f

B F A

Fatoms

Ð→ P A

FA= N ×A Ff(n,a) = (n,f a) Fatoms(n,a) = {a}

FA= N +A

Ff(Left n) = Left n Ff(Righta) = Right (f a) Fatoms(Left n) = ∅ Fatoms(Righta) = {a}

FA= ListA Ff(a1⋅a2⋅ . . . ⋅an) =f a1⋅f a2. . .⋅f an Fatoms(a1⋅a2⋅ . . . ⋅an) = {a1,a2, . . . ,an}

FA= StreamA Ff((ai)i∈N) = (f ai)i∈N

Fatoms((ai)i∈N) = {ai ∣ i ∈ N}

(67)

Examples of Natural Functors

A Ð→

f

B F A Ð→ F

F f

B F A

Fatoms

Ð→ P A

FA= N ×A Ff(n,a) = (n,f a) Fatoms(n,a) = {a}

FA= N +A Ff(Left n) = Left n Ff(Righta) = Right (f a)

Fatoms(Left n) = ∅ Fatoms(Righta) = {a}

FA= ListA Ff(a1⋅a2⋅ . . . ⋅an) =f a1⋅f a2. . .⋅f an Fatoms(a1⋅a2⋅ . . . ⋅an) = {a1,a2, . . . ,an}

FA= StreamA Ff((ai)i∈N) = (f ai)i∈N

Fatoms((ai)i∈N) = {ai ∣ i ∈ N}

(68)

Examples of Natural Functors

A Ð→

f

B F A Ð→ F

F f

B F A

Fatoms

Ð→ P A

FA= N ×A Ff(n,a) = (n,f a) Fatoms(n,a) = {a}

FA= N +A Ff(Left n) = Left n Ff(Righta) = Right (f a) Fatoms(Left n) = ∅ Fatoms(Righta) = {a}

FA= ListA Ff(a1⋅a2⋅ . . . ⋅an) =f a1⋅f a2. . .⋅f an Fatoms(a1⋅a2⋅ . . . ⋅an) = {a1,a2, . . . ,an}

FA= StreamA Ff((ai)i∈N) = (f ai)i∈N

Fatoms((ai)i∈N) = {ai ∣ i ∈ N}

(69)

Examples of Natural Functors

A Ð→

f

B F A Ð→ F

F f

B F A

Fatoms

Ð→ P A

FA= N ×A Ff(n,a) = (n,f a) Fatoms(n,a) = {a}

FA= N +A Ff(Left n) = Left n Ff(Righta) = Right (f a) Fatoms(Left n) = ∅ Fatoms(Righta) = {a}

FA= ListA

Ff(a1⋅a2⋅ . . . ⋅an) =f a1⋅f a2. . .⋅f an Fatoms(a1⋅a2⋅ . . . ⋅an) = {a1,a2, . . . ,an}

FA= StreamA Ff((ai)i∈N) = (f ai)i∈N

Fatoms((ai)i∈N) = {ai ∣ i ∈ N}

(70)

Examples of Natural Functors

A Ð→

f

B F A Ð→ F

F f

B F A

Fatoms

Ð→ P A

FA= N ×A Ff(n,a) = (n,f a) Fatoms(n,a) = {a}

FA= N +A Ff(Left n) = Left n Ff(Righta) = Right (f a) Fatoms(Left n) = ∅ Fatoms(Righta) = {a}

FA= ListA Ff(a1⋅a2⋅ . . . ⋅an) =f a1⋅f a2. . .⋅f an

Fatoms(a1⋅a2⋅ . . . ⋅an) = {a1,a2, . . . ,an}

FA= StreamA Ff((ai)i∈N) = (f ai)i∈N

Fatoms((ai)i∈N) = {ai ∣ i ∈ N}

(71)

Examples of Natural Functors

A Ð→

f

B F A Ð→ F

F f

B F A

Fatoms

Ð→ P A

FA= N ×A Ff(n,a) = (n,f a) Fatoms(n,a) = {a}

FA= N +A Ff(Left n) = Left n Ff(Righta) = Right (f a) Fatoms(Left n) = ∅ Fatoms(Righta) = {a}

FA= ListA Ff(a1⋅a2⋅ . . . ⋅an) =f a1⋅f a2. . .⋅f an Fatoms(a1⋅a2⋅ . . . ⋅an) = {a1,a2, . . . ,an}

FA= StreamA Ff((ai)i∈N) = (f ai)i∈N

Fatoms((ai)i∈N) = {ai ∣ i ∈ N}

(72)

Examples of Natural Functors

A Ð→

f

B F A Ð→ F

F f

B F A

Fatoms

Ð→ P A

FA= N ×A Ff(n,a) = (n,f a) Fatoms(n,a) = {a}

FA= N +A Ff(Left n) = Left n Ff(Righta) = Right (f a) Fatoms(Left n) = ∅ Fatoms(Righta) = {a}

FA= ListA Ff(a1⋅a2⋅ . . . ⋅an) =f a1⋅f a2. . .⋅f an Fatoms(a1⋅a2⋅ . . . ⋅an) = {a1,a2, . . . ,an}

FA= StreamA

Ff((ai)i∈N) = (f ai)i∈N

Fatoms((ai)i∈N) = {ai ∣ i ∈ N}

(73)

Examples of Natural Functors

A Ð→

f

B F A Ð→ F

F f

B F A

Fatoms

Ð→ P A

FA= N ×A Ff(n,a) = (n,f a) Fatoms(n,a) = {a}

FA= N +A Ff(Left n) = Left n Ff(Righta) = Right (f a) Fatoms(Left n) = ∅ Fatoms(Righta) = {a}

FA= ListA Ff(a1⋅a2⋅ . . . ⋅an) =f a1⋅f a2. . .⋅f an Fatoms(a1⋅a2⋅ . . . ⋅an) = {a1,a2, . . . ,an}

FA= StreamA Ff((ai)i∈N) = (f ai)i∈N

Fatoms((ai)i∈N) = {ai ∣ i ∈ N}

(74)

Examples of Natural Functors

A Ð→

f

B F A Ð→ F

F f

B F A

Fatoms

Ð→ P A

FA= N ×A Ff(n,a) = (n,f a) Fatoms(n,a) = {a}

FA= N +A Ff(Left n) = Left n Ff(Righta) = Right (f a) Fatoms(Left n) = ∅ Fatoms(Righta) = {a}

FA= ListA Ff(a1⋅a2⋅ . . . ⋅an) =f a1⋅f a2. . .⋅f an Fatoms(a1⋅a2⋅ . . . ⋅an) = {a1,a2, . . . ,an}

FA= StreamA Ff((ai)i∈N) = (f ai)i∈N

Fatoms((ai)i∈N) = {ai ∣ i ∈ N}

(75)

Iterating Shape Composition

Natural functor F∶ Set → Set

The shapes of F: ∎ ▼ ▲

− −

− − − Put them together by plugging in shape for content slot

until there are no lingering slots left!

− − −

− − − − −

The leaves are always empty-content shapes

(76)

Iterating Shape Composition

Natural functor F∶ Set → Set

The shapes of F: ∎ ▼ ▲

− −

− − −

Put them together by plugging in shape for content slot

until there are no lingering slots left!

− − −

− − − − −

The leaves are always empty-content shapes

(77)

Iterating Shape Composition

Natural functor F∶ Set → Set Copies of the shapes of F: ∎ ▼ ▲

− −

− − −

Put them together by plugging in shape for content slot

until there are no lingering slots left!

− − −

− − − − −

The leaves are always empty-content shapes

(78)

Iterating Shape Composition

Natural functor F∶ Set → Set Copies of the shapes of F: ∎ ▼ ▲

− −

− − − Put them together by plugging in shape for content slot

until there are no lingering slots left!

− − −

− − − − −

The leaves are always empty-content shapes

(79)

Iterating Shape Composition

Natural functor F∶ Set → Set Copies of the shapes of F: ∎ ▼ ▲

− −

− − − Put them together by plugging in shape for content slot

until there are no lingering slots left!

− − −

− − − − −

The leaves are always empty-content shapes

(80)

Iterating Shape Composition

Natural functor F∶ Set → Set Copies of the shapes of F: ∎ ▼ ▲

− −

− − − Put them together by plugging in shape for content slot

until there are no lingering slots left!

▲ − −

− − − − −

The leaves are always empty-content shapes

(81)

Iterating Shape Composition

Natural functor F∶ Set → Set Copies of the shapes of F: ∎ ▼ ▲

− −

− − − Put them together by plugging in shape for content slot

until there are no lingering slots left!

▲ ∎ −

− − − − −

The leaves are always empty-content shapes

(82)

Iterating Shape Composition

Natural functor F∶ Set → Set Copies of the shapes of F: ∎ ▼ ▲

− −

− − − Put them together by plugging in shape for content slot

until there are no lingering slots left!

▲ ∎ ♣

− − − − −

The leaves are always empty-content shapes

(83)

Iterating Shape Composition

Natural functor F∶ Set → Set Copies of the shapes of F: ∎ ▼ ▲

− −

− − − Put them together by plugging in shape for content slot

until there are no lingering slots left!

▲ ∎ ♣

∎ ▼ ∎ ▼ ∎

The leaves are always empty-content shapes

(84)

Iterating Shape Composition

Natural functor F∶ Set → Set Copies of the shapes of F: ∎ ▼ ▲

− −

− − − Put them together by plugging in shape for content slot

until there are no lingering slots left!

▲ ∎ ♣

∎ ▼ ∎ ▼ ∎

The leaves are always empty-content shapes

(85)

Iterating Shape Composition

Natural functor F∶ Set → Set Copies of the shapes of F: ∎ ▼ ▲

− −

− − − Put them together by plugging in shape for content slot

until there are no lingering slots left!

▲ ∎ ♣

∎ ▼ ∎ ▼ ∎

Define I

F

= the set of all such finitary couplings

(86)

Properties of I F : Bijectivity

▲ ∎ ♣

∎ ▼ ∎ ▼ ∎

▲ ∎ ♣

∎ ▼ ∎ ▼ ∎

F I

F

I

F

dtor

OO

ctor and dtor are mutually inverse bijections

(87)

Properties of I F : Bijectivity

▲ ∎ ♣

∎ ▼ ∎ ▼ ∎

▲ ∎ ♣

∎ ▼ ∎ ▼ ∎

F I

F

I

F

dtor

OO

ctor and dtor are mutually inverse bijections

(88)

Properties of I F : Bijectivity

▲ ∎ ♣

∎ ▼ ∎ ▼ ∎

▲ ∎ ♣

∎ ▼ ∎ ▼ ∎

F I

F

ctor



I

F

dtor

OO

ctor and dtor are mutually inverse bijections

(89)

Properties of I

F

: Iteration

FIF

F A

s



IF A

f f f

s

f f f

(90)

Properties of I

F

: Iteration

FIF

F A

s



IF f //A

f f f

s

f f f

(91)

Properties of I

F

: Iteration

FIF

F A

s



IF f //A

f f f

s

f f f

(92)

Properties of I

F

: Iteration

FIF F A

s



IF f //

dtor

OO

A

f f f

s

f f f

(93)

Properties of I

F

: Iteration

FIF F A

s



IF f //

dtor

OO

A

f f f

s

f f f

(94)

Properties of I

F

: Iteration

FIF

F f //F A

s



IF f //

dtor

OO

A

f f f

s

f f f

(95)

Properties of I

F

: Iteration

FIF

F f //F A

s



IF f //

dtor

OO

A

f f f

s

f f f

(96)

Properties of I

F

: Iteration

FIF

F f //F A

s



IF f //

dtor

OO

A

f f f

s

f f f

(97)

Properties of I

F

: Iteration

FIF

F f //F A

s



IF f //

dtor

OO

A

f f f

s

f f f

(98)

Properties of I

F

: Iteration

FIF

F A

s

IF

f //A

f

I

F

is the initial F-algebra

f = iter

s

(99)

Properties of I

F

: Iteration

FIF

F A

s

IF

f //A

f

I

F

is the initial F-algebra

f = iter

s

(100)

Properties of I

F

: Iteration

FIF

F A

s



IF

f //A

s

f f f

I

F

is the initial F-algebra

f = iter

s

(101)

Properties of I

F

: Iteration

FIF

F A

s

IF

f //A

s

s s s

s s s s s

I

F

is the initial F-algebra

f = iter

s

Obraz

Updating...

Cytaty

Powiązane tematy :