Exercise 1 - Natural numbers again

Documentation and user's manual

Table of contents

OCaml programs

Exercise 1 - Natural numbers again

Specification of the type  nat_2

This type gives each natural number a unique representation. It is equipped with these seven functions: These constructors: The basic constructors  zero  and  one  construct the representations of the natural numbers zero and one. The inductive constructor  sucsuc  constructs the representation of the successor of the successor of a natural number. The predicate functions  is_zero  and  is_one  check whether a natural number is zero and whether a natural number is one. The accessor  prepre  accesses the predecessor of the predecessor of a natural number greater than one. 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_2.mli  file) shows the types of these seven functions: type nat_2 val zero : unit -> nat_2 val one : unit -> nat_2 val sucsuc : nat_2 -> nat_2 val is_zero : nat_2 -> bool val is_one : nat_2 -> bool val prepre : nat_2 -> nat_2 val print_nat : nat_2 -> unit It also indicates that  nat_2  is an abstract type.

Use  nat_2 .   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

Name:  is_even . Type:  nat_2 -> bool . Tests whether a natural number is even.

2

Name:  two_times . Type:  nat_2 -> nat_2 . Returns two times a natural number.

3

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

4

Name:  half . Type:  nat_2 -> nat_2 . Returns the half of a natural number.

5

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

6

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

7

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

Exercise 1 - Natural numbers again

Documentation and user's manual

Table of contents

OCaml programs