Recursive Definitions of Partial Functions and Their Computations
Abstract
A formal syntactic and semantic model is presented for 'recursive definitions' which are generalizations of those found in LISP for example. Such recursive definitions can have two classes of fixpoints, the strong fixpoints and the weak fixpoints, and also possess a class of computed partial functions. Relations between these classes are presented: fixpoints are shown to be extensions of computed functions. More precisely, strong fixpoints are shown to be extensions of computed functions when the computations may involve 'call by name' substitutions; weak fixpoints are shown to be extensions of computed functions when the computation only involves 'call by value' substitutions. The Church-Rosser property for recursive definitions with fixpoints also follows from these results. Then conditions are given on the recursive definitions to ensure that they possess least fixpoints (of both classes), and computation rules are given for computing these two fixpoints.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 01, 1972
- Accession Number
- ADA022048
Entities
People
- J. M. Cadiou
Organizations
- Stanford University