tp : type.
tm : type.

arr : tp → tp → tp.

app : tm → tm → tm.
lam : tp → (tm → tm) → tm.

value : tm → type.
step : tm → tm → type.
s_app1 : step E1 E1' → step (app E1 E2) (app E1' E2).
s_app2 : value E1 → step E2 E2' → step (app E1 E2) (app E1 E2').
s_app3 : value E2 → step (app (lam T (\x. E1 x)) E2) (E1 E2).

has_type : tm → tp → type.
is_app : has_type E1 (arr T1 T2) → has_type E2 T1 → has_type (app E1 E2) T2.
is_lam :
  ({x : tm} has_type x T1 → has_type (E x) T2) →
    has_type (lam T1 (\x. E x)) (arr T1 T2).

rec pres : ( ⊢ has_type E T) → ( ⊢ step E E') → ( ⊢ has_type E' T) =
fn d ⇒ fn s ⇒
  case s of
  | [ ⊢ s_app1 S1] ⇒ let [ ⊢ is_app D1 D2] = d in
    let [ ⊢ D1'] = pres [ ⊢ D1] [ ⊢ S1] in [ ⊢ is_app D1' D2]
  | [ ⊢ s_app2 V S2] ⇒ let [ ⊢ is_app D1 D2] = d in
    let [ ⊢ D2'] = pres [ ⊢ D2] [ ⊢ S2] in [ ⊢ is_app D1 D2']
  | [ ⊢ s_app3 V] ⇒ let [ ⊢ is_app (is_lam (\x. \d. D1 x d)) D2] = d in
    [ ⊢ D1 _ D2];

© Computation and Logic Group
Department of Computer Science, McGill University
3480 University Street, Montreal, Quebec, Canada, H3A 0E9