The \(\lambda \) -Calculus as a Formal System of Symbolic Logic and the Container Notation

This chapter introduces the main formal aspects of the syntax of the classical untyped \(\lambda \) -calculus in the context of a formal introduction of the container notation. The chapter also discusses some cognitive aspects of this notation. More specifically, the presentation includes: the syntax of the formal system, the crucial proof-theoretical and computational operation of \(\beta \) -reduction, the Curry-Feys recursive definition of the substitution operation, examples of non-terminating processes, the concept of normal form, the Church-Rosser Theorem, the crucial concept of combinator, the reduction of polyadic functions to monadic functions via Currying, and the formal template for algorithms provided by the \(\lambda \) -calculus (according to Kleene’s explanation), among other aspects. The container notation proposes an intuitive and natural interpretation of the concepts of free and bound variable. The free variable is interpreted as an empty, available container for the operation of active substitution while the bound variable is intuitively interpreted as a completely filled container, one unavailable for any substitution (a no-operation). Each clause of the Curry-Feys recursive definition is interpreted in terms of the container notation and its relationship with Spelke’s work in cognitive science is also showed in the chapter. The notation is used profusely in other chapters.