A Scheme for Defining Partial Higher-Order Functions by Recursion

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

Article

DOI: 10.14236/ewic/IWFM1999.5

SO-VID: 04fbb937-5b8d-4cf5-988b-d2a693b93042

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: 3rd Irish Workshop on Formal Methods

Conference acronym: IWFM

Conference number: 3

Conference location: Galway, Ireland

Conference date: 1st - 2nd July 1999

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Formal Methods

History

Product

1477-9358 BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/IWFM1999.5

Self URI (journal page): https://ewic.bcs.org/

Celebrating 65 years of The Computer Journal - free-to-read perspectives - bcs.org/tcj65

A Scheme for Defining Partial Higher-Order Functions by Recursion

Abstract