Reductions in combinatory logic and Curry's last problem
- 講者何凡 先生 (國立中正大學哲學研究所)
邀請人：廖純中 - 時間2026-11-19 (Thu.) 15:30 ~ 16:45
- 地點資訊所新館106演講廳
摘要
Combinatory logic and λ-calculus have similar motivation, formation, and technical results. It should be no surprise if they correspond to each other closely. However, the most intuitive relation in combinatory logic, say, weak reduction, is not a proper analogue of well-known relations in λ-calculus, say, β-reduction and βη-reduction.
In their book Combinatory Logic, Volume I (1958), Curry and Feys introduced the notion of strong reduction, or η-strong reduction, which is generated from weak reduction. It is later proved that η-strong reduction corresponds to βη-reduction properly. Curry worked on defining a relation in combinatory logic which is analogous to β-reduction in the rest of his life; but until now, defining such a relation, which we should call β-strong reduction here, is still an open problem. This is what Hindley called Curry’s last problem.
In this talk, I shall review the studies of η-strong reduction and β-strong reduction, discuss the difficulty of defining an ideal β-strong reduction, and provide a solution to Curry’s last problem.
In their book Combinatory Logic, Volume I (1958), Curry and Feys introduced the notion of strong reduction, or η-strong reduction, which is generated from weak reduction. It is later proved that η-strong reduction corresponds to βη-reduction properly. Curry worked on defining a relation in combinatory logic which is analogous to β-reduction in the rest of his life; but until now, defining such a relation, which we should call β-strong reduction here, is still an open problem. This is what Hindley called Curry’s last problem.
In this talk, I shall review the studies of η-strong reduction and β-strong reduction, discuss the difficulty of defining an ideal β-strong reduction, and provide a solution to Curry’s last problem.