2
$\begingroup$

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

$\endgroup$
2
$\begingroup$

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

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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