Skip to main content
MathOverflow

Return to Question

link, tags, formatting
Source Link
David Roberts ♦
David Roberts ♦
  • 35.5k
  • 11
  • 124
  • 349

Altenkirch wrote ("α-conversion is easy",in the article is marked as aunpublished draft) "I leave it to the reader to show that (some natural translation functionα-conversion is easy) preserves substitution, i.e. it maps substitutions on named terms as given here to substitution on de Bruijn terms". I'm:

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?

Altenkirch wrote ("α-conversion is easy", the article is marked as a draft) "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?

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?

Source Link
Pavel Shuhray
Pavel Shuhray
  • 71
  • 3

Does substitution on named terms correspond to substitution on de Bruijn terms?

Altenkirch wrote ("α-conversion is easy", the article is marked as a draft) "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?