This is an old revision of the document!
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 , , , .
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
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?