Category Theory in Foundations of Computer Science Andrzej Tarlecki

(Universal Algebra and)

Category Theory

in Foundations of Computer Science

Andrzej Tarlecki

Institute of Informatics

Faculty of Mathematics, Informatics and Mechanics University of Warsaw

http://www.mimuw.edu.pl/~tarlecki office: 4750 tarlecki@mimuw.edu.pl phone: (48)(22)(55) 44475, 20443

This course: http://www.mimuw.edu.pl/~tarlecki/teaching/ct/

Universal algebra and category theory:

basic ideas, notions and some results

• Algebras, homomorphisms, equations: basic definitions and results

• Categories; examples and simple categorical definitions

• Limits and colimits

• Functors and natural transformations

• Adjunctions

• Cartesian closed categories

• Monads

• Institutions (abstract model theory, abstract specification theory)

BUT: Tell me what you want to learn!

Literature

Plenty of standard textbooks But this will be roughly based on:

• D.T. Sannella, A. Tarlecki.

Foundations of Algebraic Specifications and Formal Program Development. Springer, 2012.

− Chap. 1: Universal algebra

− Chap. 2: Simple equational specifications

− Chap. 3: Category theory

One motivation

Software systems (modules, programs, databases. . . ):

sets of data with operations on them

• Disregarding: code, efficiency, robustness, reliability, . . .

• Focusing on: CORRECTNESS

Universal algebra from rough analogy

module interface ;signature module;algebra

module specification;class of algebras

Category theory

A language to further abstract away from the standard notions of univer- sal algebra, to deal with their numer- ous variants needed in foundations of computer science.

Signatures

Algebraic signature:

Σ = (S, Ω)

• sort names: S

• operation names, classified by arities and result sorts: Ω = hΩ_w,si_w∈S^∗_,s∈S Alternatively:

Σ = (S, Ω, arity, sort )

with sort names S, operation names Ω, and arity and result sort functions

arity : Ω → S^∗ and sort : Ω → S.

• f : s₁ × . . . × s_n → s stands for s₁, . . . , s_n, s ∈ S and f ∈ Ω_s1...sn,s

Compare the two notions

Fix a signature Σ = (S, Ω) for a while.

Algebras

• Σ-algebra:

A = (|A|, hf_Ai_{f ∈Ω})

• carrier sets: |A| = h|A|_si_s∈S

• operations: f_A: |A|_s1 × . . . × |A|_sn → |A|_s, for f : s₁ × . . . × s_n → s

• the class of all Σ-algebras:

Alg(Σ)

Can Alg(Σ) be empty? Finite?

Can A ∈ Alg(Σ) have empty carriers?

Subalgebras

• for A ∈ Alg(Σ), a Σ-subalgebra A_sub ⊆ A is given by subset |A_sub| ⊆ |A| closed under the operations:

− for f : s₁ × . . . × s_n → s and a₁ ∈ |A_sub|_s1, . . . , a_n ∈ |A_sub|_sn,

f_Asub(a₁, . . . , a_n) = f_A(a₁, . . . , a_n)

• for A ∈ Alg(Σ) and X ⊆ |A|, the subalgebra of A genereted by X, hAi_X, is the least subalgebra of A that contains X.

• A ∈ Alg(Σ) is reachable if hAi_∅ coincides with A.

Fact: For any A ∈ Alg(Σ) and X ⊆ |A|, hAi_X exists.

Proof (idea):

• generate the generated subalgebra from X by closing it under operations in A; or

• the intersection of any family of subalgebras of A is a subalgebra of A.

Homomorphisms

• for A, B ∈ Alg(Σ), a Σ-homomorphism h : A → B is a function h : |A| → |B|

that preserves the operations:

− for f : s₁ × . . . × s_n → s and a₁ ∈ |A|_s1, . . . , a_n ∈ |A|_sn,

h_s(f_A(a₁, . . . , a_n)) = f_B(h_s1(a₁), . . . , h_sn(a_n)) Fact: Given a homomorphism h : A → B and subalgebras A_sub of A and B_sub of B, the image of A_sub under h, h(A_sub), is a subalgebra of B, and the coimage of B_sub under h, h⁻¹(B_sub), is a subalgebra of A.

Fact: Given a homomorphism h : A → B and X ⊆ |A|, h(hAi_X) = hBi_h(X). Fact: If two homomorphisms h₁, h₂: A → B coincide on X ⊆ |A|, then they coincide on hAi_X.

Fact: Identity function on the carrier of A ∈ Alg(Σ) is a homomorphism id_A: A → A. Composition of homomorphisms h : A → B and g : B → C is a homomorphism h;g : A → C.

Isomorphisms

• for A, B ∈ Alg(Σ), a Σ-isomorphism is any Σ-homomorphism i : A → B that has an inverse, i.e., a Σ-homomorphism i⁻¹: B → A such that i;i⁻¹ = id_A and i⁻¹;i = id_B.

• Σ-algebras are isomorphic if there exists an isomorphism between them.

Fact: A Σ-homomorphism is a Σ-isomorphism iff it is bijective (“1-1” and “onto”).

Fact: Identities are isomorphisms, and any composition of isomorphisms is an isomorphism.

Congruences

• for A ∈ Alg(Σ), a Σ-congruence on A is an equivalence ≡ ⊆ |A| × |A| that is closed under the operations:

− for f : s₁ × . . . × s_n → s and a₁, a₁⁰ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn,

if a₁ ≡_s1 a₁⁰ , . . . , a_n ≡_sn a⁰_n then f_A(a₁, . . . , a_n) ≡_s f_A(a⁰₁, . . . , a⁰_n).

Fact: For any relation R ⊆ |A| × |A| on the carrier of a Σ-algebra A, there exists the least congruence on A that conatins R.

Fact: For any Σ-homomorphism h : A → B, the kernel of h, K(h) ⊆ |A| × |A|, where a K(h) a⁰ iff h(a) = h(a⁰), is a Σ-congruence on A.

Quotients

• for A ∈ Alg(Σ) and Σ-congruence ≡ ⊆ |A| × |A| on A, the quotient algebra A/≡ is built in the natural way on the equivalence classes of ≡:

− for s ∈ S, |A/≡|_s = {[a]_≡ | a ∈ |A|_s}, with [a]_≡ = {a⁰ ∈ |A|_s | a ≡ a⁰}

− for f : s₁ × . . . × s_n → s and a₁ ∈ |A|_s1, . . . , a_n ∈ |A|_sn,

f_A/≡([a₁]≡, . . . , [a_n]≡) = [f_A(a₁, . . . , a_n)]≡

Fact: The above is well-defined; moreover, the natural map that assigns to every element its equivalence class is a Σ-homomorphisms [ ]_≡: A → A/≡.

Fact: Given two Σ-congruences ≡ and ≡⁰ on A, ≡ ⊆ ≡⁰ iff there exists a Σ-homomorphism h : A/≡ → A/≡⁰ such that [ ]_≡;h = [ ]_≡⁰.

Fact: For any Σ-homomorphism h : A → B, A/K(h) is isomorphic with h(A).

Products

• for A_i ∈ Alg(Σ), i ∈ I, the product of hA_ii_i∈I, Q

i∈I A_i is built in the natural way on the Cartesian product of the carriers of A_i, i ∈ I:

− for s ∈ S, |Q

i∈I A_i|_s = Q

i∈I |A_i|_s

− for f : s₁ × . . . × s_n → s and a₁ ∈ | Q

i∈I A_i|_s1, . . . , a_n ∈ |Q

i∈I A_i|_sn, for i ∈ I, f^Q

i∈I A_i(a₁, . . . , a_n)(i) = f_Ai(a₁(i), . . . , a_n(i))

Fact: For any family hA_ii_i∈I of Σ-algebras, projections π_i(a) = a(i), where i ∈ I and a ∈ Q

i∈I |A_i|, are Σ-homomorphisms π_i: Q

i∈I A_i → A_i.

Define the product of the empty family of Σ-algebras.

When the projection π_i is an isomorphism?

Terms

Consider an S-sorted set X of variables.

• terms t ∈ |T_Σ(X)| are built using variables X, constants and operations from Ω in the usual way: |T_Σ(X)| is the least set such that

− X ⊆ |T_Σ(X)|

− for f : s₁ × . . . × s_n → s and t₁ ∈ |T_Σ(X)|_s1, . . . , t_n ∈ |T_Σ(X)|_sn, f (t₁, . . . , t_n) ∈ |T_Σ(X)|_s

• for any Σ-algebra A and valuation v : X → |A|, the value t_A[v] of a term t ∈ |T_Σ(X)| in A under v is determined inductively:

− x_A[v] = v_s(x), for x ∈ X_s, s ∈ S

− (f (t₁, . . . , t_n))_A[v] = f_A((t₁)_A[v], . . . , (t_n)_A[v]), for f : s₁ × . . . × s_n → s and t₁ ∈ |T_Σ(X)|_s1, . . . , t_n ∈ |T_Σ(X)|_sn

Above and in the following: assuming unambiguous “parsing” of terms!

Term algebras

Consider an S-sorted set X of variables.

• The term algebra T_Σ(X) has the set of terms as the carrier and operations defined “syntactically”:

− for f : s₁ × . . . × s_n → s and t₁ ∈ |T_Σ(X)|_s1, . . . , t_n ∈ |T_Σ(X)|_sn, f_TΣ(X)(t₁, . . . , t_n) = f (t₁, . . . , t_n).

Fact: For any S-sorted set X of variables, Σ-algebra A and valuation v : X → |A|, there is a unique Σ-homomorphism v^#: T_Σ(X) → A that extends v. Moreover, for t ∈ |T_Σ(X)|, v^#(t) = t_A[v].

X |T_Σ(X)|

|A|

T_Σ(X)

A -

HH

HH

HH

HH H

j ? ?

id_{X ,→|TΣ(X )|}

v |v^#| ∃! v^#

Set^S Alg(Σ)

One simple consequence

Fact: For any S-sorted sets X, Y and Z (of variables) and substitutions θ₁: X → |T_Σ(Y )| and θ₂ : Y → |T_Σ(Z)|

θ₁^#;θ₂^# = (θ₁;θ₂^#)^#

X |T_Σ(X)|

Y |T_Σ(Y )|

|T_Σ(Z)|

T_Σ(X)

T_Σ(Y )

T_Σ(Z) -

HH

HH

HH

HHHj ? ?

id_{X ,→|TΣ(X )|}

θ₁ θ₁^# ∃! θ₁^#

- HH

HH

HH

HHHj ? ?

id_{X ,→|TΣ(Y )|}

θ₂ θ₂^# ∃! θ₂^#

$

%



∃! (θ₁;θ₂^#)^#

Set^S Alg(Σ)

Equations

• Equation:

∀X.t = t⁰ where:

− X is a set of variables, and

− t, t⁰ ∈ |T_Σ(X)|_s are terms of a common sort.

• Satisfaction relation: Σ-algebra A satisfies ∀X.t = t⁰ A |= ∀X.t = t⁰

when for all v : X → |A|, t_A[v] = t⁰_A[v].

Semantic entailment

Φ |=_Σ ϕ

Σ-equation ϕ is a semantic consequence of a set of Σ-equations Φ if ϕ holds in every Σ-algebra that satisfies Φ.

BTW:

• Models of a set of equations: Mod (Φ) = {A ∈ Alg(Σ) | A |= Φ}

• Theory of a class of algebras: Th(C) = {ϕ | C |= ϕ}

• Φ |= ϕ ⇐⇒ ϕ ∈ Th(Mod (Φ))

• Mod and Th form a Galois connection

Equational specifications

hΣ, Φi

• signature Σ, to determine the static module interface

• axioms (Σ-equations), to determine required module properties BUT:

Fact: A class of Σ-algebras is equationally definable iff it is closed under subalgebras, products and homomorphic images.

Equational specifications typically admit a lot of undesirable “modules”

Example

spec NaiveNat = sort Nat ops 0: Nat;

succ : Nat → Nat;

+ : Nat × Nat → Nat axioms ∀n:Nat • n + 0 = n;

∀n,m:Nat • n + succ(m) = succ(n + m) Now:

NaiveNat 6|= ∀n,m:Nat • n + m = m + n

How to fix this

• Other (stronger) logical systems: conditional equations, first-order logic, higher-order logics, other bells-and-whistles

− more about this elsewhere. . .













 Institutions!

• Constraints:

− reachability (and generation): “no junk”

− initiality (and freeness): “no junk” & “no confusion”

Constraints can be thought of as special (higher-order) formulae.

There has been a population explosion among logical systems. . .

Initial models

Fact: Every equational specification hΣ, Φi has an initial model: there exists a Σ-algebra I ∈ Mod (Φ) such that for every Σ-algebra M ∈ Mod (Φ) there exists a unique Σ-homomorphism from I to M.

Proof (idea):

• I is the quotient of the algebra of ground Σ-terms by the congruence that glues together all ground terms t, t⁰ such that Φ |= ∀∅.t = t⁰.

• I is the reachable subalgebra of the product of “all” (up to isomorphism) reachable algebras in Mod (Φ).

BTW: This can be generalised to the existence of a free model of hΣ, Φi over any (many-sorted) set of data.

Example

spec Nat = free { sort Nat ops 0: Nat;

succ : Nat → Nat;

+ : Nat × Nat → Nat axioms ∀n:Nat • n + 0 = n;

∀n,m:Nat • n + succ(m) = succ(n + m) }

Now:

Nat |= ∀n,m:Nat • n + m = m + n

Example

spec Nat⁰ = free type Nat ::= 0 | succ(Nat) op + : Nat × Nat → Nat axioms ∀n:Nat • n + 0 = n;

∀n,m:Nat • n + succ(m) = succ(n + m)

Nat ≡ Nat⁰

Another example

spec String =

generated { sort String

ops nil : String;

a, . . . ,z: String;

b : String × String → String } axioms ∀s:String • s b nil = s;

∀s:String • nil b s = s;

∀s,t,v:String • s b (t b v) = (s b t) b v }

Equational calculus

∀X.t = t

∀X.t = t⁰

∀X.t⁰ = t

∀X.t = t⁰ ∀X.t⁰ = t⁰⁰

∀X.t = t⁰⁰

∀X.t₁ = t⁰₁ . . . ∀X.t_n = t⁰_n

∀X.f (t₁ . . . t_n) = f (t⁰₁ . . . t⁰_n)

∀X.t = t⁰

∀Y.t[θ] = t⁰[θ] for θ : X → |T_Σ(Y )|

Mind the variables!

a = b does not follow from a = f (x) and f (x) = b, unless. . .

Proof-theoretic entailment

Φ `_Σ ϕ

Σ-equation ϕ is a proof-theoretic consequence of a set of Σ-equations Φ if ϕ can be derived from Φ by the rules.

How to justify this?

Semantics!

Soundness & completeness

Fact: The equational calculus is sound and complete:

Φ |= ϕ ⇐⇒ Φ ` ϕ

• soundness: “all that can be proved, is true” (Φ |= ϕ ⇐= Φ ` ϕ)

• completeness: “all that is true, can be proved” (Φ |= ϕ =⇒ Φ ` ϕ) Proof (idea):

• soundness: easy!

• completeness: not so easy!

Moving between signatures

Let Σ = (S, Ω) and Σ⁰ = (S⁰, Ω⁰)

σ : Σ → Σ⁰

• Signature morphism maps:

− sorts to sorts: σ : S → S⁰

− operation names to operation names, preserving their profiles:

σ : Ω_w,s → Ω⁰_σ(w),σ(s), for w ∈ S^∗, s ∈ S, that is: for f : s₁ × . . . × s_n → s, σ(f ) : σ(s₁) × . . . × σ(s_n) → σ(s),

Let σ : Σ → Σ⁰

Translating syntax

• translation of variables: X 7→ X⁰, where X_s⁰0 = U

σ(s)=s⁰ X_s

• translation of terms: σ : |T_Σ(X)|_s → |T_Σ⁰(X⁰)|_σ(s), for s ∈ S

• translation of equations: σ(∀X.t₁ = t₂) yields ∀X⁰.σ(t₁) = σ(t₂)

. . . and semantics

• σ-reduct: _σ : Alg(Σ⁰) → Alg(Σ), where for A⁰ ∈ Alg(Σ⁰)

− |A⁰ _σ|_s = |A⁰|_σ(s), for s ∈ S

− f_A0

σ = σ(f )_A⁰ for f ∈ Ω

Note the contravariancy!

Satisfaction condition

Fact: For all signature morphisms σ : Σ → Σ⁰, Σ⁰-algebras A⁰ and Σ-equations ϕ:

A⁰ _σ |=_Σ ϕ ⇐⇒ A⁰ |=_Σ⁰ σ(ϕ)

Proof (idea): for t ∈ |T_Σ(X)| and v : X → |A⁰ _σ|, t_A0

σ[v] = σ(t)_A⁰[v⁰], where v⁰: X⁰ → |A⁰| is given by v_σ(s)⁰ (x) = v_s(x) for s ∈ S, x ∈ X_s.

TRUTH is preserved (at least) under:

• change of notation

• restriction/extension of irrelevant context

Preservation of consequence

Given any signature morphism σ : Σ → Σ⁰, set of Σ-equations Φ and Σ-equation ϕ:

Φ |=_Σ ϕ =⇒ σ(Φ) |=_Σ⁰ σ(ϕ)

Moreover, if _σ : Alg(Σ⁰) → Alg(Σ) is surjective then:

Φ |=_Σ ϕ ⇐⇒ σ(Φ) |=_Σ⁰ σ(ϕ)





 In general, the equivalence does not hold!

Specification morphisms

Specification morphism:

σ : hΣ, Φi → hΣ⁰, Φ⁰i

is a signature morphism σ : Σ → Σ⁰ such that for all M⁰ ∈ Alg(Σ⁰):

M⁰ ∈ Mod (Φ⁰) =⇒ M⁰ _σ ∈ Mod (Φ) 

 Then _σ : Mod (Φ⁰) → Mod (Φ)

Fact: A signature morphism σ : Σ → Σ⁰ is a specification morphism σ : hΣ, Φi → hΣ⁰, Φ⁰i if and only if Φ⁰ |= σ(Φ) .

Conservativity

A specification morphism:

σ : hΣ, Φi → hΣ⁰, Φ⁰i

is conservative if for all Σ-equations ϕ: Φ⁰ |=_Σ⁰ σ(ϕ) =⇒ Φ |=_Σ ϕ







 BTW: for all specification morphisms

Φ |=_Σ ϕ =⇒ Φ⁰ |=_Σ⁰ σ(ϕ)

A specification morphism σ : hΣ, Φi → hΣ⁰, Φ⁰i admits model expansion if for each M ∈ Mod (Φ) there exists M⁰ ∈ Mod (Φ⁰) such that M⁰ _σ = M

(i.e., _σ : Mod (Φ⁰) → Mod (Φ) is surjective).

Fact: If σ : hΣ, Φi → hΣ⁰, Φ⁰i admits model expansion then it is conservative.





 In general, the equivalence does not hold!

More general signature morphisms

Let Σ = (S, Ω) and Σ⁰ = (S⁰, Ω⁰)

δ : Σ → Σ⁰

• Derived signature morphism maps sorts to sorts: δ : S → S⁰, and operation names to terms, preserving their profiles: for f : s₁ × . . . × s_n → s,

δ(f ) ∈ |T_Σ⁰({x₁:δ(s₁), . . . , x_n:δ(s_n)})|_δ(s)

• Translation of syntax, reducts of algebras, satisfaction condition, and many other notions and results: similarly as before. 

 not quite all though. . .

Partial algebras

• Algebraic signature Σ: as before

• Partial Σ-algebra:

A = (|A|, hf_Ai_{f ∈Ω})

as before, but operations f_A: |A|_s1 × . . . × |A|_sn * |A|_s, for f : s₁ × . . . × s_n → s, may now be partial functions.

 BTW: Constants may be undefined as well.

• PAlg(Σ) stands for the class of all partial Σ-algebras.

Fix a signature Σ = (S, Ω) for a while.

Few further notions

• subalgebra A_sub ⊆ A: given by subset |A_sub| ⊆ |A| closed under the operations;

(BTW: at least two other natural notions are possible)

• homomorphism h : A → B: map h : |A| → |B| that preserves definedness and results of operations; it is strong if in addition it reflects definedness of

operations; (strong) homomorphisms are closed under composition;

(BTW: very interesting alternative: partial map h : |A| * |B| that preserves results of operations)

• congruence ≡ on A: equivalence ≡ ⊆ |A| × |A| closed under the operations whenever they are defined; it is strong if in addition it reflects definedness of operations; (strong) congruences are kernels of (strong) homomorphisms;

• quotient algebra A/≡: built in the natural way on the equivalence classes of ≡;

the natural homomorphism from A to A/≡ is strong if the congruence is strong.

Formulae

(Strong) equation:

∀X.t = t^{s 0}

as before

Definedness formula:

∀X.def t

where X is a set of variables, and t ∈

|T_Σ(X)|_s is a term Satisfaction relation

partial Σ-algebra A satisfies ∀X.t = t^{s 0} A |= ∀X.t = t^{s 0}

when for all v : X → |A|, t_A[v] is de- fined iff t⁰_A[v] is defined, and then t_A[v] = t⁰_A[v]

partial Σ-algebra A satisfies ∀X.def t A |= ∀X.def t

when for all v : X → |A|, t_A[v] is defined

An alternative

• (Existence) equation:

∀X.t = t^{e 0} where:

− X is a set of variables, and

− t, t⁰ ∈ |T_Σ(X)|_s are terms of a common sort.

• Satisfaction relation: Σ-algebra A satisfies ∀X.t = t^{e 0} A |= ∀X.t = t^{e 0}

when for all v : X → |A|, t_A[v] = t⁰_A[v] — both sides are defined and equal.

BTW:

• ∀X.t = t^{e 0} iff ∀X.(t = t^{s 0} ∧ def t)

• ∀X.t = t^{s 0} iff ∀X.(def t ⇐⇒ def t⁰) ∧ (def t =⇒ t = t^{e 0})

Further notions and results

To introduce and/or check:

• partial equational specifications (trivial)

• characterization of definable classes of partial algebras (difficult!)

• existence of initial models for partial equational specifications (non-trivial for existence equations; difficult for strong equations and definedness formulae)

• proof systems for partial equational logic (ditto)

• signature morphisms, translation of formulae, reducts of partial algebras, satisfaction condition; specification morphisms, conservativity, etc. (easy)

• even more general signature morphisms: δ : Σ → Σ⁰ maps sort names to sort names, and operation names f : s₁ × . . . s_n → s to sequences hϕ_i, t_ii_i≥0, where ϕ_i is a Σ⁰-formula and t_i is a Σ⁰-term of sort δ(s), both with variables among x₁:δ(s₁), . . . , x_n:δ(s_n); syntax does not quite translate, but reducts are well defined. . .

Example

spec NatPred = free { sort Nat ops 0: Nat;

succ : Nat → Nat;

+ : Nat × Nat → Nat pred : Nat →? Nat

axioms ∀n:Nat • n + 0 = n;

∀n,m:Nat • n + succ(m) = succ(n + m)

∀n:Nat • pred(succ(n)) =^s n;

}

Example

spec NatPred⁰ = free type Nat ::= 0 | succ(pred :? Nat) op + : Nat × Nat → Nat

axioms ∀n:Nat • n + 0 = n;

∀n,m:Nat • n + succ(m) = succ(n + m)

NatPred ≡ NatPred⁰