## Solving the Problem

First we need the type of our function `split`:
```split: list alpha -> list alpha # list alpha;
```

What does split do?

```split(k) <= (firstHalf k,secondHalf k);
```

This will work fine provided that we have functions `firstHalf` and functions `secondHalf` with the following specification:

Specification: `firstHalf` is a function which takes a list `k` and returns a list consisting of the first `length(k) div 2` elements of the list. For example `firstHalf [1,2,3,4,5]` should give `[1,2]` since the length is 5 and 5 div 2 is 2.

Now what about `secondHalf`? `secondHalf` is a function which takes a list `k` and returns a list consisting of k after the first `length(k) div 2` elements k have been thrown away. So we have

```firstHalf: list(alpha) -> list(alpha);
firstHalf k <= keep( (length k) div 2 ,k);

secondHalf: list(alpha) -> list(alpha);
secondHalf k <= throwAway( (length k) div 2 ,k);
```
So all that is left to do is specify and design `keep` and `throwAway`.

The function `keep` takes a number `n` and a list `k` and returns a list consisting of the first `n` elements of `k`. That's easy:

```keep: num # list(alpha) -> list(alpha);
keep(0,k) <= [];
keep (n+1,x::k) <= x::keep(n,k);
```

The function `throwAway` takes a number `n` and a list `k` and returns list `k` with the first `n` elements thrown away.

```throwAway: num # list(alpha) -> list(alpha);
throwAway(0,k) <= k;
throwAway (n+1,x::k) <= throwAway(n,k);
```
Our task is now complete. This gives is the complete Hope program:

```throwAway: num # list(alpha) -> list(alpha);
throwAway(0,k) <= k;
throwAway (n+1,x::k) <= throwAway(n,k);

keep: num # list(alpha) -> list(alpha);
keep(0,k) <= [];
keep (n+1,x::k) <= x::keep(n,k);

length: list(alpha) -> num;
length [] <= 0;
length (x::k) <= 1 + length k;

firstHalf: list(alpha) -> list(alpha);
firstHalf k <= keep( (length k) div 2 ,k);

secondHalf: list(alpha) -> list(alpha);
secondHalf k <= throwAway( (length k) div 2 ,k);

split: list alpha -> list alpha # list alpha;
split(k) <= (firstHalf k,secondHalf k);
```
s.danicic@gold.ac.uk
Sebastian Danicic BSc MSc PhD (Reader in Computer Science)
Dept of Computing, Goldsmiths, University of London, London SE14 6NW
Last updated 2010-12-29