type theory

type theory (tsz. type theories)

1. (informatika) Típuselmélet (Type Theory) a matematikai logika és a számítástudomány találkozási pontján álló formális rendszer, amelyben a „típusok” szolgálnak az adatok és kifejezések osztályozására, valamint a fogalmak precíz specifikációjára és bizonyítására.

• Biztonságos programozás: a típusok garantálják, hogy csak értelmes műveleteket alkalmazzunk (pl. nem adunk össze számok és karakterláncok között).
• Formális bizonyítás: a típuselméletben a tételek és bizonyítások programként élnek, a Curry–Howard-korrespondencia szerint a bizonyítás egy program, típusa pedig a tétel.
• Kifejező nyelvek: a dependens típusok lehetővé teszik, hogy a típus önmagában kifejezze a program specifikációját (pl. „ez a tömb pont ${\textstyle n}$ elemű”).

1. Egyszerű típusos lambda‐kalkulus (Simply Typed λ-Calculus)

   • Vannak alap­típusok (például Bool, Int), és típusösszetételek: függvénytípus ${\textstyle A\to B}$.
   • A kifejezések (lambda‐kifejezések) csak akkor értelmezettek, ha a típusuk kiterjeszthető a kezdeti szabályokkal.

2. Típusellenőrzés

   • Egy kifejezéshez (λx.e) hozzárendelünk egy kontextusban (x:A) típusokat, és szabályokkal eldöntjük, hogy ${\textstyle e}$ milyen típusú.

   • Példa:

     $${\displaystyle {\frac {\Gamma ,\,x:A\vdash e:B}{\Gamma \vdash (\lambda x.e):A\to B}}\quad {\frac {\Gamma \vdash f:A\to B\quad \Gamma \vdash a:A}{\Gamma \vdash f\,a:B}}}$$

• Dependens típus: egy típus magában hordozhat értékváltozókat, például

  $${\displaystyle {\mathsf {Vec}}(A,n)}$$

  a „${\textstyle A}$-típusú listák pontosan ${\textstyle n}$ hosszú” típusát jelöli.

• Előny: a függvények típusában leírhatjuk az invariánsokat, pl.

  $${\displaystyle {\mathsf {head}}:\forall A.\;\forall n>0.\;{\mathsf {Vec}}(A,n)\to A,}$$

  itt a függvény csak nem‐üres listákra alkalmazható.

• Propozíció ↔ típus: minden logikai állításhoz tartozik egy típus.
• Bizonyítás ↔ program: egy konstrukciós bizonyítás egyben program is, melynek típusa maga a propozíció.
• Példák:
  • „${\textstyle A\land B}$” propozíció ↔ páros típus ${\textstyle (A,B)}$.
  • „${\textstyle A\to B}$” ↔ függvénytípus ${\textstyle A\to B}$.
  • „${\textstyle A\lor B}$” ↔ szumma‐típus ${\textstyle {\mathsf {Either}}\;A\;B}$.

1. Martin-Löf típuselmélet – Alapja a konstruktív logikának, dependens típusokat és induktív típusokat tartalmaz.
2. Coq – Tételbizonyító asszisztens és programozási nyelv, mely Gallina nyelvre épül (dependens tipizálás, taktikák).
3. Agda – Dependens típusú programozási nyelv, interaktív bizonyításra és programírásra.
4. Idris – Praktikus dependens típusos nyelv, erős típusellenőrzéssel.
5. Lean – Tételbizonyító rendszer, könyvtárakkal matematikai formalizálásokhoz.

• Formal verification: szoftverek és hardverek formális biztonsági vagy helyességi tulajdonságainak ellenőrzése.
• Biztonságos API‐k: típusokkal kódolt API‐biztonság, pl. HTTP-kérések formátuma, kriptográfiai invariánsok garantálása.
• Matematikai formalizálás: tételbizonyítás és könyvtárak építése (elemző geometriától a halmazelméletig).

A típuselmélet egységes keretet ad a programok és bizonyítások formális kezelésére, a dependens típusok lehetővé teszik a specifikációk és invariánsok közvetlen beágyazását a kódba, a Curry–Howard‐korrespondencia pedig összekapcsolja a logikát és a programozást. A modern tételbizonyító rendszerek és erős típusos nyelvek a kutatói és ipari területeken egyaránt egyre nagyobb szerepet játszanak.

• type theory - Szótár.net (en-hu)
• type theory - Sztaki (en-hu)
• type theory - Merriam–Webster
• type theory - Cambridge
• type theory - WordNet
• type theory - Яндекс (en-ru)
• type theory - Google (en-hu)
• type theory - Wikidata
• type theory - Wikipédia (angol)