lambda 演算中的代入与 Curry 学派的作用
计算机科学中的逻辑
2024-01-08 v1
摘要
代入在数学和计算的基础与实现中扮演着重要角色。在 lambda 演算中，若没有某种形式的代入就无法定义 alpha 同余，但为了使代入和归约生效，我们又需要假设某种形式的 alpha 同余（例如，当我们对 lambda 项模去约束变量时）。学习 lambda 演算课程的学生通常对此感到困惑。Curry 学派的优雅著作和研究很好地解决了这一问题。本文旨在颂扬 Curry 学派（特别是 Hindley 和 Seldin 的优秀著作）在 alpha 同余和代入主题上的贡献。
引用
@article{arxiv.2401.02745,
title = {Substitution in the lambda Calculus and the role of the Curry School},
author = {Fairouz Kamareddine},
journal= {arXiv preprint arXiv:2401.02745},
year = {2024}
}