Redukcja tematu
W teorii typów system typów ma właściwość redukcji podmiotowej (również przedmiotowej , zachowania typu lub po prostu zachowania ), jeżeli ocena wyrażeń nie powoduje zmiany ich typu . Formalnie, jeśli Γ ⊢ e 1 : τ i e 1 → e 2 to Γ ⊢ e 2 : τ . Intuicyjnie oznacza to, że nie chciałoby się napisać wyrażenia, powiedzmy Haskella , typu Int i ocenić je na wartość v , tylko po to, aby dowiedzieć się, że v jest łańcuchem.
Wraz z postępem jest to ważna właściwość metateoretyczna do ustalania poprawności typu systemu typów.
Własność przeciwna, jeśli Γ ⊢ e 2 : τ i e 1 → e 2 to Γ ⊢ e 1 : τ , nazywana jest rozwinięciem podmiotu . Często nie sprawdza się, ponieważ ocena może usunąć źle wpisane podterminy wyrażenia, w wyniku czego powstaje dobrze wpisany.
- Wright, Andrew K.; Felleisen, Matthias (1994). „Składniowe podejście do poprawności typu” . Informacja i obliczenia . 115 (1): 38–94. doi : 10.1006/inco.1994.1093 . S2CID 31415217 .
- Pierce, Benjamin C. (2002). „8.3 Bezpieczeństwo = postęp + ochrona” . Typy i języki programowania . MIT Press. s. 95–98. ISBN 0262162091 . LCCN 2001044428 .