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.
Content
Author and article information
Contributors
William M. Farmer
Conference
Publication date:
July
1999
Publication date
(Print):
July
1999
Pages: 1-13
Affiliations
[0001]St. Cloud State University
St. Cloud, Minnesota, USA