Curry-Howardova korešpondencia

Základné pojmy

V tejto kapitole sa budeme venovať jednému z najdôležitejších prepojení medzi matematickou logikou a programovaním – Curry–Howardovej korešpondencii. Ide o prekvapivo jednoduchú, no mimoriadne hlbokú myšlienku:

Logické výroky sú typy a dôkazy sú programy.

V prvej časti budú predstavené základné pojmy intuicionistickej logiky, prirodzenej dedukcie a spôsob, akým sa dôkazy konštruujú v dedukčných systémoch. Následne uvidíme, že rovnaké štruktúry, ktoré sa používajú na tvorbu logických dôkazov, môžu byť interpretované ako typy a programy v jednoducho typovanom λ-kalkule.

Táto kapitola bude rozdelená do troch hlavných blokov:

1. Intuicionistická logika a prirodzená dedukcia
   – predstavíme syntax, sémantiku a dedukčný kalkul, čo bude tvoriť “logickú” stranu korešpondencie.

2. Curry–Howardova korešpondencia
   – ukážeme, ako logické spojky zodpovedajú typovým konštruktorom, ako dôkazy zodpovedajú termom, a ako odvodzovacie pravidlá dedukčného kalkulu zodpovedajú typovacím pravidlám.

3. Hľadanie termu typu (type inhabitation)
   – predstavíme spôsob generovania dôkazov/programov z logických špecifikácií a príklady, ktoré ilustrujú, ako sa konštruktívne dôkazy premietajú do programov.

Cieľom tejto prednášky je nielen vysvetliť formálnu korešpondenciu medzi dvoma odlišnými svetmi — logikou a programovaním — ale ukázať aj to, prečo ide o základný koncept v návrhu typových systémov, verifikácii programov a automatických či interaktívnych dokazovacích systémoch.

Curry–Howardova korešpondencia

Curry–Howardova korešpondencia (niekedy nazývaná aj Curry–Howardov izomorfizmus) je základný koncept v informatike a matematickej logike, ktorý opisuje hlbokú súvislosť medzi logickými systémami a teóriami typov. Definuje, že výroky v logike zodpovedajú typom v teórii typov, a dôkazy týchto výrokov zodpovedajú programom, ktoré majú daný typ.

Inými slovami:

Takýto pohľad umožňuje interpretovať programy ako konštruktívne dôkazy a typy ako výroky, ktoré tieto programy dokazujú. Správne typovaný program vo funkcionálnom jazyku je teda konštruktívnym dôkazom výroku korešpondujúceho s jeho typom.

Vo všeobecnosti ide o korešpondenciu medzi konkrétnou intuicionistickou logikou a vhodne zvolenou teóriou typov. V našom prístupe sa budeme zaoberať korešpondenciou medzi intuicionistickou výrokovou logikou a jednoducho typovaným λ-kalkulom.

Typová kontrola, Odvodenie typu, Nájdenie termu typu

Pri práci s teóriou typov (a teda aj v rámci Curry–Howardovej korešpondencie) rozlišujeme tri kľúčové problémy:

1. Type checking (kontrola typov)
   Má daný term t typ T?
   Formálne: overujeme, či platí Γ ⊢ t : T.

2. Type inference (odvodenie typov)
   Aký typ má term t?
   Formálne: hľadáme typ T taký, že Γ ⊢ t : ?.

3. Type inhabitation (hľadanie termu)
   Existuje term t taký, že má typ T?
   Inými slovami: má typ T (logický výrok) term (dôkaz)?
   Formálne: hľadáme term t taký, že Γ ⊢ ? : T.

Doteraz sme sa venovali predovšetkým prvým dvom problémom:

• kontrole typov (type checking),
• a odvodeniu typov (type inference).

V tejto kapitole sa však sústredíme na tretí problém — nájdenie termu typu (type inhabitation).
Ten je v kontexte Curry–Howardovej korešpondencie kľúčový, pretože:

• term typu $T$ zodpovedá dôkazu korešpondujúceho výroku $\varphi$,
• teda hľadať program typu T znamená hľadať konštruktívny dôkaz korešpondujúceho výroku $\varphi$.

Intuicionistická logika

Intuicionistická logika (nazývaná aj konštruktívna logika), môže byť stručne opísaná ako klasická logika bez:

• Aristotelovho pravidla vylúčenia tretieho: $$φ \lor \neg φ,$$
• zákonu dvojitej negácie $$¬¬φ ≡ φ.$$

Intuicionizmus je filozofický a matematický prístup, ktorý sa zameriava na konštruktívny postup v matematike a tvrdí, že matematické objekty musia byť skutočne skonštruované, nie iba abstraktne definované. Intuicionisti odmietajú princípy klasického deduktívneho dôkazu, ktorý sa vychádza zo zákona vylúčenia tretieho, ktorý hovorí, že ak existuje nejaký výrok, tak je buď pravdivý alebo nepravdivý.

Konštruktívny dôkaz je druh matematického dôkazu, ktorý dokazuje existenciu matematického objektu tým, že ukáže spôsob, ako tento objekt skutočne skonštruovať. Tento prístup k matematickému dôkazu sa líši od tradičného dôkazu, ktorý iba dokazuje existenciu objektu bez skutočnej konštrukcie.

Formálny dôkaz je konečná postupnosť viet (v prípade logiky sú to formuly), z ktorých každá je axiómou, predpokladom alebo je odvodená z predchádzajúcich viet pomocou dedukčného pravidla. Od idiomatického dôkazu pomocou prirodzeného jazyka sa formálny dôkaz líši tým, že je rigorózny, jednoznačný a mechanicky overiteľný.

Jazyk intuicionistickej logiky

Jazyk intuicionistickej logiky je rovnaký ako jazyk klasickej logiky, avšak logické spojky intuicionistickej logiky nie sú definované rovnakým spôsobom ako v klasickej logike.

Syntax výrokovej intuicionistickej logiky v BNF

Je definovaná produkčným pravidlom v Backus-Naurovej forme, prostredníctvom ktorého je možné konštruovať všetky prípustné tvary formúl: $$ \varphi ::= p \mid \top \mid \bot \mid \neg\varphi \mid \varphi \land \psi \mid \varphi \lor \psi \mid \varphi \Rightarrow \psi, $$ kde p je množina atomických výrokov. Platí rovnaká priorita a asociativita operátorov ako v klasickej výrokovej logike.

Priorita a asociativita

Vlastnosti syntaxe intuicionistickej logiky

Žiadnu zo základných logických spojok nemožno vyjadriť pomocou ostatných a preto je nutná prítomnosť všetkých štyroch.

• Negácia ($\neg$) je definovaná ako implikácia do absurda $\neg φ ≡ φ ⇒ ⊥$.
• Vérum ($\top$) je definované ako $\bot \Rightarrow \bot$.
• Ekvivalencia ($\Leftrightarrow$) nie je považovaná za základnú spojku, ale rovnako ako v klasickej výrokovej logike za konjunkciu dvoch implikácií.

Mnoho tautológii klasickej logiky neplatí v intuicionistickej logike. To zahŕňa nielen zákon vylúčenia tretieho či eliminácie dvojitej negácie, ale tiež Peirceové pravidlo $(((φ \Rightarrow ψ) \Rightarrow φ) \Rightarrow φ)$. Pretože nie všetky tautológie klasickej logiky sú teorémy intuicionistickej logiky, ale všetky teorémy intuicionistickej logiky platia v klasickej logike, je možné sa na intuicionistickú logiku pozerať ako na oslabenie klasickej logiky, avšak s mnohými užitočnými vlastnosťami.

Sémantika intuicionistickej logiky

Keďže intuicionistická logika neakceptuje niektoré klasické zákony (napríklad zákon vylúčenia tretieho, či princíp dôkazu sporom), jej sémantika nie je viazaná výhradne na klasické pravdivostné hodnoty. Umožňuje rôzne interpretácie, ktoré zachytávajú jej konštruktívny charakter.

Definícia: Tautologický dôsledok

Nech $\Gamma$ je množina formúl (predpokladov) a $\varphi$ je formula.
Potom zápis: $$ \Gamma \models \varphi $$ znamená, že φ je tautologickým dôsledkom množiny predpokladov Γ, t.j. že $\varphi$ platí vo všetkých modeloch, v ktorých platia všetky formuly z $\Gamma$.

Brouwer–Heyting–Kolmogorova (BHK) interpretácia

BHK interpretácia poskytuje neformálnu konštruktívnu sémantiku. Namiesto klasických pravdivostných hodnôt opisuje význam logických spojok pomocou konštruktívnych dôkazov.

Intuitívne:

Význam formuly je daný tým, čo znamená mať jej konštruktívny dôkaz.

BHK podmienky:

• Konjunkcia (φ ∧ ψ)
  Konštruktívny dôkaz pozostáva z dôkazu φ a dôkazu ψ.

• Disjunkcia (φ ∨ ψ)
  Konštruktívny dôkaz pozostáva buď z dôkazu φ, alebo dôkazu ψ, spolu s informáciou, ktorá vetva bola zvolená.

• Implikácia (φ ⇒ ψ)
  Dôkaz je funkcia, ktorá každý dôkaz φ prevedie na dôkaz ψ.

• Negácia (¬φ)
  Definovaná ako φ ⇒ ⊥. Dôkaz je konštrukcia, ktorá každý dôkaz φ prevedie na absurdum ⊥.

• Absurdum (⊥)
  Nemá žiadny konštruktívny dôkaz.

• Vérum (⊤)
  Má triviálny konštruktívny dôkaz.

Intuitívna interpretácia v štýle „programovanie ako dôkaz“

Formuly môžeme predstaviť ako úlohy/problémy, a dôkazy ako metódy/programy, ktoré ich riešia:

• φ, ψ, θ, … → úlohy/problémy
• a, b, c, … → dôkazy/metódy/programy

Interpretácia základných logických spojok:

• Konjunkcia
  Dôkaz φ ∧ ψ je dvojica ⟨a, b⟩, kde a rieši φ a b rieši ψ.

• Disjunkcia
  Dôkaz φ ∨ ψ je označený variant:

  • ⟨a, b⟩.1 – dôkaz φ (ľavá vetva)
  • ⟨a, b⟩.2 – dôkaz ψ (pravá vetva)

• Implikácia
  Dôkaz φ ⇒ ψ je funkcia f, ktorá z každého dôkazu a formuly φ vytvorí dôkaz f(a) formuly ψ.

BHK interpretácia tvorí konceptuálny most medzi intuicionistickou logikou a konštruktívnym programovaním. Je priamym predchodcom Curry–Howardovej korešpondencie, kde sa konštruktívne dôkazy korešpondujú s programami a logické formuly s typmi.

Prirodzená dedukcia

Je to dedukčný kalkul (niekedy nazývaný aj dôkazový systém) prostredníctvom ktorého je možné dokazovať pravdivosť formúl. Prirodzenú dedukciu predstavil Gerhard Gentzen. Pre intuicionistickú logiku sa používa systém NJ, pre klasickú logiku existuje systém NK.

Prirodzená dedukcia umožňuje zapisovať dôkazy tak, aby každý krok odvodzoval ďalšie formuly logicky priamo z predpokladov, teda spôsobom „prirodzeným“ pre ľudské uvažovanie.

Prirodzená dedukcia pre intuicionistickú logiku (NJ) sa dá definovať ako dedukčný kalkul klasickej logiky (NK) bez pravidla sporu.

Definícia: Sekvent

V dedukčných kalkuloch logických systémov sa formuly najčastejšie zapisujú v tvare sekventu: $$ \Gamma \vdash \varphi $$ kde:

• $\Gamma$ je kontext - množina predpokladov (premís) v tvare: $\varphi_1, ..., \varphi_n$,
• $\varphi$ je formula (cieľ), ktorú chceme dokázať.

Sekvent teda vyjadruje, že z množiny predpokladov $\Gamma$ možno dokázať formulu $\varphi$ pomocou príslušného dedukčného systému.

Vlastnosti prirodzenej dedukcie:

Konzistentnosť a úplnosť dedukčného kalkulu (Soundness and Completeness)

• Konzistentnosť voči sémantike logického systému. Ak v dedukčnom kalkule je formula $\varphi$ dokázateľná z množiny predpokladov $Γ$, potom formula $φ$ vyplýva z množiny predpokladov $Γ$ vzhľadom na definovanú sémantiku daného logického systému: $$\text{ak} \quad Γ \vdash φ, \quad \text{potom}~ \quad Γ \models φ.$$
• Úplnosť voči dedukčnému kalkulu logického systému. Ak formula $φ$ vyplýva z množiny predpokladov $Γ$ vzhľadom na definovanú sémantiku daného logického systému, potom v dedukčnom kalkule je formula $\varphi$ dokázateľná z množiny predpokladov $Γ$. $$\text{ak} \quad Γ \models φ, \quad \text{potom}~ \quad Γ \vdash φ.$$
• Dedukčný kalkul je konzistentný a úplný (silná forma vety) ak platí: $$Γ \models φ \quad \text{vtt.}~ \quad Γ \vdash φ.$$

Inými slovami a zjednodušene, ak je formula tautológia vzhľadom na definíciu sémantiky v danom logickom systéme, potom musí byť aj dokázateľná v jeho dedukčnom kalkule a vice versa. To hovorí slabá veta forma vety konzistentnosti a úplnosti dedukčného kalkulu: $$\models φ \quad \text{vtt.}~ \quad \vdash φ.$$

Axiómy
      ↓↓↓
Dedukčné pravidlá aplikované na axiómy
      ↓↓↓
Dokázateľné formuly   
      ↓↓↓
Dedukčné pravidlá aplikované na dokázateľné formuly 
      ↓↓↓
Nové dokázateľné formuly   
      ↓↓↓
... a pod. ...

Dedukčný kalkul prirodzenej dedukcie

Dedukčný kalkul pozostáva zo sady odvodzovacích (dedukčných) pravidiel, ktoré určujú, ako možno odvodiť nové formuly zo zadaných predpokladov.

Každé odvodzovacie pravidlo má tvar:

kde horná časť pravidla obsahuje nula až $n$ predpokladov a dolná časť je formula (záver) odvodená týmto pravidlom.

Typy odvodzovacích pravidiel v prirodzenej dedukcii

Odvodzovacie pravidlá v prirodzenej dedukcii môžeme kategorizovať nasledovne:

• Pravidlá zavádzajúce (Introduction, I): Opisujú, ako získať novú formulu s danou logickou spojkou.

• Pravidlá eliminujúce (Elimination, E): Umožňujú využiť existujúcu formulu na odvodenie ďalších logických záverov.

• Axiómy: pravidlá bez predpokladov, ktoré ukončujú vetvy dôkazu.

Táto štruktúra je základom prirodzenej dedukcie a slúži ako rámec pre formálne odvodzovanie v intuicionistickej aj klasickej logike.

Dôkaz formuly prirodzenou dedukciou

Dôkazom sekventu $\Gamma \vdash \varphi$ je dôkazový strom, ktorý je zostrojený následovným spôsobom:

• V koreni stromu sa nachádza dokazovaný sekvent $\Gamma \vdash \varphi$.
• Každý uzol stromu vznikol aplikáciou jedného odvodzovacieho pravidla.
• Všetky listy stromu sú axiómy.

Zjednodušene:

Dôkaz konštruujeme od konca, t.j. od dokazovaného výroku, aplikáciou príslušných odvodzovacích pravidiel, pokiaľ všetky listy stromu niesu axiómy.

Odvodzovacie pravidlá

Axióma:

Dedukčné pravidlá systému NJ:

Pravidlo sporu (platí v klasickej logike, neplatí v intuicionistickej logike)

Curry–Howardová korešpondencia medzi jednoducho typovaným $λ$-kalkulom a výrokovou intuicionistickou logikou

V 1943 Haskell Curry spozoroval korešpondenciu medzi intuicionistickym logickým systémom a teóriou typov, ktorú neskôr znovuobjavil William Howard v 1969 a publikoval v 1980.

Korešpondencia definuje presný vzťah medzi jednoducho typovaným $λ$-kalkulom a intuicionistickou logikou:

• Výrok $φ$ považujeme za typ.
• Dôkaz výroku $φ$ je term typu $T$.
• Dokazovanie formuly prirodzenou dedukciou korešponduje s typovou kontrolou.
• Zjednodušenie dôkazov korešponduje s vyhodnocovaním termu.

Korešpondencia typovacích pravidiel $\lambda_\rightarrow$ a odvodzovacích pravidiel Systému NJ

Typovacie pravidlá korešpondujú s dedukčnými pravidlami systému NJ.

Motivačný príklad: Extrakcia programu z dôkazu

Ako prvý motivačný príklad uvedieme jednoduchý program Swap. Na vstupe dostane dvojicu a na výstupe vráti tú istú dvojicu, avšak v obrátenom poradí.

Intuitívne typ takéhoto programu bude: $$A \times B \to B \times A,$$ čo korešponduje s intuicionistickou formulou: $$B∧A ⇒ A∧B.$$

Dôkaz formuly $B∧A ⇒ A∧B$ prirodzenou dedukciou je možné skonštruovať nasledovne:

Z vyššie uvedeného dôkazu môžeme priamo prečítať aj príslušný program. Každý krok dôkazu zodpovedá určitej konštrukcii v λ-kalkule:

• Záverečný krok → zavedenie λ-abstrakcie
• Eliminácie konjunkcie → projekcie z.1, z.2
• Zavedenie konjunkcie → konštrukcia dvojice <_, _>

V dôkaze sa nachádza hypotéza v kontexte, ktorú označíme premennou $$z : B ∧ A,$$ čo v λ-kalkule zodpovedá výrazu typu $$z : B × A.$$

Následne v dôkazovom strome používame pravidlá ∧E₁ a ∧E₂, ktoré nám umožnia získať jednotlivé zložky dvojice.
V λ-kalkule sa tieto kroky prejavia ako projekcie:

• z pravidla ∧E₁ získame prvú zložku: z.1 : B
• z pravidla ∧E₂ získame druhú zložku: z.2 : A

Potom aplikujeme pravidlo ∧I, ktoré v konštrukcii programu znamená, že z oboch výsledkov vytvoríme novú dvojicu:

$$⟨ z.2 , z.1 ⟩ : A × B$$

Nakoniec posledný krok dôkazu využíva pravidlo implikácie ⇒I, ktoré sa v λ-kalkule prejaví ako zavedenie λ-abstrakcie:

$$λz : B × A. ⟨ z.2 , z.1 ⟩: A \times B \to A × B $$

Typová kontrola termu:

Motivačný príklad: Extrakcia dôkazu z programu

V predchádzajúcom príklade bolo demonštrované, ako je možné z dôkazu v prirodzenej dedukcii extrahovať príslušný program v λ-kalkule.

Tento príklad je zameraný na opačný smer: z typu programu odvodíme jeho korešpondujúcu logickú formulu a následne sformulujeme aj jej dôkaz na základe príslušného termu daného typu.

Uvažujme nasledujúci funkčný typ:

$$ A + B \;\to\; (A \to C) \;\to\; (B \to C) \;\to\; C $$

Tento typ korešponduje s nasledujúcou intuicionistickou formulou:

$$ A \lor B \;\Rightarrow\; (A \Rightarrow C) \;\Rightarrow\; (B \Rightarrow C) \;\Rightarrow\; C. $$

Intuitívne ide o klasickú konštrukciu case-analysis:
ak máme dôkaz disjunkcie $A \lor B$, tak:

• ak platí $A$, môžeme použiť dôkaz $A \Rightarrow C$,
• ak platí $B$, môžeme použiť dôkaz $B \Rightarrow C$.

V oboch prípadoch získame dôkaz $C$.

Z programu vidíme dôkaz.

Pri pohľade na typové a dedukčné pravidlá, je možné pozorovať nasledujúcu korešpondenciu:

• zavedenie implikácie → λ-abstrakcia,
• eliminácia disjunkcie → case … of,
• eliminácia implikácie → aplikácia funkcie.

Korešpondujúci program je:

$$ \begin{array}{l} λx : A + B.\; λf : A \to C.\; λg : B \to C.\; \\ \qquad \text{case } x \text{ of } \\ \qquad \qquad \ \ \ \text{inl } a \Rightarrow f\; a \\ \qquad \qquad \mid\mid \text{inr } b \Rightarrow g\; b \\ : A + B \;\to\; (A \to C) \;\to\; (B \to C) \;\to\; C \end{array} $$

Typová kontrola daného termu:

Dôkaz formuly
$$ A \lor B \;\Rightarrow\; (A \Rightarrow C) \;\Rightarrow\; (B \Rightarrow C) \;\Rightarrow\; C $$
prirodzenou dedukciou na základe stromu typovej kontroly je možné zostaviť nasledovne:

Záver

Jedným z najvýznamnejších objavov informatiky minulého storočia je Curry–Howardova korešpondencia, ktorá odhaľuje hlboké prepojenie medzi logikou a programovaním. Tento koncept ukazuje, že každý konštruktívny dôkaz logického výroku môže byť interpretovaný ako program, a naopak, každý správne typovaný program predstavuje dôkaz výroku. Táto idea je základom moderných typových systémov a interaktívnych dokazovacích systémov (kde patrí aj systém Rocq).

• Dôkaz formuly konštruuje funkciu daného typu – každý konštruktívny dôkaz korešponduje s konkrétnym termom v jednoducho typovanom λ-kalkule.
• Rozhodnuteľnosť typovej kontroly – overenie, či je daný λ-term správne typovaný, je algoritmicky rozhodnuteľné a deterministické.
• Hľadanie dôkazu (type inhabitation) – existencia termu daného typu, resp. dôkazu pre daný výrok, je vo všeobecnosti nerozhodnuteľný problém.
• Funkcia dôkazu tvrdenia – typová kontrola funguje ako algoritmus, ktorý overuje, či je tvrdenie dokázateľné, a ukazuje spôsob, ako môže byť dôkaz (program) konštruovaný.
• Význam intuicionistickej logiky – konštruktívny prístup k dôkazom, odmietanie zákona vylúčenia tretieho a dvojitej negácie, dôraz na explicitnú konštrukciu matematických objektov (programov).
• Korešpondencia typovacích a dedukčných pravidiel – každý λ-term a jeho typ zodpovedá konkrétnemu dôkazu a odvodzovaciemu pravidlu v prirodzenej dedukcii.
• Redukcia dôkazu = β-redukcia programu – zjednodušenie dôkazu zodpovedá zjednodušeniu programu, čo ukazuje presnú korešpondenciu medzi logikou a λ-kalkulom.
• Kontrast dôkazov a typovania – dôkazy môžu mať nekonečne veľa variantov, zatiaľ čo typová kontrola je jednoznačná a deterministická.
• Praktický význam – základy pre typové systémy, verifikáciu programov, interaktívne a automatické dokazovanie, generovanie programov zo špecifikácií.

Kľúčová myšlienka:

Každý správne typovaný program je konštruktívnym dôkazom výroku, čo umožňuje premostiť svet matematickej logiky a funkcionálneho programovania.

Korešpondencie medzi typovými systémami a logikami

Zdroje

1. Pierce, Benjamin C. Types and programming languages. MIT press, Cambridge, 2001 (Перевод на русский язык: Бенджамин Пирс. Типы в языках программирования. — Добросвет, 2012. — ISBN 978-5-7913-0082-9)
2. Sørensen, M. H., Urzyczyn, P., Lectures on the Curry-Howard isomorphism (Vol. 149). Elsevier. 2006
3. Wadler, P., Propositions as types. Communications of the ACM, 58 (12), 75-84. 2015
4. Open Logic Project, 2025
5. OCaml Programming: Correct + Efficient + Beautiful: Lecture notes, Cornell University, 2025
6. Брагилевский, В. Н. Соответствие Карри–Ховарда: от математической логики к программированию, Летняя школа «Современная математика», посвященная памяти Виталия Арнольда, 2017
7. Брагилевский, В. Н. Соответствие Карри—Ховарда: от математической логики к программированию и обратно, Записи лекций на XVII Летней школе «Современная математика», 2017
8. Крупский, В.Н., Кузнецов, С.Л., Практикум по математической логике. COQ. МГУ имени М.В. Ломоносова, 2013