next up previous contents index
Next: The Computation System Up: Semantics Previous: Semantics


For the purposes of giving the procedure for evaluation and explaining the semantics of judgements, we would only need to consider substitution of closed terms for free variables and hence would not need to consider simultaneous  substitution or capture. However, for the purpose of specifying inference rules later we shall want to have simultaneous substitution of terms with free variables for free variables. The result of such a substitution is indicated thus:

where , are variables (not necessarily distinct) and are terms. It is handy to permit multiple occurrences of the same variable among the targets for replacements, all but the last of which are ignored. is the result of replacing each free occurrence of in t by for , where is with j the greatest k such that is .

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995