λ演算和其它演算中的λ机制
The lambda mechanism in lambda calculus and in other calculi
摘要：
兰丁的λ演算形式与丘奇的比较表明，独立于λ演算，存在一种机制，用于将参数由变量索引的函数转换为参数由数字索引的通常类型的函数。我们称之为“lambda机制”，并展示了如何在其他演算中使用它。在一阶谓词逻辑中，它可以用来定义新的函数和新的谓词。在纯命令式程序设计语言中，它可以用来提供类似于Algol的过程设施。
英文摘要：
A comparison of Landin's form of lambda calculus with Church's shows that, independently of the lambda calculus, there exists a mechanism for converting functions with arguments indexed by variables to the usual kind of function where the arguments are indexed numerically. We call this the "lambda mechanism" and show how it can be used in other calculi. In first-order predicate logic it can be used to define new functions and new predicates in terms of existing ones. In a purely imperative programming language it can be used to provide an Algol-like procedure facility.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
