Pure type system

A pure type system is defined by a triple (\mathcal{S}, \mathcal{A}, \mathcal{R}) where \mathcal{S} is the set of sorts, \mathcal{A} \subseteq \mathcal{S}^2 is the set of axioms, and \mathcal{R} \subseteq \mathcal{S}^3 is the set of rules. Typing in pure type systems is determined by the following rules, where s is any sort: \frac{(s_1, s_2) \in \mathcal{A}}{\vdash s_1 : s_2}\quad \text{(axiom)} \frac{\Gamma \vdash A : s \quad x \notin \text{dom}(\Gamma)}{\Gamma, x : A \vdash x : A }\quad \text{(start)} \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)} \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)} \frac{\Gamma \vdash C : \Pi x : A. B \quad \Gamma \vdash a : A}{\Gamma \vdash Ca : B[x := a]}\quad\text{(application)} \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)} \frac{\Gamma \vdash A : B \quad B =_{\beta} B' \quad \Gamma \vdash B' : s}{\Gamma \vdash A : B'}\quad\text{(conversion)} == Implementations ==