Lambda-definable partial function
= Lambda-definable partial function
A partial function is lambda-definable when one lambda term maps Church numerals in its domain to the numeral of the output and produces no numeral on inputs outside its domain.