ex-rec

# LiP assignment #2

## 1. Arithmetic functions defined by recursion

Write the following functions on natural numbers (using no recursion):

1. `iszero: int → bool`, tests for equality with 0
2. `succ: int → int`, computes the successor of a natural number
3. `pred: int → int`, computes the predecessor of a natural number (we stipulate that `pred 0 = 0`).

then, use them to define (using recursion) the functions at items 1 to 7. Note that you cannot use any arithmetical operator (such as +, -, <, > etc…) but only the functions that you have already defined, at previous items.

1. `leq: int → int → bool`, evaluates `leq n m` to true if `n ≤ m`, false otherwise
2. `eq: int → int → bool`, evaluates to true if `n = m`, false otherwise
3. `add: int → int → int`, computes the sum of two naturals
4. `sub: int → int → int`, computes the difference of two naturals (we stipulate that `sub n m = 0` if `n<m`)
5. `mul: int → int → int`, computes the product of two natural numbers
6. `pow: int → int → int`, computes the power of two natural numbers (i.e. `pow n m = nm`)
7. `ack: int → int → int`, the Ackermann function

## 2. Euclid's algorithm for GCD

Write a function `gcd: int → int → int` that computes the GCD between two natural numbers, using Euclid's algorithm.

## 3. Exponential

Write a function `exp : int → int → int` such that `exp n x = xn`. Exploit the fact that x2n = (xn)2, and x2n+1 = (xn)2 x. Hint. Use pattern matching with guards for a cleaner definition.

## 4. Tail recursive absolute value

Write a tail-recursive version of the following function, that computes the absolute value of an integer:

```let rec abs x =
if x=0 then 0
else if x>0 then 1 + abs (1-x)
else 1 + abs (-1-x);;```

## 5. Goldbach's conjecture

Write a primality test for natural numbers, that is a function `isprime: int → bool` such that `isprime n` evaluates to `true` if `n` is prime, `false` otherwise.

Then, write a function `goldbach: unit → bool` such that

• `goldbach ()` evaluates to false, if the Goldbach's conjecture is false
• `goldbach ()` diverges (i.e. it does not terminate), if the Goldbach's conjecture is true 