Same variable considered different

[roeger]

Subject of the issue

If I parse an axiom (:derived (P ?v - mytype) (Q ?v))), the two occurrences of ?v are different variables. I am not sure whether I consider this a bug but it is definitively surprising and it took me a while to figure out why my code does not work as expected.

I did not check how it is with action parameters and variables occurring in the precondition and effect, but the situation is analogous.

Steps to reproduce

You can use the following PDDL domain (remove .txt suffix):
domain_same_variable_different.pddl.txt

import pddl

domain = pddl.parse_domain("domain_same_variable_different.pddl")
axiom = next(iter(domain.derived_predicates))
print(axiom)
var1 = axiom.predicate.terms[0]
var2 = axiom.condition.terms[0]
print("var1:", var1, "var2:", var2)
print("Is this the same variable?", var1 == var2)
print("Why not?") 
print("Type tags of var1:", var1.type_tags)
print("Type tags of var2:", var2.type_tags)

The output is:

(:derived (P ?v) (Q ?v))
var1: ?v var2: ?v
Is this the same variable? False
Why not?
Type tags of var1: frozenset({'mytype'})
Type tags of var2: frozenset()

Expected behaviour

I would have expected that the variables in the axiom condition assume the same type requirements as set in the head, so that the variables are actually equal.

Actual behaviour

They variables from the body have empty type tags and are thus different from the ones in the head.

[haz]

To be clear, it's the variables which are scoped to be the same that you hope are equivalent? So these two ?v's would be different..

(:predicates
    (pred1 ?v)
    (pred2 ?v)
)

As an aside, isn't it infuriating we need to .txt-ify all our PDDLs? We need to send someone from the planning community to go work at GitHub for a spill...

[roeger]

Yes, it is about the scope of variables, independently of whether they are introduced in an action parameter, axiom head or quantified condition.

For example, in the condition of (:derived (P ?v) (exists (?w - mytype) (Q ?v ?w))) the two occurrences of ?w are considered different variables because the type information from the introduction of ?w is not carried over to its occurrence within the atom.

In your example, the two variables are not within the same scope, so they are anyways independent. I currently cannot think of a situation where it is relevant whether they are considered differently or equivalent.

Here is a more interesting case: (:derived (P ?v) (exists (?v) (Q ?v))). It is somewhat silly because the quantified ?v shadows the ?v from the head, but should the axiom parameter ?v be the same as the v in (Q ?v)? Conceptually not, but I would not see this so strict, because we want to be able to consider variables without a full context. So I am fine with two variables being equal if they have the same name and types.

What I struggle with is that the type of the conceptually same variable is not carried over to all of its occurrences (as in my two earlier examples).

[haz]

Thanks, @roeger , all makes sense!

@francescofuggitti @marfvr : So this would require keeping the dictionary of variable to type (from parameters) in the recurse parse call. Something relatively viable?

[marfvr]

So this would require keeping the dictionary of variable to type (from parameters) in the recurse parse call. Something relatively viable?

I added a PR with some tests to keep track of the reported issue and to check whether we would have the same issue with actions (seems we don't). #152

I also added a comment in the PR where I reasoned on how we can achieve our goal and resolve this issue.