2
$\begingroup$

Can you help me with my approach to the following task:

Define simultaneous substitution $\phi[\psi_1,...,\psi_k/p_1,...,p_k]$ recursively.

Usually we have recursive definitions about formulas, but I think here I have to define it rekursively on k?


base case - $k=1$.

$\phi[\psi_1/p_1] = \phi[\psi_1/p_1]$

recursive case - $k > 1$.

Let $p^'_k$ be a variable not in $\psi_i$ for all $i \in \{1,...,k-1\}$ and not in $\phi$.

$\phi[\psi_1,...,\psi_k/p_1,...,p_k] = \left(\left(\phi[p^'_k/p_k]\right)[\psi_1,...,\psi_{k-1}]\right)[p_k/p^'_k]$

  • 1
    No ... since you want to have *simultaneous* substitution (and not one after the other as in recursion on $k$), I think you have to do it by recursion on $\phi$.2012-05-14
  • 0
    @martini: But how to do it by recursion on $\phi$? Aim is to define simultaneous substitution so I can't use a simultaneous substitution e. g. in the recursive case $\phi = \phi_1 \circ \phi_2$ as $\phi[\psi_1,...,\psi_k/p_1,...,p_k] = \phi_1[\psi_1,...,\psi_k/p_1,...,p_k] \circ \phi_2[\psi_1,...,\psi_k/p_1,...,p_k]$ since simultaneous recursion isn't defined at this moment!2012-05-14
  • 1
    When you use resursion on formulas, you start with basic formulas. So in you recursive step above, you haven't defined substitution for $\phi$, but for $\phi_1$ and $\phi_2$.2012-05-15

1 Answers 1