ρ, σ, τ, the functional S(rρ→σ→τ,sρ→σ, tρ) = (r(t))(s(t)) is a primitive recursive functional For any type τ, and f of type τ, and any g of type 0→τ→τ, the functional R(f,g)0→τ defined recursively as R(f,g)(0) = f, R(f,g)(n+1) = g(n,R(f,g)(n)) is a primitive recursive functional See also Dialectica interpretation Higher-order function Primitive recursive function Simply typed lambda calculus References Proof theory Computability theory