A more interesting example - repetition

Just as Pascal's conditional statement is replaced by Hope's conditional value, so the repetitive statement is replaced by the repetitive value. Here's a Pascal function that multiplies two numbers using repeated addition:

     function mult ( x, y : INTEGER ) : INTEGER ;
     var prod  : INTEGER ;

          begin
            prod := 0 ;
            while y > 0 do
              begin
           prod := prod + x ;
           y := y - 1
              end ;
            mult := prod
          end ;

It's hard to be sure this function does enough additions (it took me three tries to get it right) and this seems to be a general problem with loops in programs. A common way of checking imperative programs is to simulate their execution. If we do this for input values of 2 and 3, we'll find that prod starts with the value 0 and gets values of 2, 4 and 6 on successive loop iterations, which suggests the definition is correct.

Hope doesn't have any loops, so we must write all the additions that the Pascal program performed in a single expression. It's much easier to see that this has the right number of additions:

     dec mult : num # num -> num ;

     --- mult ( x, y ) <= 0 + x + x + ...

or would be if we knew how many times to write + x. The hand simulation suggests we need to write it y times, which is tricky when we don't know the value of y. What we do know is that for a given value of y, the expressions:

     mult ( x, y )

and

     mult ( x, y-1 ) + x

will have the same number of + x terms if written out in full. The second one always has two terms, whatever the value of y, so we'll use it as the definition of mult:

     --- mult ( x, y ) <= mult ( x, y-1 ) + x ;

On the face of it we've written something ridiculous, because it means we must apply mult to find the value of mult. Remember however that this is really shorthand for 0 followed by y occurrences of + x. When y is zero, the result of mult is also zero because there are no + x terms. In this case mult isn't defined in terms of itself, so if we add a special test for it, the definition terminates. A usable definition of mult is:

     --- mult ( x, y ) <= if y = 0 then 0 else mult ( x, y-1 ) + x ;

Functions that are defined using themselves like this are called recursive. Every Pascal program using a loop can be expressed as a recursive function in Hope. All recursive definitions need one case (called the base case) where the function isn't defined in terms of itself, just as Pascal loops need a terminating condition.