Seminář 5: Kartézské uzavřené kategorie a λ-kalkul
Exponenciál (function object)
Nechť C je kategorie a a, b ∈ C. Exponenciál [a ⇒ b] (alternativní značení: ba
) je objekt takový, že:
• existuje morfismus eval : ([a ⇒ b] × a) → b
• pro každý další objekt z s morfismem g : z×a → b existuje unikátní morfismus h : z → (a → b),
který faktorizuje g skrz eval, tedy g = eval ◦ (h × id)
[a ⇒ b] × a
z × a b
evala
b
g
h×ida
Kartézská uzavřená kategorie
Kategorie C se nazývá kartézská uzavřená (CCC), pokud splňuje následující podmínky:
• obsahuje terminální objekt
• pro každou dvojici objektů a, b ∈ C obsahuje jejich produkt a × b
• pro každou dvojici objektů a, b ∈ C obsahuje jejich exponenciál [a ⇒ b]
Příklady CCC:
• Set - exponenciál [a ⇒ b] je množina funkcí mezi a a b.
• Booleova algebra - morfismy jsou ≤, terminální objekt je 1, produkt a × b je infimum a ∧ b,
exponenciál [a ⇒ b] je „implikace“ ¬a ∨ b
Bikartézská uzavřená kategorie
Kategorie C se nazývá bikartézská uzavřená (BCCC), pokud je kartézská uzavřená a navíc splňuje
následující podmínky:
• obsahuje iniciální objekt
• pro každou dvojici objektů a, b ∈ C obsahuje jejich koprodukt a + b
(Typovaný) λ-kalkul
Korektní výrazy λ-kalkulu:
• každá proměnná x
• pokud t je výraz a x je proměnná, potom λx.t je výraz (abstrakce)
• pokud t a s jsou výrazy, pak i ts je výraz (aplikace)
1
Proměnná je ve výrazu volná v těchto případech:
• proměnná x je volná ve výrazu x
• proměnná x je volná v λy.t, pokud x ̸= y a x je volná v t
• proměnná x je volná v st, pokud je volná v s nebo t
Proměnná je ve výrazu vázaná v těchto případech:
• proměnná x je vázaná v λy.t, pokud x = y nebo x je vázaná v t
• proměnná x je vázaná v st, pokud je vázaná v s nebo t
Na názvech proměnných nezáleží, tedy λx.x ≡ λy.y. Takovému přejmenování se říká α-konverze
a využívá se pro předcházení jmenným konfliktů.
Nahrazení vázané proměnné argumentem se nazývá β-redukce a dá se chápat jako výpočetní krok.
Např. (λx.ax)y ≡ ay
Pokud f neobsahuje x jako volnou proměnnou, platí λx.fx ≡ f. Tomuto se říká η-redukce
Typovaný λ-kalkul je rozšíření λ-kalkulu, ve kterém má každý výraz svůj typ. Zaveďme si
množiny typových symbolů S = {S1, S2, ...}, potom definujeme typ takto:
• Symbol Si je typ.
• Pokud T1 a T2 jsou typy, pak i T1 → T2 je typ.
Pokud je t výraz, potom pro označení, že jeho typ je T píšeme t : T.
• c : T označuje konstantu typu T
• pro každý typ T existuje spočetně mnoho proměnných x1 : T, x2 : T, ...
• Pokud t : T1 → T2 a s : T1 potom ts : T2
• Pro proměnnou x : T1 a výraz t : T2 platí λx.t : T1 → T2
• Existuje singleton typ 1 s výrazem ∗ : 1. Libovolný další výraz tohoto typu je ekvivalentní s
∗.
Daný typovaný λ-kalkul L můžeme chápat jako kategorii C(L), kde:
• Objekty jsou typy T
• morfismy A → B jsou třídy ekvivalentních uzavřených výrazů [c] : A → B
• identity jsou idT = λx.x (kde x je typu T)
• skládání: c ◦ b = λx.c(bx)
2