Redigerer Typeteori (avsnitt)

== Barendregts lambda-kube ==
[[File:Lambda cube.png|thumb|Lambda cube]]
Matematikeren [[Henk Barendregt]] utviklet lambda-kuben, <math>\lambda</math>-kuben, for å utforske forskjellige utvidelser av typesystemer.
Han tar utgangspunkt i <math>\lambda^\to</math>, og ser på tre utvidelser, som vises som akser i kuben:

# Typeoperatorer — typer som er avhenger av typer, z-aksen
# Polymorphisme — termer som avhenger av typer, y-aksen
# ''Dependent'' typer — typer som avhenger av termer, x-aksen

Disse utvidelsene gir opphav til åtte forskjellige typesystemer, avhengig av hvilke utvidelser man tar med. Lambda-kuben gir et 
rammeverk som definerer alle åtte systemene samtidig, men det er også mulig å definere hvert system for seg selv.
Hvis man ikke tar med noen av utvidelsene så får man <math>\lambda^\to</math> som beskrevet over, 
og tar man med alle, får man noe som tilsvarer [[Calculus of Constructions]].

=== Definisjon av lambda kuben ===
Det er ikke lenger praktisk å ha to seperate syntaktiske kategorier for termer og typer, og i <math>\lambda</math>-kuben definerer man derfor pseudo-termer som
:<math> \mathcal{T} ::= x \mid C \mid \mathcal{T}_1\, \mathcal{T}_2 \mid \lambda x : \mathcal{T}_1 . \mathcal{T}_2 \mid \Pi x : \mathcal{T}_1 . \mathcal{T}_2</math>
hvor <math>C</math> er en mengde konstanter, som minst inneholder <math>*</math> (les: type) og <math>\Box</math> (les: 'kind').

==== Felles regler ====
Alle systemene har noen regler til felles.
{| align="center" cellpadding="9"
| align="left" | <math>{ \mathrm{} \over \cdot \vdash * : \Box }</math> (ax) En type er en kind.
|-
| align="left" | <math>{ \Gamma \vdash N : A \over \Gamma, x : B \vdash N : A }</math> (wk) Man kan legge til variabler.
|-
| align="left" | <math>{ \mathrm{} \over \Gamma, x : A \vdash x : A }</math> (var) 
|- 
| align="left" | <math>{ \Gamma \vdash N : \Pi x : A . B \quad \Gamma \vdash M : A \over \Gamma \vdash N \, M : B[M/x] }</math> (app) 
|- 
| align="left" | <math>{ \Gamma, x : A \vdash N : B \over \Gamma \vdash \lambda x : A . N : \Pi x : A . B }</math> (abs)
|-
| align="left" | <math>{ \Gamma \vdash N : A \quad A =_\beta A' \over \Gamma \vdash N : A' }</math> (conv)
|}

==== Parametriske regler ====
Følgende regel er parametrisk i <math> s_1, s_2 \in \{ *, \Box \}</math>. 

:<math>\Gamma \vdash A : s_1 \quad \Gamma, x : A \vdash B : s_2 \over \Gamma \vdash \Pi x:A.B : s_2 </math>

Man kan bestemme hvilket typesystem man ønsker ved å bestemme hvilke instanser av <math>(s_1, s_2)</math> man som er godtatt. Tabellen under lister opp alle mulighetene.
{| class="wikitable"
|-
!  !! ''Dependent'' typer !! Polymorfi !! Typeoperatorer !! Forkortelse !! Navn
|-
| <math>(*, *)</math> ||  ||  ||  || <math>\lambda^\to</math> || ''Simply typed lambda calculus''
|-
| <math>(*, *)</math> ||  ||  || <math>(\Box, \Box)</math> || <math>\lambda\underline\omega</math> || 
|-
| <math>(*, *)</math> ||  || <math>(\Box, *)</math> ||  || <math>\lambda 2</math> || ''System F''
|-
| <math>(*, *)</math> ||  || <math>(\Box, *)</math> || <math>(\Box, \Box)</math> || <math>\lambda\omega</math> || ''System F<math>\omega</math>''
|-
| <math>(*, *)</math> || <math>(*, \Box)</math> ||  ||  || <math>\lambda P</math> || LF (''Logical Framework'')
|-
| <math>(*, *)</math> || <math>(*, \Box)</math> ||  || <math>(\Box, \Box)</math> || <math>\lambda P \underline\omega</math> ||
|-
| <math>(*, *)</math> || <math>(*, \Box)</math> || <math>(\Box, *)</math> || || <math>\lambda P 2</math> || 
|-
| <math>(*, *)</math> || <math>(*, \Box)</math> || <math>(\Box, *)</math> || <math>(\Box, \Box)</math> || Coc, <math>\lambda C</math>, <math>\lambda P\omega</math> || ''Calculus of Construction''
|}