2
$\begingroup$

Altenkirch wrote (in the unpublished draft α-conversion is easy):

I leave it to the reader to show that (some natural translation function) preserves substitution, i.e. it maps substitutions on named terms as given here to substitution on de Bruijn terms.

I'm trying to show it but I can't (and I doubt that his method is suitable). Does anyone have complete proof?

Improve this question
$\endgroup$
1

1 Answer 1

Reset to default
2
$\begingroup$

See the 2021-present work of Joshua Grosso, who formalised the paper in Coq, correcting some errors in the process (last update 3 weeks ago). However, Grosso wrote:

To our knowledge, all of the main results contained within the paper itself have been formalized. (Proving equivalence to de Bruijn terms is still in progress, but because it is left to the reader in the original paper, we are comfortable sharing this formalization as-is.)

So it might be that with the improved treatment the desired equivalence is easier to show?

Improve this answer
$\endgroup$
8
  • $\begingroup$ Is Grosso trying to find a counterexample? (joke) $\endgroup$
    – Pavel Shuhray
    Commented Nov 19, 2023 at 13:14
  • $\begingroup$ @PavelShuhray Personally, I’m not aware of anyone who’s written up a proof of this specific statement. And unfortunately, I haven't yet been able to prove it myself. However, it has been a while since I last thought about the problem, so I should probably take another shot at it! $\endgroup$
    – Josh Grosso
    Commented Nov 20, 2023 at 1:28
  • $\begingroup$ And I definitely wouldn't put much weight on my failure to find a proof—I'm still a student, so my research skills still leave much to be desired :-) $\endgroup$
    – Josh Grosso
    Commented Nov 20, 2023 at 1:30
  • $\begingroup$ @JoshuaGrosso thanks for chiming in! Perhaps you and Pavel can get in touch off-site and combine your efforts? It would be a great MO success story to get a solid answer on this out of the connection made here. $\endgroup$
    – David Roberts ♦
    Commented Nov 20, 2023 at 23:01
  • 1
    $\begingroup$ @DavidRoberts I proved it proofassistants.stackexchange.com/questions/4277/… $\endgroup$
    – Pavel Shuhray
    Commented Oct 22 at 20:34

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .