for introducing a procedure, as well as influencing the development of functional programming techniques involving the use of higher-order functions in Lisp. But early Lisps were not suitable expressions of the lambda calculus because of their treatment of free variables.

A formal lambda system has axioms and a complete calculation rule. It is helpful for the analysis using mathematical