I image a bunch of people here have encountered the lambda calculus somewhere. Maybe for some, even before function programming languages. My question is: has anyone been introduced to or seen introductory material that jumps straight to De Bruijn indices, avoiding named variables all together? If so, how was the learning experience? Do you believe it was "harder" than it should have been or "equivalent" (I suppose its normal to struggle with lambda calculus a bit in the beginning, even without De Bruijn indices)?
_Types and Programming Languages_ discusses lambda calculus with variables "up to renaming", then solves the problem by using DeBruijn indices. I'm not sure you could motivate them any faster than that, honestly. The only implementation given uses DeBruijn.
I image a bunch of people here have encountered the lambda calculus somewhere. Maybe for some, even before function programming languages. My question is: has anyone been introduced to or seen introductory material that jumps straight to De Bruijn indices, avoiding named variables all together? If so, how was the learning experience? Do you believe it was "harder" than it should have been or "equivalent" (I suppose its normal to struggle with lambda calculus a bit in the beginning, even without De Bruijn indices)?
_Types and Programming Languages_ discusses lambda calculus with variables "up to renaming", then solves the problem by using DeBruijn indices. I'm not sure you could motivate them any faster than that, honestly. The only implementation given uses DeBruijn.