-
Notifications
You must be signed in to change notification settings - Fork 2
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
ρ
should not be injected during .ρ
dispatch
#448
Comments
Here is the modification of the example that involves delta and two non-joinable paths:
Normal order of evaluationWith the normal order of evaluation, we reduce
After that everything goes as expected and the result is When inner reductions go firstIf
Then, when we do inner
After this step, the evaluation ends with |
Thank you for the example. Clearly, substitution of the
|
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.The text was updated successfully, but these errors were encountered: