The Church numeral corresponding to the natural number isA function is a lambda-definable function if some closed lambda term satisfiesfor all natural numbers .
DefineThen beta reduction givesTherefore the successor function is lambda-definable; this is the lambda definition of the successor function.
Articles by others on the same topic
There are currently no matching articles.