Commit 7ab24f19 by Heiko Becker

 #+TITLE: Environmental Approximation Relation - Why and How? #+AUTHOR: Heiko Becker #+LATEX_CLASS_OPTIONS: [a4paper] #+LATEX_HEADER:\parindent0pt\usepackage{bussproofs} #+OPTIONS: toc:nil num:nil * State of the framework Before daisys certificate checking supported let-Bindings, there were only arithmetic expressions. Although we needed an evaluation relation, instead of a function, the "state" function in the evaluation could not change. This simplified the soundness proofs for the interval validator and the error bound checker, since there was no need to deal with changed environments. This is not the case for let-bindings. Take for example $f := \textsf{let}~x = e1~\textsf{in}~g$ In the formalization, f will reduce as in lamdba calculus, by adding a binding for variable x to the value environment. The value to which x is bound will change depending on which machine epsilon is used for the evaluation of e1. This means that when proving soundness of the error checker, the proof becomes more complicated since now the environments may not contain the very same values, but rather related values. * Relating values We differentiate between expressions and commands. Expressions are arithmetic expressions that may not introduce binders. Commands can either be a let binding combined with a command or a return statement. For a moment, assume that soundness of error checking for expressions still holds. By soundness, we can upper bound the difference between the real valued execution of e1 and the float valued execution of e1 by the error from the analysis result. This relation can be used to express relations between environments of command executions. Assume that E1 and E2 are already related under a given analysis result A: $E_1 \approx_{A} E_2$ We can now extend this relation by saying that if we get two values $v_R$ and $v_F$. Let the difference between them be upper bounded by $A x$, where x is an arbitrary variable. It must hold that $E_1 [x \mapsto v_R] \approx_{A} E_2 [x \mapsto v_F]$ In combination with a reflexivity rule ($\forall E A. E \approx_{A} E$), we obtain an inductive characterization of an environmental approximation relation. \begin{figure} \begin{prooftree} \AxiomC{} \LeftLabel{Refl} \UnaryInfC{$E \approx_{A} E$} \end{prooftree} % \begin{prooftree} \AxiomC{$E_1 \approx_{A} E_2$} \AxiomC{$|v_R - v_F| \leq A\,x$} \LeftLabel{Approx} \BinaryInfC{$E_1 [x \mapsto v_R] \approx_{A} E_2 [x \mapsto v_F]$} \end{prooftree} \caption{Environment Approximation Relation $\approx$} \end{figure} * Proving soundness With the new environmental approximation relation, soundness of error checking and interval validation now argues both for expressions and commands about two environments, related by that relation. The statements of the lemmas for binary and unary operations, as well as constants and parameters do not change. The only thing changing is that the proof for variables does not follow anymore by contradiction (they were not part of the framework before), but rather from the fact that we were given two related environments.