Substitutions

A substitution involves the replacement of all free occurrences of a given variable in an expression with another expression. Here we restrict the substituted expressions to the set of numbers.

Consider the language FUN. Now define a relation e,x,n ⇒se' if e' can be obtained from e by replacing all free occurrences of the variable x by n. The inductive definition of this relation follows:

Expressions
Number	n',x,n ⇒s n'
Variable	x,x,n ⇒s n x',x,n ⇒s x' when x'≠x
Composite	e1,x,n ⇒s e1' e2,x,n ⇒s e2' -------------------------- e1 op e2,x,n ⇒s e1' op e2'
Let	e0,x,n ⇒s e0' ----------------------------------------- let x = e0 in e1,x,n ⇒s let x = e0' in e1        e0,x,n ⇒s e0' e1,x,n ⇒s e1' ----------------------------------------- let x' = e0 in e1,x,n ⇒s let x = e0' in e1' when x'≠x

References

R. Burstall. Language Semantics and Implementation. Course Notes. 1994.