 Curry intended to provide a general theory of functionality as part of a foundation for logic, “pre-logic”, as Curry called it. See in particular (Curry 1934) and, with Robert Feys, (Curry and Feys 1958). At around the same time as Curry’s first publications in the area, Alonzo Church developed his untyped \(\lambda\)-calculus, also designed to provide a foundation for logic, indeed mathematics more generally, and also taking functions, very generally applicable, as fundamental. In these functional calculi, (for a comprehensive account see Barendregt (1984), also the entry on  the lambda calculus)  a concatenation \(fg\) is used to represent the application of function \(f\) to argument \(g\) yielding an output value, where both argument and value can themselves be functions and where self-application is allowed. Whereas Curry’s system is variable-free, variable binding in Church’s occurs by means of the \(\lambda\) term, the variable \(x\) if and where it occurs in \(N\) being bound in \(\lambda x.N\). The fundamental operation in \(\lambda\)-calculus is \(\beta\)-reduction, the transformation which takes us from \((\lambda x.N)M\) to \(N[x := M].\) Here \(N[x := M]\) is the result of substituting \(M\) for all free occurrences of \(x\) in  \(N\).[1]  So, for example, \((\lambda x.xx)f\) \(\beta\)-reduces to \(ff\). We can write this as: 