% Subject reduction for the simply typed lambda-calculus % Author: Brigitte Pientka tp:type. %name tp T a. nat: tp. arr: tp -> tp -> tp. exp: type. %name exp E x. lam: tp -> (exp -> exp) -> exp. app: exp -> exp -> exp. % ------------------------------------------------------------------------------ % Typing rules type_of: exp -> tp -> type. %name type_of D u. t_lam: type_of (lam _ E) (arr T T') <- ({x}type_of x T -> type_of (E x) T'). t_app: type_of (app E1 E2) T <- type_of E1 (arr T2 T) <- type_of E2 T2. % ------------------------------------------------------------------------------ % A term is not a lambda-abstraction notLam: exp -> type. n_app: notLam (app M N). % ------------------------------------------------------------------------------ % Reduction relation (big step) step: exp -> exp -> type. s_lam: step (lam T M) (lam T N) <- ({x:exp}step x x -> notLam x -> step (M x) (N x)). s_app1: step (app M N) R <- step M (lam T M') <- step (M' N) R. s_app2: step (app M N) (app M' N') <- step M M' <- notLam M' <- step N N'. % ------------------------------------------------------------------------------ % Subject reduction % Theorem: If G |- type_of M T and G |- step M M' then G |- type_of M' T tps: type_of M T -> step M M' -> type_of M' T -> type. %mode tps +D +S -F. tps_lam: tps (t_lam D) (s_lam S) (t_lam F) <- ({x:exp}{u:type_of x T}{v:step x x}{n:notLam x} tps u v u -> tps (D x u) (S x v n) (F x u)). tps_app1: tps (t_app D2 D1) (s_app1 S2 S1) F <- tps D1 S1 (t_lam F1) <- tps (F1 _ D2) S2 F. tps_app2: tps (t_app D2 D1) (s_app2 S2 _ S1) (t_app F2 F1) <- tps D1 S1 F1 <- tps D2 S2 F2. %block la : block {a:tp}. %block l : some {T:tp} block {x:exp}{u:type_of x T}{v:step x x}{n:notLam x}{d:tps u v u}. %worlds (l | la) (tps D S F). %covers tps +D +S -F. %terminates S (tps D S F). %total S (tps D S F). % Theorem: If . |- type_of M T and . |- step M M' then . |- type_of M' T tps' : type_of M T -> step M M' -> type_of M' T -> type. %mode tps' +D +S -F. t_main: tps' D S F <- tps D S F. %worlds ( ) (tps' D S F). %covers tps' +D +S -F. %terminates S (tps' D S F). %total S (tps' D S F).