Warning

Documentation and user's manual

Table of contents

OCaml programs

Warning

From this valid mathematical formula 0! = 1 and n! = n (n - 1)! for any positive natural number n immediately follows a correct recursive definition of the factorial function.

Now consider another valid mathematical formula a + b = b + a for any pair (a,b) of integers from which follows this recursive definition let rec add = function a, b -> add (b, a) Any application of  add  loops.

So, consider both formulas and the meaning of the word valid in both cases. The first formula is a valid definition of factorials. The second formula is a valid expression of the commutativity of addition of integers. But it is not a definition of the addition of integers. She is also a valid expression of the commutativity of multiplication of integers or of addition of real numbers for instance. Look at the type of  add  val add : 'a * 'b -> 'c It is fully polymorphic then it does not refer to a type whose values could represent integers. Yet  add  is (bound to) a well-typed functional value! Therefore it can be applied ... but never returns a result. Its range is empty, that is, it is defined nowhere. Thus it is useless.

Given a functional value (or a type) the useful formulas are those that express a way to construct this functional value (or this type). To be such a formula must contain a basis (case). The formula related to  add  has no basis. Similarly this code type int_bin_tree = Plant of int * int_bin_tree * int_bin_tree (* induction *) does not contain a basis. Yet evaluating this phrase does not fail. But no value of this type  int_bin_tree  can be expressed! Thus it is useless.

The existence of a basis is necessary but it is not sufficient. For instance this does not define the predicate function checking whether a natural number is even let rec is_even = function n -> (* n >= 0 *) if n = 0 then true (* basis *) else is_even (n - 2) (* induction *) This codes only defines the function indicating that an even number is even! To get a correct definition the basis must be widened: let rec is_even = function n -> (* n >= 0 *) if n <= 1 then if n = 0 then true (* basis *) else false (* basis *) else is_even (n - 2) (* induction *)

Warning

Documentation and user's manual

Table of contents

OCaml programs