MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Let $\sigma$ denote an independent simultaneous substitution. Now I wonder if the following holds:

If $\Gamma \vartriangleright (A\ (\sigma\ \tau))\ \rho$ then there are $\psi$, $\phi$ such that $\Gamma \vartriangleright (A\ \sigma)\ \psi$ and $\psi\ \phi = \tau\ \rho$.

Is this true in Prolog?

Best Regards

share|cite|improve this question

closed as not a real question by Andrés E. Caicedo, Dan Petersen, Ryan Budney, S. Carnahan Oct 22 '11 at 9:32

It's difficult to tell what is being asked here. This question is ambiguous, vague, incomplete, overly broad, or rhetorical and cannot be reasonably answered in its current form. For help clarifying this question so that it can be reopened, visit the help center.If this question can be reworded to fit the rules in the help center, please edit the question.

I did not downvote. But your question provides no motivation or evidence —apart from your wondering— and all the notation used is undefined. While it is of course not necessarily that everything be understandable to everyone here, people will express with their votes if they thought they question (and answers) were useful for them in one of a myriad different ways, or not. There is no courage involved in these matters, this is not the far west! – Mariano Suárez-Alvarez Oct 22 '11 at 0:16
I am closing the question because the text provides essentially no context. You may interpret this as a certain success, if you wish. – S. Carnahan Oct 22 '11 at 9:32
By the way, I strongly recommend against deleting comments in a conversation where other people made a good-faith effort to reply. – S. Carnahan Oct 22 '11 at 9:35
I have posted a delete request here:… – Countably Infinite Oct 22 '11 at 21:40

OK, so $\Gamma$ is a set of universal Horn sentences, and $A\sigma$ is a conjunction of atomic formulas. In theory, Prolog is supposed to find substitutions $\rho$ which make the query provable from $\Gamma$, and moreover, such that any other such substitution is less general than one of those which are output. (Essentially, for each admissible propositional skeleton of a resolution proof, it outputs the most general unifier that makes it a proof.)

In this model, the property holds: since $(A\sigma\tau)\rho=(A\sigma)(\tau\rho)$ is entailed by $\Gamma$, $\tau\rho$ must factor through one of the substitutions, call it $\psi$, output for $A\sigma$.

However, this model does not describe actual Prolog, which is neither sound nor complete from the logical point of view. It is not sound, because due to the lack of “occurs check”, most implementations will happily unify terms that are not unifiable, thereby proving formulas that are not provable. I will ignore this problem, as any Prolog program whose result depends on the presence or absence of occurs check is invalid (not conforming to the language standard). Prolog is also incomplete, as it uses a deterministic proof search strategy which may get lost in a cycle before having a chance of finding a valid proof, or the substitution we are looking for. This makes the “de-lifting” property fail.

Here’s an example (using the notation from the comments): $\sigma=[\\ ]$, $A=p(X)$, $\tau=[X=a]$, $\rho=[\\ ]$

?- listing(p).

p(f(A)) :-

?- X=a, p(X).

X = a

?- p(X).

(The second query enters an infinite loop.) Here is another example, where the query is answered, but the needed substitution is never output:

?- listing(p).

p(f(A)) :-

?- X=a, p(X).

X = a

?- p(X).

X = b ;

X = f(b) ;

X = f(f(b)) ;

X = f(f(f(b))) ;

X = f(f(f(f(b)))) ;

X = f(f(f(f(f(b))))) ;

share|cite|improve this answer
Then I really don’t understand your notation. Would you care to clarify your question, starting with specifying what each of the undefined symbols ($\Gamma$, $A$, ...) stands for? And what does “Prolog search with substitution” mean? – Emil Jeřábek May 23 '11 at 19:14
You know, it would really improve matters if you reformulated the original question in a clear, coherent and unambiguous way, instead of this game of having people second-guess what you think and then point out where they failed. People are notoriously incapable of reading other people’s minds. I find it a bit rude that you expect other to do all the work for you, and you can’t be bothered even to properly express what is it that you actually want. Having said that, the last version of your question seems to be already positively answered by the first two paragraphs of my answer. – Emil Jeřábek May 30 '11 at 11:57
A unifier is, by definition, a substitution which makes the entailment hold. A complete set of unifiers is, by definition, a set of unifiers such that every other unifier is a substitution instance of one of them. The abstract model of Prolog is that it outputs a complete list of unifiers. So, the property you want holds essentially by definition, there is nothing to prove. Do you get it? – Emil Jeřábek Oct 19 '11 at 11:57
Do you understand the difference between “there exists” and “for all”? I wrote that $\tau\rho\le\psi_i$ for some $i$, not for all $i$. A unifier of a query $A$ is a substitution $\tau$ such that $A\tau$ is provable from the initial set of Horn clauses (the program), which I also have already written above. I have no idea what “general sense” are you talking about now, but the “de-lifting” lemma is trivial. – Emil Jeřábek Oct 19 '11 at 17:38
I imagine there were other comments, that were later deleted? – Mariano Suárez-Alvarez Oct 22 '11 at 0:11