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 ===== | ||