Substitution plays a prominent role in the foundation and implementation of mathematics and computation. In the lambda calculus, we cannot define congruence without a form of substitution but for substitution and reduction to work, we need to assume a form of alpha congruence (e.g., when we take lambda terms modulo bound variables). Students on a lambda calculus course usually find this confusing. The elegant writings and research of the Curry school have settled this problem very well. This article is an ode to the contributions of the Curry school (especially the excellent book of Hindley and Seldin) on the subject of alpha congruence and substitution.

Original language | English |
---|

Title of host publication | A Century since Principia's Substitution Bedazzled Haskell Curry |
---|

Subtitle of host publication | In Honour of Jonathan Seldin's 80th Anniversary |
---|

Place of Publication | London |
---|

Publisher | College Publications |
---|

Pages | 145-178 |
---|

Number of pages | 34 |
---|

Edition | 1st |
---|

ISBN (Print) | 9781848904361 |
---|

Publication status | Published - 11 Jul 2023 |
---|

Name | Tributes |
---|

Publisher | College Publications |
---|

Volume | 51 |
---|

- General Computer Science
- General Mathematics