Recursive Definitions of Partial Functions and Their Computations

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.