lambda演算中的替换与Curry学派的作用
Substitution in the lambda Calculus and the role of the Curry School
AI总结：
本文探讨了lambda演算中替换与alpha同余的相互依赖问题，指出Curry学派的研究优雅地解决了这一让学生困惑的难题，以此颂扬其在替换与alpha同余领域的贡献。
摘要：
替换在数学和计算的基础与实现中扮演着重要角色。在lambda演算中，没有某种形式的替换就无法定义alpha同余，但要让替换和归约正常运作，又需假设某种alpha同余（例如，将lambda项按约束变量取模）。学习lambda演算的学生通常对此感到困惑。Curry学派优雅的著作与研究很好地解决了这一问题。本文是对Curry学派（特别是Hindley和Seldin的优秀著作）在alpha同余与替换方面贡献的颂扬。
英文摘要：
Substitution plays a prominent role in the foundation and implementation of mathematics and computation. In the lambda calculus, we cannot define alpha 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
