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)$


1 Answer 1


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*}

  • $\begingroup$ 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. $\endgroup$
    – S0rin
    Apr 21, 2014 at 19:55
  • $\begingroup$ 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. $\endgroup$ Apr 21, 2014 at 20:05
  • $\begingroup$ Are you sure that this is allowed? I cannot find any example in the literature. $\endgroup$
    – S0rin
    Apr 22, 2014 at 11:23
  • $\begingroup$ 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. $\endgroup$ Apr 22, 2014 at 21:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.