Page 56 - Textos de Matemática Vol. 40

44 Chapter 1. Applicative theories
1.8 A case study: least fixed points
A recursively defined program is given by a recursion equation f ( ⃗x ) = t ( f , ⃗x ) ,
where the program f may be called in the body of its definition. Every higher programming language offers a syntactical construction to define programs re- cursively. In general, there are several different solutions to such a recursive definition, i.e., there are several functions satisfying the recursion equation. In every introduction to the semantics of programming languages one finds that the intended semantics is given by the least fixed point of the recursion equa- tion (with respect to the definedness order), cf. e.g., Manna [Man74], Schmidt [Sch86] or Jones [Jon97].
Hence we need a powerful principle to prove statements about recursive programs. Probably the most famous such principle is fixed point induction introduced by Scott [Sco69] which is based on a CPO interpretation of terms. For a good overview of Scott’s induction principle and its connection to CPO models see for example Mitchell [Mit96].
Looking at the untyped λ calculus we find that in continuous λ-models, e.g., Pω or D∞, fixed point combinators are interpreted by the least fixed point operator in the model, cf. e.g., Amadio and Curien [AC98] or Barendregt [Bar84]. This fact makes it possible to prove semantically many properties of recursively defined programs.
However, if we look at the purely syntactical side of formal frameworks which are used to analyze programming languages, we often do not find any direct account to least fixed points. In particular, the untyped λ calculus allows to define a fixed point combinator, but there is no possibility to express the leastness of a fixed point, cf. Curry, Hindley, and Seldin [CHS72], Hindley and Seldin [HS86] or Barendregt [Bar84]. Also in the typed λ calculus we may have fixed point combinators, but the question of leastness, which corre- sponds to termination, is answered from the outside by the use of normalization proofs. Comparing this with functional programming languages we see that in a type free language, like scheme, we can define a fixed point operator which “solves” recursive equations; and in typed languages, like ml, such operators are usually built in. However, there is no way to guarantee on the syntactical level that the solution produced by these operators will be the least fixed point. This is only given by the semantical interpretation, cf. e.g., Reade [Rea89].
Here, our aim is to define an applicative theory which allows to define a least fixed point operator. As we know from Proposition 1.2.2 we have in applicative theories the Recursion Theorem at our disposal which provides a term rec to solve recursive equations. However, it is not provable that a solution obtained by rec is minimal with respect to the natural definedness ordering.
The Section on least fixed points is based on [KS01].