`ρ` should not be injected during `.ρ` dispatch

[eyihluyc]

I think our test ρ and nested dispatches is incorrect. This is the term from the test:

⟦
  x ↦ ⟦
    a ↦ ⟦
      b ↦ ⟦ c ↦ ξ.ρ ⟧.c
    ⟧.b
  ⟧.a, 
  λ ⤍ Package
⟧

Here, formation that contains attribute c is inside formation that contains attribute b, which is inside formation that contains a. In other words, a-object is/should be ρ of b-object which should be ρ of c-object.

Here are first few steps of normalizing an object from the test. First several steps are OK:

Dataizing: ⟦
  x ↦ ⟦
    a ↦ ⟦
      b ↦ ⟦ c ↦ ξ.ρ ⟧.c
    ⟧.b
  ⟧.a, 
  λ ⤍ Package
⟧

R_DOT: ⟦
  x ↦ ⟦
    a ↦ ⟦
      b ↦ ⟦ c ↦ ξ.ρ ⟧.ρ
    ⟧.b
  ⟧.a, 
  λ ⤍ Package
⟧

R_DOT: ⟦
  x ↦ ⟦
    a ↦ ⟦
      c ↦ ξ.ρ, 
      ρ ↦ ⟦ b ↦ ⟦ c ↦ ξ.ρ ⟧.ρ ⟧
    ⟧.ρ
  ⟧.a, 
  λ ⤍ Package
⟧

And then there is a problematic reduction. It is R_DOT on ⟦ c ↦ ξ.ρ, ρ ↦ ⟦ b ↦ ⟦ c ↦ ξ.ρ ⟧.ρ ⟧ ⟧.ρ

R_DOT: ⟦
  x ↦ ⟦
    a ↦ ⟦
      b ↦ ⟦ c ↦ ξ.ρ ⟧.ρ, 
      ρ ↦ ⟦
        ρ ↦ ⟦ b ↦ ⟦ c ↦ ξ.ρ ⟧ .ρ ⟧,
        c ↦ ξ.ρ
      ⟧
    ⟧
  ⟧.a, 
  λ ⤍ Package
⟧

From here on, ρ of b-object is a c-object (and before that, it was assumed it should be an a-object).

R_DOT: ⟦
  x ↦ ⟦
    b ↦ ⟦ c ↦ ξ.ρ ⟧.ρ, 
    ρ ↦ ⟦
      ρ ↦ ⟦
        b ↦ ⟦ c ↦ ξ.ρ ⟧.ρ
      ⟧,
      c ↦ ξ.ρ
    ⟧
  ⟧,
  λ ⤍ Package
⟧

Normal form: ⟦
  x ↦ ⟦
    b ↦ ⟦ c ↦ ξ.ρ ⟧.ρ, 
    ρ ↦ ⟦
      ρ ↦ ⟦
        b ↦ ⟦ c ↦ ξ.ρ ⟧.ρ
      ⟧,
      c ↦ ξ.ρ
    ⟧
  ⟧,
  λ ⤍ Package
⟧

Overall, this happens when/because we inject (with substitution) a formation that does not have ρ. After such injection, information about the "original" ρ gets lost.

[eyihluyc]

Here is the modification of the example that involves delta and two non-joinable paths:

⟦ a ↦ ⟦ 
    b ↦ ⟦ y ↦ ⟦ Δ ⤍ 01- ⟧ ⟧.ρ,
    x ↦ ξ.ρ.y, 
  ⟧.b,
  y ↦ ⟦ Δ ⤍ 02- ⟧
⟧.a.x

Normal order of evaluation

With the normal order of evaluation, we reduce .a first and inject the correct ρ into the object:

⟦ b ↦ ⟦ y ↦ ⟦ Δ ⤍ 01- ⟧ ⟧.ρ,
  x ↦ ξ.ρ.y,
  ρ ↦ ⟦ 
    a ↦ ...,
    y ↦ ⟦ Δ ⤍ 02- ⟧
  ⟧
⟧.b.x

After that everything goes as expected and the result is ⟦ Δ ⤍ 02- ⟧.

When inner reductions go first

If .b reduction is performed first, we get

⟦ a ↦ ⟦ 
    y ↦ ⟦ Δ ⤍ 01- ⟧,
    ρ ↦ ⟦ 
      b ↦ ⟦ y ↦ ⟦ Δ ⤍ 01- ⟧ ⟧.ρ,
      x ↦ ξ.ρ.y
    ⟧
  ⟧.ρ,
  y ↦ ⟦ Δ ⤍ 02- ⟧
⟧.a.x

Then, when we do inner .ρ, as a result of substitution wrong ρ attribute gets inserted:

⟦ a ↦ ⟦ 
    b ↦ ⟦ y ↦ ⟦ Δ ⤍ 01- ⟧ ⟧.ρ,
    x ↦ ξ.ρ.y
    ρ ↦ ⟦ 
      y ↦ ⟦ Δ ⤍ 01- ⟧,
      ρ ↦ ...
    ⟧
  ⟧,
  y ↦ ⟦ Δ ⤍ 02- ⟧
⟧.a.x

After this step, the evaluation ends with ⟦ Δ ⤍ 01- ⟧.

[fizruk]

Thank you for the example. Clearly, substitution of the $\rho$-attribute is not quite correct. I see 3 ways of handling this:

1. Add locator increment to the substitution definition (when we attach to $\rho$).
2. Modify dispatch for $\rho$, so that substitution does not take place (meaning locator decrement does not happen, so it's ok, I think, to not increment it).
3. Allow to override $\rho$-attribute (this would fix the example above, but I'm not sure about the correctness of this approach in general).