Closed eyihluyc closed 3 days ago
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
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- ⟧
.
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- ⟧
.
Thank you for the example. Clearly, substitution of the $\rho$-attribute is not quite correct. I see 3 ways of handling this:
I think our test
ρ and nested dispatches
is incorrect. This is the term from the test:Here, formation that contains attribute
c
is inside formation that contains attributeb
, which is inside formation that containsa
. In other words,a
-object is/should beρ
ofb
-object which should beρ
ofc
-object.Here are first few steps of normalizing an object from the test. First several steps are OK:
And then there is a problematic reduction. It is
R_DOT
on⟦ c ↦ ξ.ρ, ρ ↦ ⟦ b ↦ ⟦ c ↦ ξ.ρ ⟧.ρ ⟧ ⟧.ρ
From here on,
ρ
ofb
-object is ac
-object (and before that, it was assumed it should be ana
-object).Overall, this happens when/because we inject (with substitution) a formation that does not have
ρ
. After such injection, information about the "original"ρ
gets lost.