Writing correct recursive definitions of functions - AgainTutorial (draft)Inductive structuresNatural numbersDocumentation and user's manualTable of contentsOCaml programs

Natural numbers

The non-built-in type  nat_1  is provided by the  Nat_1  module.

Specification
of the
type  nat_1 		 This type gives each natural number a unique representation. It is equipped with these five functions:
  • These constructors:
    • The basic constructor  zero  constructs the representation of the natural number zero.
    • The inductive constructor  suc  constructs the representation of the successor of a natural number.
  • The predicate function  is_zero  checks whether a natural number is zero.
  • The accessor  pre  accesses the predecessor of a positive natural number.
  • The printing function  print_nat  prints a string representation of a natural number.
The interface definition of the module (i.e. the content of the  Nat_1.mli  file) shows the types of these five functions: 

type nat_1
val zero : unit -> nat_1
val suc : nat_1 -> nat_1
val is_zero : nat_1 -> bool
val pre : nat_1 -> nat_1
val print_nat : nat_1 -> unit

It also indicates that  nat_1  is an abstract type.

Use  nat_1 .   For each of the following specifications of functional values first write a mathematical formula then write a recursive definition based on the formula and meeting the specification:

   
  Name:  add . Type:  nat_1 * nat_1 -> nat_1 . Adds two natural numbers.

   
  A mathematical formula:

For all natural numbers m: m+0=m

For all natural numbers m: for all positive natural numbers n: m+n=(m+(n-1))+1

This recursive definition of  add  follows: 

let rec add = function
  m, n -> if is_zero (n)
            then m
            else suc (add (m, pre (n)))

   
  Name:  mult . Type:  nat_1 * nat_1 -> nat_1 . Multiply two natural numbers.

   
  A mathematical formula:

For all natural numbers m: (m)(0)=0

For all natural numbers m: for all positive natural numbers n: mn=(m(n-1))+m

This recursive definition of  add  follows: 

let rec mult = function
  m, n -> if is_zero (n)
            then zero ()
            else add (mult (m, pre (n)), m)

   
  Name:  greater_than . Type:  nat_1 * nat_1 -> bool . Tests whether m > n given a pair (m, n) of natural numbers.

   
  A mathematical formula:

For all natural numbers n: 0 <= n

For all positive natural numbers m: m>0

For all positive natural numbers m: for all positive natural numbers n: m>n if and only if m-1>n-1

This recursive definition of  add  follows: 

let rec greater_than = function
  m, n -> if is_zero (m)
            then false
            else
              if is_zero (n)
                then true
                else greater_than (pre (m), pre (n))

   
  Name:  subtract . Type:  nat_1 * nat_1 -> nat_1 . Returns the natural number m - n given a pair (m, n) of natural numbers where m is greater than of equal to n.

   
  A mathematical formula:

For all natural numbers m: m-0=m

For all natural numbers m: for all positive natural numbers n less than or equal to m: m-n=(m-(n-1))-1

This recursive definition of  add  follows: 

let subtract =
  let rec f = function
    m, n -> if is_zero (n)
              then m
              else pre (f (m, pre (n)))
  in
    function
      m, n -> if greater_than (n, m)
                then failwith ("subtract : the first argument must be >= to the second one")
                else f (m, n)

   
  The function  failwith  has type  string -> 'a . Its application stops the computation and prints its argument.

   
 

In Objective Caml there exist ways of dealing with run-time errors much better than using  failwith !

   
  Name:  nat_of_int . Type:  int -> nat_1 . Converts a non-negative  int  value to the corresponding  nat_1  value.

   
  A mathematical formula:

0 is the first natural number

For all positive natural numbers n: n is the successor of n-1

This recursive definition of  add  follows: 

let nat_of_int =
  let rec f = function n -> (* n >= 0 *)
                            if n = 0 then zero ()
                                     else suc (f (n - 1))
in
  function
    z -> if z >= 0
           then f (z)
           else failwith ("nat_of_int : requires a non-negative integer as its argument") ;;

   
  Name:  int_of_nat . Type:  nat_1 -> int . Converts a  nat_1  value to the corresponding  int  value.

   
  A mathematical formula:

The first natural number is 0

For all non-zero natural numbers n: n is m+1 where m is the predecessor of n

This recursive definition of  add  follows: 

let rec int_of_nat = function
  n -> if is_zero (n)
         then 0
         else int_of_nat (pre (n)) + 1

Latest update : October 5, 2006
This document was translated from LaTeX by Hyperlatex 2.5, which is not the latest version of Hyperlatex.

Writing correct recursive definitions of functions - AgainTutorial (draft)Inductive structuresNatural numbersDocumentation and user's manualTable of contentsOCaml programs