Tags: variable-substitution math concept inference-rule

variable-substitution (math concept)

See also

python declaration class | python inclusion class | python sample

Definition

variable-substitution is the inference-rule:

\[\left( \boldsymbol{P}, \boldsymbol{\Phi} \right) \vdash \boldsymbol{Q}'\]

Where:

  • \(\boldsymbol{P}\) is a formula-statement that includes \(n\) variables, where \(n\) is a natural-number

  • \(\boldsymbol{\Phi}\) is a finite tuple of \(n\) well-formed formulae,

  • \(\boldsymbol{P}\) is a modified version of \(\boldsymbol{P}\) whose variables have been substituted with the corresponding formulae in \(\boldsymbol{\Phi}\)

Multiple algorithms are possible to implement variable-substitution. Punctilious uses the following algorithm:

  1. Parse \(\boldsymbol{P}\) top-down first, left-right second

  2. Whenever a variable is newly encountered during parsing, assign it a sequential number

  3. Following order, pair every variable in that sequence of variables with formulae in \(\boldsymbol{P}\)

  4. Parse \(\boldsymbol{P}\) and substitute every occurrence of variables with its paired formula

In straightforward language, by substituting the variables in \(\boldsymbol{P}\) with the formulae in \(\boldsymbol{P}\), a new statement \(P'\) follows.