Exercise 2 - Natural numbers once more

Documentation and user's manual

Table of contents

OCaml programs

Exercise 2 - Natural numbers once more

Specification of the type  nat_3

This type gives each natural number a unique representation. It is equipped with these eight functions: These constructors: The basic constructor  zero  constructs the representation of the natural number zero. The inductive constructor  d0  constructs the representation of the natural number that is two times a positive natural number, and the inductive constructor  d1  constructs that of the natural number that is the successor of two times a natural number. The predicate functions  is_even_non_zero  and  is_odd  check whether a natural number is even and positive, and whether a natural number is odd. The accessors  inv_d0  and  inv_d1  are the inverses of the functions  d0  and  d1 . 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_3.mli  file) shows the types of these eight functions: type nat_3 val zero : unit -> nat_3 val d0 : nat_3 -> nat_3 val d1 : nat_3 -> nat_3 val is_even_non_zero : nat_3 -> bool val is_odd : nat_3 -> bool val inv_d0 : nat_3 -> nat_3 val inv_d1 : nat_3 -> nat_3 val print_nat : nat_3 -> unit It also indicates that  nat_3  is an abstract type.

Use  nat_3 .   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:

1

Write the value of type  nat_3  that represents the natural number two.

2

Write the value of type  nat_3  that represents the natural number three.

3

Name:  is_zero . Type:  nat_3 -> bool . Tests whether a natural number is zero.

4

Name:  is_power_of_two . Type:  nat_3 -> bool . Tests whether a natural number is a power of two.

5

Name:  suc . Type:  nat_3 -> nat_3 . Returns the successor of a natural number.

6

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

7

Name:  pre . Type:  nat_3 -> nat_3 . Returns the predecessor of positive natural number.

8

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

Exercise 2 - Natural numbers once more

Documentation and user's manual

Table of contents

OCaml programs