Library sect_3_1_small_step_lambda

Small-step syntax-directed MSOS for lambda-calculus


Require Export Coq.Lists.List
               Coq.Arith.EqNat
               Coq.Structures.Equalities.

Language syntax

Definition Identifier := nat.

Inductive Expr0 :=
| V0 : Val0 -> Expr0
| T0 : Trm0 -> Expr0
with Val0 :=
| NAT0 : nat -> Val0
| CLO0 : Identifier ->
        Expr0 ->
        list (Identifier * Val0) ->
        Val0
with Trm0 :=
| VAR0 : Identifier ->
        Trm0
| APP0 : Expr0 ->
         Expr0 ->
         Trm0
| ABS0 : Identifier ->
         Expr0 ->
         Trm0.

Auxiliary entities

Environments
Definition Env0 := list (Identifier * Val0).

Fixpoint map_lookup {Value : Type}
                    (m : list (Identifier * Value))
                    (i : Identifier) :=
  match m with
    | nil => None
    | cons (i', v) m' =>
      match beq_nat i i' with
        | true => Some v
        | false => map_lookup m' i
      end
  end.

Fixpoint map_update {Value : Type}
                    (m : list (Identifier * Value))
                    (i : Identifier)
                    (v : Value) :=
  match m with
    | nil => cons (i, v) nil
    | cons (i', v) m' =>
      match beq_nat i i' with
        | true => cons (i, v) m'
        | false => map_update m' i v
      end
  end.

Divergence flag
Inductive Div :=
| UPARROW : Div
| DNARROW : Div.

Labels
Definition Label0 := (Env0 * Div * unit)%type.

Definition get_env0 (l : Label0) : Env0 :=
  match l with
    | (rho, _, _) => rho
  end.

Definition get_div0 (l : Label0) : Div :=
  match l with
    | (_, div, _) => div
  end.

Definition replace_env0 (l : Label0) (e : Env0) : Label0 :=
  match l with
    | (e', d, tail) => (e, d, tail)
  end.

Definition replace_div0 (l : Label0) (div : Div) : Label0 :=
  match l with
    | (rho, div', tail) => (rho, div, tail)
  end.

Definition unobs_label0 (l : Label0) : bool :=
  match l with
    | (e, DNARROW, _) => true
    | (e, UPARROW, _) => false
  end.

Rules

Inductive Step0 : Expr0 -> Label0 -> Expr0 -> Prop :=
| STEP0_VAR x l v :
    unobs_label0 l = true ->
    map_lookup (get_env0 l) x = Some v ->
    Step0 (T0 (VAR0 x)) l (V0 v)
| STEP0_ABS x t l :
    unobs_label0 l = true ->
    Step0 (T0 (ABS0 x t)) l (V0 (CLO0 x t (get_env0 l)))
| STEP0_APP1 t1 e2 e1' l :
    Step0 (T0 t1) l e1' ->
    Step0 (T0 (APP0 (T0 t1) e2)) l (T0 (APP0 e1' e2))
| STEP0_APP2 v1 t2 l e2' :
    Step0 (T0 t2) l e2' ->
    Step0 (T0 (APP0 (V0 v1) (T0 t2))) l (T0 (APP0 (V0 v1) e2'))
| STEP0_APP3 x t e' rho v2 l :
    Step0 (T0 t) (replace_env0 l (map_update rho x v2)) e' ->
    Step0 (T0 (APP0 (V0 (CLO0 x (T0 t) rho)) (V0 v2)))
          l
          (T0 (APP0 (V0 (CLO0 x e' rho)) (V0 v2)))
| STEP0_APP4 x v rho v2 l :
    unobs_label0 l = true ->
    Step0 (T0 (APP0 (V0 (CLO0 x (V0 v) rho)) (V0 v2))) l (V0 v).

Inductive Eval0 : Expr0 -> Label0 -> Expr0 -> Prop :=
| TRANS0 t1 e2 e3 env :
    Step0 (T0 t1) (env, DNARROW, tt) e2 ->
    Eval0 e2 (env, DNARROW, tt) e3 ->
    Eval0 (T0 t1) (env, DNARROW, tt) e3
| REFL0_V v l :
    unobs_label0 l = true ->
    Eval0 (V0 v) l (V0 v).

Small-step syntax-directed MSOS for lambda-calculus with

exceptions
Expr0 is renamed to Expr1 and we add the THROW constructor.
Val0 is renamed to Val1 and we add the UNIT value.
Inductive Expr1 :=
| V1 : Val1 -> Expr1
| T1 : Trm1 -> Expr1
with Val1 :=
| NAT1 : nat -> Val1
| CLO1 : Identifier ->
          Expr1 ->
          list (Identifier * Val1) ->
          Val1
| UNIT1 : Val1
with Trm1 :=
| VAR1 : Identifier ->
           Trm1
| APP1 : Expr1 ->
           Expr1 ->
           Trm1
| ABS1 : Identifier ->
           Expr1 ->
           Trm1
| THROW1 : Val1 ->
           Trm1.

Auxiliary entities

Definition Env1 := list (Identifier * Val1).

We introduce an Exception1 entity
Inductive Exception1 :=
| TAU1 : Exception1
| ERR1 : Val1 -> Exception1.

And an Exc1 read-write label component
Definition Exc1 := (Exception1 * Exception1)%type.

The label is extended by this component.
Definition Label1 := (Env1 * Div * Exc1 * unit)%type.

Definition get_env1 (l : Label1) : Env1 :=
  match l with
    | (rho, _, _, _) => rho
  end.

Definition get_div1 (l : Label1) : Div :=
  match l with
    | (_, div, _, _) => div
  end.

Definition get_exc1 (l : Label1) : Exc1 :=
  match l with
    | (_, _, exc, _) => exc
  end.

Definition replace_env1 (l : Label1) (rho : Env1) : Label1 :=
  match l with
    | (rho', div, exc, tail) => (rho, div, exc, tail)
  end.

Definition replace_div1 (l : Label1) (div : Div) : Label1 :=
  match l with
    | (rho, div', exc, tail) => (rho, div, exc, tail)
  end.

Definition replace_exc1 (l : Label1) (exc : Exc1) : Label1 :=
  match l with
    | (rho, div, exc', tail) => (rho, div, exc, tail)
  end.

Definition unobs_label1 (l : Label1) : bool :=
  match l with
    | (_, DNARROW, (TAU1, TAU1), _) =>
      true
    | (_, _, _, _) => false
  end.

Rules

Added STEP1_THROW M7 rule
Inductive Step1 : Expr1 -> Label1 -> Expr1 -> Prop :=
| STEP1_VAR x l v :
    unobs_label1 l = true ->
    map_lookup (get_env1 l) x = Some v ->
    Step1 (T1 (VAR1 x)) l (V1 v)
| STEP1_ABS x t l :
    unobs_label1 l = true ->
    Step1 (T1 (ABS1 x t)) l (V1 (CLO1 x t (get_env1 l)))
| STEP1_APP1 t1 e2 e1' l :
    Step1 (T1 t1) l e1' ->
    Step1 (T1 (APP1 (T1 t1) e2)) l (T1 (APP1 e1' e2))
| STEP1_APP2 v1 t2 l e2' :
    Step1 (T1 t2) l e2' ->
    Step1 (T1 (APP1 (V1 v1) (T1 t2))) l (T1 (APP1 (V1 v1) e2'))
| STEP1_APP3 x t e' rho v2 l :
    Step1 (T1 t) (replace_env1 l (map_update rho x v2)) e' ->
    Step1 (T1 (APP1 (V1 (CLO1 x (T1 t) rho)) (V1 v2)))
          l
          (T1 (APP1 (V1 (CLO1 x e' rho)) (V1 v2)))
| STEP1_APP4 x v rho v2 l :
    unobs_label1 l = true ->
    Step1 (T1 (APP1 (V1 (CLO1 x (V1 v) rho)) (V1 v2))) l (V1 v)
| STEP1_THROW v l :
    get_exc1 l = (TAU1, ERR1 v) ->
    unobs_label1 (replace_exc1 l (TAU1, TAU1)) = true ->
    Step1 (T1 (THROW1 v)) l (V1 UNIT1).

Updated evaluation rules
Inductive Eval1 : Expr1 -> Label1 -> Expr1 -> Prop :=
| TRANS1 t1 e2 e3 env a a' :
    Step1 (T1 t1) (env, DNARROW, (TAU1, a), tt) e2 ->
    Eval1 e2 (env, DNARROW, (a, a'), tt) e3 ->
    Eval1 (T1 t1) (env, DNARROW, (TAU1, a'), tt) e3
| REFL1_V v l :
    unobs_label1 l = true ->
    Eval1 (V1 v) l (V1 v)
| REFL1_ERR e v l :
    get_exc1 l = (ERR1 v, ERR1 v) ->
    unobs_label1 (replace_exc1 l (TAU1, TAU1)) = true ->
    Eval1 e l e.

Example test_app_abs_throw :
  Eval1 (T1 (APP1 (T1 (ABS1 0 (T1 (VAR1 0))))
                  (T1 (THROW1 (NAT1 42)))))
         (nil, DNARROW, (TAU1, ERR1 (NAT1 42)), tt)
         (T1 (APP1 (V1 (CLO1 0 (T1 (VAR1 0)) nil))
                   (V1 UNIT1))).
Proof.
  eapply TRANS1.
  apply STEP1_APP1.
  apply STEP1_ABS.
  Focus 2.
  eapply TRANS1.
  apply STEP1_APP2.
  apply STEP1_THROW.
  simpl; reflexivity.
  simpl; reflexivity.
  eapply REFL1_ERR.
  simpl; reflexivity.
  simpl; reflexivity.
  simpl; reflexivity.
Qed.

Small-step syntax-directed MSOS for lambda-calculus with

exception handling
Expr1 is renamed to Expr2 and we add the IF, EQ, and CATCH constructors.
Val2 is renamed to Val2 and we add the TRUE and FALSE value. Also, we make exception entities value instances

Inductive Expr2 :=
| V2 : Val2 -> Expr2
| T2 : Trm2 -> Expr2
with Val2 :=
| NAT2 : nat -> Val2
| CLO2 : Identifier ->
          Expr2 ->
          list (Identifier * Val2) ->
          Val2
| UNIT2 : Val2
| TRUE : Val2
| FALSE : Val2
| VEXC : Exception2 ->
          Val2
with Trm2 :=
| VAR2 : Identifier ->
           Trm2
| APP2 : Expr2 ->
           Expr2 ->
           Trm2
| ABS2 : Identifier ->
           Expr2 ->
           Trm2
| THROW2 : Val2 ->
           Trm2
| IF2 : Expr2 ->
           Expr2 ->
           Expr2 ->
           Trm2
| EQ2 : Expr2 ->
           Expr2 ->
           Trm2
| CATCH2 : Expr2 ->
           Expr2 ->
           Trm2
with Exception2 :=
| TAU2 : Exception2
| ERR2 : Val2 -> Exception2.

Auxiliary entities

Definition Env2 := list (Identifier * Val2).

And an Exc2 read-write label component
Definition Exc2 := (Exception2 * Exception2)%type.

The label is extended by this component.
Definition Label2 := (Env2 * Div * Exc2 * unit)%type.

Definition get_env2 (l : Label2) : Env2 :=
  match l with
    | (rho, _, _, _) => rho
  end.

Definition get_div2 (l : Label2) : Div :=
  match l with
    | (_, div, _, _) => div
  end.

Definition get_exc2 (l : Label2) : Exc2 :=
  match l with
    | (_, _, exc, _) => exc
  end.

Definition replace_env2 (l : Label2) (rho : Env2) : Label2 :=
  match l with
    | (rho', div, exc, tail) => (rho, div, exc, tail)
  end.

Definition replace_div2 (l : Label2) (div : Div) : Label2 :=
  match l with
    | (rho, div', exc, tail) => (rho, div, exc, tail)
  end.

Definition replace_exc2 (l : Label2) (exc : Exc2) : Label2 :=
  match l with
    | (rho, div, exc', tail) => (rho, div, exc, tail)
  end.

Definition unobs_label2 (l : Label2) : bool :=
  match l with
    | (_, DNARROW, (TAU2, TAU2), _) =>
      true
    | (_, _, _, _) => false
  end.

Rules

Auxiliary helper predicate for extracting the value from an error entity.
Definition unwrap_err2 (err : Exception2) : Val2 :=
  match err with
    | ERR2 v => v
    | _ => UNIT2
  end.

Added STEP2_ M7 rule
Inductive Step2 : Expr2 -> Label2 -> Expr2 -> Prop :=
| STEP2_VAR x l v :
    unobs_label2 l = true ->
    map_lookup (get_env2 l) x = Some v ->
    Step2 (T2 (VAR2 x)) l (V2 v)
| STEP2_ABS x t l :
    unobs_label2 l = true ->
    Step2 (T2 (ABS2 x t)) l (V2 (CLO2 x t (get_env2 l)))
| STEP2_APP1 t1 e2 e1' l :
    Step2 (T2 t1) l e1' ->
    Step2 (T2 (APP2 (T2 t1) e2)) l (T2 (APP2 e1' e2))
| STEP2_APP2 v1 t2 l e2' :
    Step2 (T2 t2) l e2' ->
    Step2 (T2 (APP2 (V2 v1) (T2 t2))) l (T2 (APP2 (V2 v1) e2'))
| STEP2_APP3 x t e' rho v2 l :
    Step2 (T2 t) (replace_env2 l (map_update rho x v2)) e' ->
    Step2 (T2 (APP2 (V2 (CLO2 x (T2 t) rho)) (V2 v2)))
          l
          (T2 (APP2 (V2 (CLO2 x e' rho)) (V2 v2)))
| STEP2_APP4 x v rho v2 l :
    unobs_label2 l = true ->
    Step2 (T2 (APP2 (V2 (CLO2 x (V2 v) rho)) (V2 v2))) l (V2 v)
| STEP2_THROW v l :
    get_exc2 l = (TAU2, ERR2 v) ->
    unobs_label2 (replace_exc2 l (TAU2, TAU2)) = true ->
    Step2 (T2 (THROW2 v)) l (V2 UNIT2)
| STEP2_IF t e' e1 e2 l :
    Step2 (T2 t) l e' ->
    Step2 (T2 (IF2 (T2 t) e1 e2)) l
          (T2 (IF2 e' e1 e2))
| STEP2_IFTRUE e1 e2 l :
    unobs_label2 l = true ->
    Step2 (T2 (IF2 (V2 TRUE) e1 e2)) l e1
| STEP2_IFFALSE e1 e2 l :
    unobs_label2 l = true ->
    Step2 (T2 (IF2 (V2 FALSE) e1 e2)) l e2
| STEP2_EQ1 t1 e1' e2 l :
    Step2 (T2 t1) l e1' ->
    Step2 (T2 (EQ2 (T2 t1) e2)) l (T2 (EQ2 e1' e2))
| STEP2_EQ2 v1 t2 e2' l :
    Step2 (T2 t2) l e2' ->
    Step2 (T2 (EQ2 (V2 v1) (T2 t2))) l (T2 (EQ2 (V2 v1) e2'))
| STEP2_EQ v1 v2 l :
    v1 = v2 ->
    unobs_label2 l = true ->
    Step2 (T2 (EQ2 (V2 v1) (V2 v2))) l (V2 TRUE)
| STEP2_EQN v1 v2 l :
    v1 <> v2 ->
    unobs_label2 l = true ->
    Step2 (T2 (EQ2 (V2 v1) (V2 v2))) l (V2 FALSE)
| STEP2_CATCH_V v1 e2 l :
    unobs_label2 l = true ->
    Step2 (T2 (CATCH2 (V2 v1) e2)) l (V2 v1)
| STEP2_CATCH t1 e1' e2 l a :
    Step2 (T2 t1) l e1' ->
    get_exc2 l = (TAU2, a) ->
    Step2 (T2 (CATCH2 (T2 t1) e2)) l
          (T2 (IF2 (T2 (EQ2 (V2 (VEXC a)) (V2 (VEXC TAU2))))
                   (T2 (CATCH2 e1' e2))
                   (T2 (APP2 e2 (V2 (unwrap_err2 a)))))).

Inductive Eval2 : Expr2 -> Label2 -> Expr2 -> Prop :=
| TRANS2 t1 e2 e3 env a a' :
    Step2 (T2 t1) (env, DNARROW, (TAU2, a), tt) e2 ->
    Eval2 e2 (env, DNARROW, (a, a'), tt) e3 ->
    Eval2 (T2 t1) (env, DNARROW, (TAU2, a'), tt) e3
| REFL2_V v l :
    unobs_label2 l = true ->
    Eval2 (V2 v) l (V2 v)
| REFL2_ERR e v l :
    get_exc2 l = (ERR2 v, ERR2 v) ->
    unobs_label2 (replace_exc2 l (TAU2, TAU2)) = true ->
    Eval2 e l e.