Subject reduction

In type theory, a type system has the property of subject reduction (also subject evaluation, type preservation or simply preservation) if evaluation of expressions does not cause their type to change. Formally, if Γ ⊢ e1 : τ and e1e2 then Γ ⊢ e2 : τ.

Together with progress, it is an important meta-theoretical property for establishing type soundness of a type system.

The opposite property, if Γ ⊢ e2 : τ and e1e2 then Γ ⊢ e1 : τ, is called subject expansion. It often does not hold as evaluation can erase ill-typed sub-terms of an expression, resulting in a well-typed one.


This article is issued from Wikipedia - version of the 5/5/2014. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.