Haskell usnig termination in a function-CodePudding

I would like to know more about termination in functions, for example: how termination work in this function when n is a natural number or how I can terminate this function

sum :: Int -> Int
sum 0 = 0
sum n = n   sum (n - 1)

CodePudding user response：

The recursion code works like this - there are two clauses, one which defines itself in terms of itself, and one which terminates the calculation by returning a single value. The termination clause here is sum 0 = 0, and the definition of sum is given by sum n = n sum (n-1).

You can work it out using pen and paper, for the parameter n = 5:

n        sum   
5        5   sum (4)
         5   4   sum (3)
         5   4   3   sum (2)
         5   4   3   2   sum (1)
         5   4   3   2   1   sum (0)
         5   4   3   2   1   0

Because we specified sum (0) as being 0, the calculation ends here.

The calculation can go wrong and never terminate for a number of reasons:

There is no termination clause
The termination clause is never reached

Consider, if you will, the following evil piece of code:

badSum :: Int -> Int
badSum 6 = 6
badSum n = n   badSum (n-1)

badSum 5 -- locks up, press Ctrl-C

Because the termination clause is never reached, the recursion never terminates. Also, for your sum and the illegal value of n = -1.

As an aside, Haskell has two basic integer types, Int and Integer. The type Int is a long integer, whereas Integer is a unlimited integer. Int is faster, but Integer may work better for recursions, particularly in the case where the answer increases very quickly - such as factorials. You have to cast (convert) from one type to the other, as Haskell won't do this for you. In this case, toInteger to cast from Int to Integer, and more generally fromIntegral.

fact :: Int -> Int
fact 1 = 1
fact n = n * fact (n-1)

fact2 :: Int -> Integer
fact2 1 = 1
fact2 n = (toInteger n) * fact2 (n-1)

In both cases, the factorial is defined in terms of itself, with a termination clause of n = 1 resulting in a value of 1. Both do a reasonable job, but for larger n fact starts behaving very oddly indeed:

 n      fact                   fact2
 1                    1                              1
 5                  120                            120
10              3628800                        3628800
20  2432902008176640000            2432902008176640000
30   -8764578968847253504          265252859812191058636308480000000

Because Int is a fixed length integer, eventually the value will wrap around, in this case producing a negative value.

Finally, real-world Haskell wouldn't use a recursion like that. There is a sum function which your code has temporarily replaced. The sum from 1 to n is given by sum [1 .. n], and the factorial is given by product [1 .. n].