Lab for Automated Reasoning and Analysis LARA


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

Link to this comparison view

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)
note_on_substitutions.txt · Last modified: 2007/03/21 14:57 by test