Differences

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

--- sav08:fol_with_update_expressions [2008/04/08 23:55]
vkuncak
+++ sav08:fol_with_update_expressions [2008/04/09 00:23]
vkuncak
@@ Line 1: / Line 1: @@
 ====== FOL with Update Expressions ======
-Syntactic extension of FOL.
+Syntactic extension of FOL with if-then-else, function update, sets.
 === If-Then-Else ===
@@ Line 9: / Line 9: @@
 === Function Update ===
-f(a:=b)(x) = ++|ite(x=a,b,f(x))++
+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 =====
-===== Substituting Function Symbols =====
+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?