Pure Type System

A pure type system is a typed lambda calculus specified by a set of sorts , an axiom relation , and a dependent-product relation . Its expressions include variables, sorts, applications, annotated abstractions , and dependent products . The axiom relation specifies which sorts classify other sorts, while the product relation specifies admissible domain, codomain, and resulting sorts. Relations need not be functional.

A legal expression is either the subject or expected type of a derivable judgment in a valid finite context. Full beta reduction includes the rule

The substitution avoids capture, and reductions may also act within abstraction annotations and either component of a dependent product. Weak normalization means that every legal expression in every valid context has some terminating beta-reduction sequence. Strong normalization means that every beta-reduction sequence from every such expression is finite.