Commit 2b2c010a authored by Heiko Becker's avatar Heiko Becker
Browse files

Incorporate Magnus Feedback, remove unused parameters

parent 3e046357
......@@ -23,51 +23,46 @@ let upd_env_simps = define
Small Step semantics for Daisy language, parametric by evaluation function.
*)
let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
`(!x (e:(real)exp) s (env:num->real) (v:real)
(eval:(real)exp->(num->real)->real)
`(!x (e:(real)exp) s (env:num->real) (v:real) eps
(env:num->real).
eval e env = v ==>
sstep (Let x e s) env eval s (upd_env x v env)) /\
(!(c:(real)bexp) s t
(eval:(real)exp->(num->real)->real)
eval_exp eps env e v ==>
sstep (Let x e s) env s (upd_env x v env)) /\
(!(c:(real)bexp) s t eps
(env:num->real).
bval c env eval = T ==>
sstep (Ite c s t) env eval s env) /\
(!(c:(real)bexp) s t
(eval:(real)exp->(num->real)->real)
bval eps env c T ==>
sstep (Ite c s t) env s env) /\
(!(c:(real)bexp) s t eps
(env:num->real).
bval c env eval = F ==>
sstep (Ite c s t) env eval t env) /\
(!(e:(real)exp) (v:real)
(eval:(real)exp->(num->real)->real)
bval eps env c F ==>
sstep (Ite c s t) env t env) /\
(!(e:(real)exp) (v:real) eps
(env:num->real).
eval e env = v ==>
sstep (Ret e) env eval Nop (upd_env (0) v env))`;;
eval_exp eps env e v ==>
sstep (Ret e) env Nop (upd_env (0) v env))`;;
(*
Analogously define Big Step semantics for the Daisy language,
parametric by the evaluation function*)
let bstep_RULES,bstep_INDUCT,bstep_CASES = new_inductive_definition
`(!x (e:(real)exp) s (env:num->real) (v:real)
(eval:(real)exp->(num->real)->real)
`(!x (e:(real)exp) s (env:num->real) (v:real) eps
(env:num->real)
(env2:num->real).
eval e env = v /\ bstep s (upd_env x v env) eval s env2 ==>
bstep (Let x e s) env eval s env2) /\
(!(c:(real)bexp) s1 s2 t
(eval:(real)exp->(num->real)->real)
eval_exp eps env e v /\
bstep s (upd_env x v env) s env2 ==>
bstep (Let x e s) env s env2) /\
(!(c:(real)bexp) s1 s2 t eps
(env:num->real)
(env2:num->real).
bval c env eval = T /\ bstep s1 env eval s2 env2 ==>
bstep (Ite c s1 t) env eval s2 env2) /\
(!(c:(real)bexp) s t1 t2
(eval:(real)exp->(num->real)->real)
bval eps env c T /\
bstep s1 env s2 env2 ==>
bstep (Ite c s1 t) env s2 env2) /\
(!(c:(real)bexp) s t1 t2 eps
(env:num->real)
(env2:num->real).
bval c env eval = F /\ bstep t1 env eval t2 env2 ==>
bstep (Ite c s t1) env eval t2 env2) /\
(!(e:(real)exp) (v:real)
(eval:(real)exp->(num->real)->real)
bval eps env c F /\
bstep t1 env t2 env2 ==>
bstep (Ite c s t1) env t2 env2) /\
(!(e:(real)exp) (v:real) eps
(env:num->real).
eval e env = v ==>
bstep (Ret e) env eval Nop env)`;;
eval_exp eps env e v ==>
bstep (Ret e) env Nop env)`;;
(*
Formalization of the base expression language for the daisy framework
*)
needs "Infra/tactics.hl";;
(* needs "/home/heiko/Git_Repos/hol-light/IEEE/make.ml";; *)
(*
Expressions will use binary operators.
Define them first
......@@ -38,35 +36,27 @@ let m_eps = define `m_eps:real = (&1)`;;
*)
let perturb = define `(perturb:real->real->real) = \r e. r * ((&1) + e)`;;
(*
Define expression evaluation parametric by an "error function".
This function will be used later to express float computations using a perturbation
Define expression evaluation relation parametric by an "error" delta.
This value will be used later to express float computations using a perturbation
of the real valued computation by (1 + d)
Additionally we need an "error id" function which uniquely numbers an expression.
*)
let eval_err = new_recursive_definition exp_REC
`(eval_err (Var name) err_fun env
= perturb (env name) (err_fun (Var name))) /\
(eval_err (Const v) err_fun env
= perturb v (err_fun (Const v))) /\
(eval_err (Binop binop e1 e2) err_fun env
= perturb (eval_binop binop (eval_err e1 err_fun env) (eval_err e2 err_fun env))
(err_fun (Binop binop e1 e2)))`;;
(*
Define real evaluation as stated above:
*)
let eval_real = define
`eval_real (e:(real)exp) (env:num->real) = eval_err e (\x. &0) env`;;
let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition
`(!eps env v delta.
abs delta <= eps ==>
eval_exp eps env (Var v) (perturb (env v) delta)) /\
(!eps env n delta.
abs delta <= eps ==>
eval_exp eps env (Const n) (perturb n delta)) /\
(!eps env b e1 e2 v1 v2 delta.
eval_exp eps env e1 v1 /\
eval_exp eps env e2 v2 /\
abs delta <= eps ==>
eval_exp eps env (Binop b e1 e2) (perturb (eval_binop b v1 v2) delta))`;;
(*
float evaluation is non-deterministic, since the perturbation is existencially quantified
--> state as predicate when float evaluation using errors is valid, related to errors
Define real evaluation as a predicate on the epsilon of the evaluation relation
*)
let is_valid_err_float = define
`is_valid_err_float (err_fun:num->real) <=>
!id. ?n.
(&n = err_fun id \/ --(&n) = err_fun id) /\
abs (&n) <= m_eps`;;
let is_real_value = define
`is_real_value (e:(real)exp) (env:num->real) (v:real) = eval_exp (&0) env e v`;;
(*
Using the parametric expressions, define boolean expressions for conditionals
*)
......@@ -75,13 +65,17 @@ let bexp_INDUCT, bexp_REC = define_type
| less (V)exp (V)exp";;
(*
Define evaluation of booleans for reals
Define evaluation of boolean expressions
*)
let bval_SIMPS = define
`(bval (leq e1 e2) (E:num->real) (eval:(real)exp->(num->real)->real) =
(eval e1 E) <= (eval e2 E)) /\
(bval (less e1 e2) (E:num->real) (eval:(real)exp->(num->real)->real) =
(eval e1 E) < (eval e2 E))`;;
let bval_exp_RULES, bval_exp_IND, bval_exp_CASES = new_inductive_definition
`(!eps env e1 e2 v1 v2.
eval_exp eps env e1 v1 /\
eval_exp eps env e2 v2 ==>
bval eps env (leq e1 e2) (v1 <= v2))/\
(!eps env e1 e2 v1 v2.
eval_exp eps env e1 v1 /\
eval_exp eps env e2 v2 ==>
bval eps env (less e1 e2) (v1 < v2))`;;
(* Simplify arithmetic later by making > >= only abbreviations *)
let gr_simps = define
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment