Word operation definable in the typed \(\lambda\)-calculus (Q1099156)

The problem of representability of word functions over a binary (any finite) alphabet by closed terms of the type \(\underline B^ n\to \underline B\) (where \(\underline B = (0\to 0)\to ((0\to 0)\to (0\to 0)))\) is solved. It is proved that the set FUN Ḇ, i.e. \(\cup^{\infty}_{i=1}Cl(\underline B^ i\to \underline B),\) is finitely generated. This is an extension of Schwichtenberg's and Statman's results.