Consider the tail-recursive version of the reverse function we defined in class
ID: 647899 • Letter: C
Question
Consider the tail-recursive version of the reverse function we defined in class a while ago.
Let us represent the reverse of a list l in mathematical notation by writing l^R. Further, let us use the infix operator + to represent the appending of lists at a mathematical level, i.e. l1+ l2 represents the result of appending the two lists l1 and l2. Using this notation, the correctness of reverse can be expressed as the following property:
For all lists l, (reverse l) evaluates to l^R.
The task in this part is to prove that reverse satisfies this property. You are to do this in the following steps:
Articulate a property of rev that you can both prove and that would be helpful in proving that reverse satisfies the property required of it.
Prove the property of rev that you have stated using induction on the structure of lists.
Use the property that you have proved for rev to prove that reverse satisfies the property required of it.
In writing your arguments, you can use simple facts about lists at the mathematical level, such as the following
for all lists l1 and l2 and all x that can be elements of such lists, (x::l1)^R + l2 = l1^R + (x:: l2).
Of course, such properties must be obvious once you write them down, otherwise you must prove them.
Consider now the following function that computes the length of a list:
The task in this part is to show that reverse preserves the lengths of lists, i.e. that
for all lists l, (length (reverse l)) evaluates to the same value as (length l)
Follow the same sequence of steps as in the first part, i.e.
Articulate a property based on length for rev.
Prove the property about rev and length using induction on lists.
Use the property you have proved for rev to conclude that reverse preserves the lengths of lists.
Include solutions to this problem in comment form in the homework file.
Explanation / Answer
let reverse str =
let len = String.length str in
let res = String.create len in
for i = 0 to pred len do
let j = pred len - i in
res.[i] <- str.[j]
done;
(res)