= Lambda representation of partial computable functions
Every <partial computable function> is represented on <Church numerals> by a closed <untyped lambda calculus> term. First represent all <primitive recursive functions> using zero, successor, projections, composition and <lambda definition of primitive recursion by pair iteration>. Apply the <Kleene normal form theorem> and search successive history codes with a <fixed-point combinator>. Test the represented total predicate using a <Church numeral zero test>; return the decoded output only on the true branch. If no history passes, normal-order head reduction continues the search indefinitely and the term has no <head normal form>, so cannot be in <beta equivalence> with a <Church numeral>. This avoids the incorrect assumption that a lazy outer <function> must evaluate a divergent argument in an unguarded composition.
Back to article page
