Abstract

λ-calculi are of interest to logicians and computer scientists but have largely escaped philosophical commentary, perhaps because they appear narrowly technical or uncontroversial or both. I argue that even within logic λ-expressions need to be understood correctly, as functors signifying functions in intension within a categorical or typed language. λ-expressions are not names but pure viable binders generating functors, and as such they are of use in giving explicit definitions. But λ is applicable outside logic and computer science, anywhere where the notions of complex whole, substitution, abstraction and structure make sense. To illustrate this, two domains are considered. One is somewhat frivolous: the study of flags; the other is very serious: manufacturing engineering. In each case we can employ λ-abstraction to describe substitutions within a structure, and in the latter case there is even a practical need for such a notation.