• names -> de Bruijn -> names
Might fail, but if it doesn't it will give you back the same process.
• de Bruijn -> names -> de Bruijn
Might give you back a different process, but it will always succeed.
Conversation
What do you mean when you say 'process' here?
1
Sorry, just any kind of term, it's just that I'm doing pi calculus
2
1
Oh, right, np! Why does converting back to names give a different term/process?
1
Going from de Bruin to name you lose information: names might be shadowed. However, you are guaranteed to build a well-scoped process.
1
Ahh right - is it possible to handle this in the conversion? Like, I try to handle shadowing in my core-to-surface language translation pass (core language uses de Bruijn, surface language uses names). I could be doing something wrong though. 😅
1
1
If you are willing to generate fresh names, then absolutely. In my case, if the user provides a well-scoped process, they get the exact well-scoped process back. Though maybe I should not attempt to do this and do the disambiguation?
1
1
Ahh cool! Yeah, fresh names is how I am doing it - I keep hints around of the original names to do it in a best-effort way.
1
1
I guess it's the sensible way forward for any half-serious implementation
Then de Bruijn -> names -> de Bruin would leave with the same syntax, while there wouldn't be much to say about names -> de Bruijn -> names (I guess you could prove that it converges on the second pass?)
1
1
Replying to
Yeah, a similar pattern actually pops up in binary format serialization/deserialization! See the paper on Narcissus:
