Does a definition of primitive recursion exist for the untyped lambda calculus? Does the definition of primitive recursion require typing for natural numbers?
The only definitions I can find are for the typed lambda calculus: http://www.math.nagoya-u.ac.jp/~garrigue/lecture/2013_tenbo/recfun_en.pdf. Perhaps if I just ignore the types it will still be valid?