Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:fol_with_update_expressions [2008/04/08 23:55] vkuncak |
sav08:fol_with_update_expressions [2008/04/09 00:15] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== FOL with Update Expressions ====== | ====== FOL with Update Expressions ====== | ||
| - | Syntactic extension of FOL. | + | Syntactic extension of FOL with if-then-else, function update, sets. |
| === If-Then-Else === | === If-Then-Else === | ||
| Line 10: | Line 10: | ||
| f(a:=b)(x) = ++|ite(x=a,b,f(x))++ | 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))++ | ||
| === Sets === | === Sets === | ||
| + | |||
| + | Set variables (not quantified). | ||
| + | |||
| + | Set operations $\cup$, $\cap$, $\setminus$, $\{x,y\}$. | ||
| ===== Syntax Summary ===== | ===== 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 ===== | ===== 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 ===== | ===== Substituting Function Symbols ===== | ||