# FOL substitution - is it possible to substitute two variables with each other? e.g. $\theta=\{x/y,y/x\}$?

Let $C = m(P,X,Y) \leftarrow m(Q,X,Z), m(R,Z,Y)$.

Is it possible to do the following substitution?

$D = C\theta$ where $\theta = \{Q/R,R/Q\}$ s.t. $D = m(P,X,Y) \leftarrow m(R,X,Z),m(Q,Z,Y)$

Given the usual substitution function $[x/y]$ s.t.

$M[x/y]$ is the result of substituting all free occurrences of '$y$' with '$x$' in $M$,

your desired function can be defined as follows:

$M [x//y] =_{df} M[x'/y][y/x][x/x']$ provided $x'$ doesn't occur in $M$.

Example. Let $C = m(P,X,Y)←m(Q,X,Z),m(R,Z,Y)$. Then:

\begin{align*} D &= C~[Q~//~R]\\ &= [m(P,X,Y)←m(Q,X,Z),m(R,Z,Y)][Q'/R][R/Q][Q/Q'] \\ &= [m(P,X,Y)←m(Q,X,Z),m(Q',Z,Y)][R/Q][Q/Q']\\ &= [m(P,X,Y)←m(R,X,Z),m(Q',Z,Y)][Q/Q']\\ &= m(P,X,Y)←m(R,X,Z),m(Q,Z,Y) \end{align*}

• thank you. Do you know if there is a name for this type of substitution? I have never seen the x//y syntax before. Also, do you know if any literature supporting this? Thanks again. Apr 21 '14 at 19:55
• I believe Curry came up with [x/y], and [x//y] is just syntactic sugar for three of those stacked together to achieve your desired effect, so it's certainly not a new type of substitution. You haven't seen it before because I made the 'x//y' abbreviation up after reading your question. Since [x/y,y/x] has a symmetry to it (hence the chosen equality-like '//' symbol), we can maybe call it symmetric substitution. Apr 21 '14 at 20:05
• Are you sure that this is allowed? I cannot find any example in the literature. Apr 22 '14 at 11:23
• As I said, the //-substitution is just a bunch of /-substitutions, so the question is whether the /-substitution is allowed. If the /-substitution is not given to you, you can easily define it by induction on the structure of FOL formulas. That should be straightforward, except where you have variable-binding operators such as $\forall$, $\exists$, $\lambda$, $\iota$, etc. For those you need to do extra work and rename variables to avoid accidental bindings. Apr 22 '14 at 21:10