# Differences

This shows you the differences between two versions of the page.

 sav08:fol_with_update_expressions [2008/04/09 00:23]vkuncak sav08:fol_with_update_expressions [2015/04/21 17:30] Line 1: Line 1: - ====== FOL with Update Expressions ====== - - Syntactic extension of FOL with if-then-else,​ function update, sets. - - === If-Then-Else === - - ite(p,x,y) = if p then x else y - - === Function Update === - - f (a:=b)(x) - - f ( (a,b) :=c)(x,y) - - === Sets === - - Set variables (not quantified). - - Set operations $\cup$, $\cap$, $\setminus$,​ $\{x,y\}$. - - ===== Syntax Summary ===== - - $\begin{array}{l} - F ::= A \mid F \land F \mid F \lor F \mid \lnot F \mid \exists x.F \mid \forall x.F \\ - A ::= R(T,​\ldots,​T) \mid T=T \mid S \subseteq S \mid S=S \\ - T ::= V_o \mid U(T,​\ldots,​T) \mid ite(F,T,T) \\ - U ::= f \mid U((T,​\ldots,​T):​=T) \\ - S ::= V_s \mid S \cup S \mid S \cap S \mid S \setminus S \mid \{T,​\ldots,​T\} ​ - \end{array}$ - - ===== Elimination of Extensions ===== - - f(a:=b)(x) = ++|ite(x=a,​b,​f(x))++ - - f ( (a,b):=c )(x,y) = ++|ite(x=a & y=b, c,f(x,y))++ - - z=ite(p,​x,​y) $\leftrightarrow$ ++| (p & z=x) | (~p & z=y) ++ - - F(ite(p,​x,​y)) $\leftrightarrow$ ++|F(z) & z=ite(p,​x,​y)++ - - S1 = S0 Un {a} $\leftrightarrow$ ++| ALL x. S1(x) <-> S0(x) | x=a ++ - - === Substituting Function Symbols === - - Consider symbolic execution of assignment to local variable - x = e - Evaluate e in current symbolic state, then assign symbolic value of x to result. - - Consider - x.f = e; - i.e. - f = f(x:=e) - We need to replace f with f(x:=e). - * do we always get syntactically valid formula in FOL extension above?