Intrinsic theories for free algebras were introduced at the LCC'94 workshop, along with their ramified versions. We recall the main concepts, outline some new results, and relate these theories to applied lambda calculi and functional programming languages.

The intrinsic theory T(A) for an algebra A refers to no function other than the constructors of A, and uses no axiom other than the closure conditions of A and the schema of induction over A. The provable functional algorithms are those which, taken as a formula (i.e. universal closure of a conjunction of equations), imply in T(A) that the function computed preserves membership in A. For instance, the provable functions of T(N) are precisely the provably recursive functions of Peano Arithmetic, notwithstanding the extreme simplicity of T(N).

Natural restrictions on A-induction yield major computational complexity classes. One can either restrict the syntactic complexity of induction formulas, ramify the algebra, or do both. Depending on the algebra, the syntactic restriction on induction, and the ramification condition, we obtain the classes of primitive recursive, elementary, exponential-time, poly-space, poly-time, linear space, alternating poly-log-space, NC, or alternating log time functions.

Under Schonfinkel-Curry-Howard homomorphisms each restricted implicit theory maps to an applied lambda calculus and a functional programming language, whose computable functions are precisely the provable functions of that theory.