Pure type system

In the branches of

The systems from the lambda cube are all known to be

A pure type system is defined by a triple ${\textstyle ({\mathcal {S}},{\mathcal {A}},{\mathcal {R}})}$ where ${\textstyle {\mathcal {S}}}$ is the set of sorts, ${\textstyle {\mathcal {A}}\subseteq {\mathcal {S}}^{2}}$ is the set of axioms, and ${\textstyle {\mathcal {R}}\subseteq {\mathcal {S}}^{3}}$ is the set of rules. Typing in pure type systems is determined by the following rules, where ${\textstyle s}$ is any sort:^[4]

${\displaystyle {\frac {(s_{1},s_{2})\in {\mathcal {A}}}{\vdash s_{1}:s_{2}}}\quad {\text{(axiom)}}}$

${\displaystyle {\frac {\Gamma \vdash A:s\quad x\notin {\text{dom}}(\Gamma )}{\Gamma ,x:A\vdash x:A}}\quad {\text{(start)}}}$

${\displaystyle {\frac {\Gamma \vdash A:B\quad \Gamma \vdash C:s\quad x\notin {\text{dom}}(\Gamma )}{\Gamma ,x:C\vdash A:B}}\quad {\text{(weakening)}}}$

${\displaystyle {\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash B:s_{2}\quad (s_{1},s_{2},s_{3})\in {\mathcal {R}}}{\Gamma \vdash \Pi x:A.B:s_{3}}}\quad {\text{(product)}}}$

${\displaystyle {\frac {\Gamma \vdash C:\Pi x:A.B\quad \Gamma \vdash a:A}{\Gamma \vdash Ca:B[x:=a]}}\quad {\text{(application)}}}$

${\displaystyle {\frac {\Gamma ,x:A\vdash b:B\quad \Gamma \vdash \Pi x:A.B:s}{\Gamma \vdash \lambda x:A.b:\Pi x:A.B}}\quad {\text{(abstraction)}}}$

${\displaystyle {\frac {\Gamma \vdash A:B\quad B=_{\beta }B'\quad \Gamma \vdash B':s}{\Gamma \vdash A:B'}}\quad {\text{(conversion)}}}$

Implementations

The following programming languages have pure type systems:^{[citation needed]}

• SAGE ^[11]
• Yarrow ^[12]
• Henk 2000 ^[13]

See also

• System U – an example of an inconsistent PTS
• λμ-calculus uses a different approach to control than CPTS

Notes