Feasible functionals and intersection of ramified types

We show that the basic feasible functions of Cook and Urquhart's BFF [8,9] are precisely the functionals definable in a natural system of ramified recurrence that uses type intersection (for tier-variants of a common type). This further confirms the stability of BFF as a notion of computational feasibility in higher type. It also suggests the potential usefulness of type-intersection restricted to sort-variants of a common type.

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Daniel Leivant
• Keywords: Basic Feasible Functions, Common Type, ENTCS 2002, Type Intersection