The syntax operation , where , is a total computable function on valid codes: decode the finite syntax trees, form their application, and encode it again. Extend it arbitrarily on invalid codes if necessary. Similarly is total computable because the finite numeral syntax can be generated effectively from . The preceding characterization of lambda-definable functions supplies closed representatives withHere is lambda quotation, not a code of a beta equivalence class. In particular quotes the syntax of the numeral itself; it is not simply successor or an identity operation.
Articles by others on the same topic
There are currently no matching articles.