A Scheme for Defining Partial Higher-Order Functions by Recursion

William M. Farmer

1999

Abstract

This paper describes a scheme for defining partial higher-order
functions as the least fixed points of monotone functionals.  The
scheme can be used to define both single functions by recursion and
systems of functions by mutual recursion.  The scheme is implemented
in the IMPS Interactive Mathematical Proof System.  The IMPS
implementation includes an automatic syntactic check for monotonicity
that succeeds for many common recursive definitions.