The lambda mechanism in lambda calculus and in other calculi

TL;DR

This paper introduces the 'lambda mechanism', a method for transforming functions with variable arguments into standard functions, and demonstrates its application across lambda calculus, predicate logic, and imperative programming languages.

Contribution

It formalizes the lambda mechanism and shows its versatility in defining functions and procedures across different formal systems and programming paradigms.

Findings

The lambda mechanism can convert variable-argument functions into standard functions.

It enables the definition of new functions and predicates in predicate logic.

It provides a procedure facility in imperative programming languages.

Abstract

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.