CODEWITHSUNDEEP
recursionocaml
Zagatho
Zagatho

Reputation: 523

Explaination of recursive function

I want to understand the following code example: 

let rec sumlen = function
  | []     -> (0,0)
  | x::xs  -> let (s,l) = sumlen xs in (s+x,l+1)

The result is clear: It prints out the pair sum and length. But i do not know how this piece of code works.
For example: if i want to print out the sumlen of [1;2;3]: 

    sumlen [1;2;3]  
    let (s,l) = sumlen [2;3] in (s+1,l+1)
    let (s,l) = let (s,l) = sumlen [3] in (s+2,l+1) in (s+1,l+1)
    let (s,l) = let (s,l) = let(s,l) = sumlen [] in (s+3,l+1) in (s+2,l+1) in (s+1,l+1)
    let (s,l) = let (s,l) = let(s,l) = (0,0) in (s+3,l+1) in (s+2,l+1) in (s+1,l+1)

I do not know if I am right, and if I am right why this works.

The reason why I need to understand this, is because i have to prove that

sumlen xs = ( sum xs, length xs )

Can someone help me?
Thank you

Upvotes: 0

Views: 53

Answers (2)

Pierre G.
Pierre G.

Reputation: 4431

agreed with answer of Jeffrey.
I am trying to answer to your comment : "My problem in this snippet was the let...in statement. I dont know how to prove the code."

let (s,l) = let (s,l) = let (s,l) = (3,1) in (s+2,l+1) in (s+1,l+1)

I rewrite it this way:

let (s,l) = 
   let (s,l) =
      let (s,l) = (3,1) 
      in 
   (s+2,l+1)
in
(s+1,l+1)

"let" binds variables in a given scope. The inner let binds (s,l) to (3,0) and returns (5,1) ; which is then used to binds (s,l) in the intermediate scope. The outer let will then bind (s,l) to (6,2) - and this (s,l) is visible at top-level scope.

Upvotes: 0

Jeffrey Scofield
Jeffrey Scofield

Reputation: 66808

There are quite a few ways to understand the code. You can unfold the text repeatedly as you have done. In fact your result is correct if you evaluate it:

# let (s,l) = let (s,l) = let(s,l) = (0,0) in (s+3,l+1) in (s+2,l+1) in (s+1,l+1);;
- : int * int = (6, 3)

This works pretty well for understanding what's going on, but it doesn't work so well for proving things.

As a rule, recursion is related directly to the proof method of induction.

To prove something about this code you can show two things:

  1. It works when the input list is empty.

  2. If it works for a list of length n - 1, then it works for a list of length n.

This would be called "induction on the length of the list".

Different people have different responses to whether induction actually "explains" how the code works. In my opinion, it does explain the code.

Upvotes: 2

Related Questions