PreTalent23.Spl
SimPle Language (SPL)
Inductive expr :=
| Num (n : nat)
| Bool (b : bool)
| ITE (c t f : expr)
| And (e1 e2 : expr)
| Or (e1 e2 : expr)
| Not (e : expr)
| Le (e1 e2 : expr)
| Eq (e1 e2 : expr)
| Add (e1 e2 : expr)
| Sub (e1 e2 : expr)
| Mul (e1 e2 : expr).
Example add23 := Add (Num 2) (Num 3).
Example if3le5 := ITE ((Le (Num 3) (Num 5))) (Num 2) (Num 3).
Example bad_prog := ITE (Num 3) (Num 4) (Num 5).
Example sub74 := Sub (Num 7) (Num 4).
The semantics of SPL
Useful functions for working with results
We define two functions on result for computing one result based on an earlier result. The function when_num takes an r and function f that applies when the input is a number. If r is indeed a number, we get the result of f applied to that number. Otherwise, we get an error. The function when_bool is defined similarly.Definition when_num (r : result) (f : nat → result) : result :=
match r with
| NumRes n => f n
| _ => Err
end.
Notation "r >>n= f" := (when_num r f) (at level 60, right associativity).
Lemma when_num_not_Err r f : r >>n= f ≠ Err → r ≠ Err.
Proof. intros Hr ->; apply Hr; trivial. Qed.
Lemma when_num_correct1 r f : r >>n= f ≠ Err → ∃ n, r = NumRes n.
Proof. destruct r; [eauto|simpl; congruence|simpl; congruence]. Qed.
Lemma when_num_correct2 r f :
r >>n= f = Err → r = Err ∨ (∃ b, r = BoolRes b) ∨ ∃ n, r = NumRes n ∧ f n = Err.
Proof. destruct r; eauto. Qed.
Definition when_bool (r : result) (f : bool → result) : result :=
match r with
| BoolRes b => f b
| _ => Err
end.
Notation "r >>b= f" := (when_bool r f) (at level 60, right associativity).
Lemma when_bool_not_Err r f : r >>b= f ≠ Err → r ≠ Err.
Proof. intros Hr ->; apply Hr; trivial. Qed.
Lemma when_bool_correct1 r f : r >>b= f ≠ Err → ∃ b, r = BoolRes b.
Proof. destruct r; [simpl; congruence|eauto|simpl; congruence]. Qed.
Lemma when_bool_correct2 r f :
r >>b= f = Err → r = Err ∨ (∃ n, r = NumRes n) ∨ ∃ b, r = BoolRes b ∧ f b = Err.
Proof. destruct r; eauto. Qed.
The eval function
We define the eval function as follows:Exercise (in class)
Complete the [eval] function below:
Fixpoint eval (e : expr) : result :=
match e with
| Num n => NumRes n
| Bool b => BoolRes b
| ITE c t f =>
eval c >>b= (λ b, if b then eval t else eval f)
| And e1 e2 => eval e1 >>b= (λ b1, eval e2 >>b= (λ b2, BoolRes (b1 && b2)))
| Or e1 e2 => eval e1 >>b= (λ b1, eval e2 >>b= (λ b2, BoolRes (b1 || b2)))
| Not e => eval e >>b= (λ b, BoolRes (negb b))
| Le e1 e2 => eval e1 >>n= (λ n1, eval e2 >>n= (λ n2, BoolRes (Nat.leb n1 n2)))
| Eq e1 e2 => eval e1 >>n= (λ n1, eval e2 >>n= (λ n2, BoolRes (Nat.eqb n1 n2)))
| Add e1 e2 => eval e1 >>n= (λ n1, eval e2 >>n= (λ n2, NumRes (n1 + n2)))
| Sub e1 e2 => eval e1 >>n= (λ n1, eval e2 >>n= (λ n2, NumRes (n1 - n2)))
| Mul e1 e2 => eval e1 >>n= (λ n1, eval e2 >>n= (λ n2, NumRes (n1 * n2)))
end.
Eval compute in eval add23. (* Should print: NumRes 5 *)
Eval compute in eval if3le5. (* Should print: NumRes 2 *)
Eval compute in eval bad_prog. (* Should print: Err *)
Eval compute in eval sub74. (* Should print: NumRes 3 *)
What goes wrong when we get an error in evaluating SPL programs?
Exercise (in class)
Complete the following typing relations for expressions and results:
Inductive res_typed : result → typ → Prop :=
| NumRes_typed n : res_typed (NumRes n) TNum
| BoolRes_typed b : res_typed (BoolRes b) TBool.
Inductive typed : expr → typ → Prop :=
| Num_typed n : typed (Num n) TNum
| Bool_typed b : typed (Bool b) TBool
| IFE_typed c t f typ :
typed c TBool →
typed t typ →
typed f typ →
typed (ITE c t f) typ
| And_typed e1 e2 :
typed e1 TBool →
typed e2 TBool →
typed (And e1 e2) TBool
| Le_typed e1 e2 :
typed e1 TNum →
typed e2 TNum →
typed (Le e1 e2) TBool.
The eval function respects types
Exercise (in class)
Once the typing relations above are completed, the induction in theorem below will have more cases. Finish the proof.
Theorem eval_respects_types (e : expr) (t : typ) : typed e t → res_typed (eval e) t.
Proof.
intros Htp.
induction Htp.
- constructor.
- constructor.
- simpl.
destruct (eval c).
+ inversion IHHtp1.
+ simpl.
destruct b; trivial.
+ inversion IHHtp1.
- simpl.
destruct (eval e1).
+ inversion IHHtp1.
+ simpl.
destruct (eval e2).
* inversion IHHtp2.
* simpl. constructor.
* inversion IHHtp2.
+ inversion IHHtp1.
-
Abort.
Type soundness
The following theorem is usually referred to as the type safety or type soundness theorem. It states that well-typed programs do not result in an error. The type soundness theorem is one of the main properties that we usually prove about typed programming languages. In our settings, type soundness is a corollary of the theorem above, eval_respects_types.Exercise
Prove the following corollary.
In addition to soundness of a type system, one can ask whether it is complete or not.
That is, is it the case that any program that does not result in an error is well-typed
according to our typing relation?
The answer very often, if not always, is no, and SPL is no exception.
In fact, in SPL there are programs that do not result in an error but are also not well-typed.
Prove the following theorem.
Exercise
Prove the following theorem.