En la teoría de tipos , un sistema de tipos tiene la propiedad de reducción de sujetos (también evaluación de sujetos , preservación de tipos o simplemente preservación ) si la evaluación de expresiones no hace que su tipo cambie. Formalmente, si Γ ⊢ ae 1 : τ y e 1 → e 2 entonces Γ ⊢ e 2 : τ . Intuitivamente, esto significa que a uno no le gustaría escribir una expresión, digamos Haskell de tipo Int, y hacer que se evalúe a un valor v, solo para descubrir que v es una cadena.
Junto con el progreso , es una propiedad metateórica importante para establecer la solidez de los tipos de un sistema de tipos.
La propiedad opuesta, si Γ ⊢ ae 2 : τ y e 1 → e 2 entonces Γ ⊢ e 1 : τ , se llama expansión tema . A menudo no se sostiene, ya que la evaluación puede borrar los sub-términos mal escritos de una expresión, dando como resultado uno bien escrito.
Referencias
- Wright, Andrew K .; Felleisen, Matthias (1994). "Un enfoque sintáctico para escribir solidez". Información y Computación . 115 (1): 38–94. CiteSeerX 10.1.1.44.5122 . doi : 10.1006 / inco.1994.1093 .
- Pierce, Benjamin C. (2002). "8.3 Seguridad = Progreso + Preservación". Tipos y lenguajes de programación . Prensa del MIT. ISBN 978-0-262-16209-8.