The Container Notation in the \(\lambda \) -Calculus (1): Arithmetic

The chapter explores the intuitiveness, naturalness, and logico-computational power of substitution and \(\beta \) -reduction under the interpretation provided by the container notation (formally defined in Chap. 4 ) on an ordered sequence of self-explanatory examples in arithmetic (addition, multiplication, and exponentiation) developed with all detail. The reduction strategy used is normal order. Two crucial combinators, Church numerals and the encoding of the successor function, are reconsidered before going into the examples. A specific logico-algorithmic format is used for all the examples. Each step of reasoning/computation is divided in two sub-steps: the “external” result of the \(\beta \) -reduction (sub-step i, for \(i\in \mathrm {N})\) and the detail of the substitution operation in terms of the container notation (sub-step \(i_{\beta })\) . More specifically, each sub-step i indicates, by means of overbraces, the subterms which play the roles of the terms \(M \) and \(N \) in the definition 4.1 of \(\beta \) -reducing. Step \( i_{\beta } \) shows the \(\beta \) -reduction operation in action: it has the form of the contractum [N/var]M (the result of substituting N for every occurrence of variable var in \( M)\) . Using the symbols of the container notation, those terms unavailable for substitution are graphically distinguished from those terms in which active substitution is possible \(.\)