- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

— |
note_on_substitutions [2007/03/21 14:57] (current) test created |
||
---|---|---|---|

Line 1: | Line 1: | ||

+ | ====== On substitutions ====== | ||

+ | |||

+ | Let t1[x:=t0] denote the result of substituting all occurrences of variable x in term t1 with the term t0. These rules define substitution recursively: | ||

+ | |||

+ | x[x:=t0] = t2 | ||

+ | y[x:=t0] = y (for any variable y distinct from x) | ||

+ | c[x:=t0] = c (for any constant symbol c) | ||

+ | f(t1,...,tn)[x:=t0] = f(t1[x:=t0],...,tn[x:=t0]) | ||

+ | |||

+ | The first cases are base cases and the last case is recursive case. | ||

+ | |||

+ | For quantifier-free formulas, we similarly substitute recursively. We rename quantified variables along the way to make them distinct from other variables (this avoides accidental "variable capture"): | ||

+ | |||

+ | R(t1,...,tn)[x:=t0] = R(t1[x:=t0],...,tn[x:=t0]) | ||

+ | (t1=t2)[x:=t0] = (t1[x:=t0] = t2[x:=t0]) | ||

+ | (F1 & F2)[x:=t0] = (F1[x:=t0] & F2[x:=t0]) | ||

+ | (~F)[x:=t0] = ~(F[x:=t0]) | ||

+ | (forall y. F) [x:=t0] = forall y. (F[x:=t0]), if y does not occur in t (otherwise, rename y as a bound variable) | ||

+ | (exists y. F) [x:=t0] = exists y. (F[x:=t0]), if y does not occur in t (otherwise, rename y as a bound variable) | ||