Help with simple induction

I am trying to prove the correctness of a simple recursive program, its the function where it returns a string but reversed.

Code:

---

def rev(s):
    if len(s)<2
        return s
    return s[-1]+rev(s[:-1])

---

This is what i have for the proof, I am stuck in the induction step. What am I doing wrong?

P(k): If s is a string and k is len(s), then rev(s) terminates and returns a reverse string of s.

Prove for all k in N, P(k). [PSI]

Basis: For k=0
Then rev(“”) returns “”. [line 1,2]
Therefore reverse of “” is “”, as wanted.
For k=1
Let c be a string s.t. len(c)=k
Then rev(c) returns c. [line 1,2]
Therefore reverse of c is c, as wanted.

I.S.: Let k be in N s.t. k>=1 (@)
Suppose P(k) [I.H.]
Let d be a string s.t. |d|=k+1 i.e. |d|>=2 since k+1>=2 [(@)] (*)

d[-1]+rev(d[:-1]) = rev(d[-1])+rev(d[:-1])
= rev(d[-1]+d[:-1])
= rev(d) [I.H.]

Therefore P(k+1) holds.

Please explain the following notations:

s[k] for k > 0
s[k] for k < 0
s[:k] for k > 0
s[:k] for k < 0
If applicable, other relevant notations, such as s[k:n]

Are s[0] and s[:0] defined?

What exactly is a reverse string s? What facts are known about it?

the code is in python

so for example if
s="hello"
then
s[0]="h"
s[1]="e"
s[2]="l"
s[3]="l"
s[4]="o"
s[-1]="o" (negative index start from end)
s[-2]="l"

s[:1] is a string slice, from the beginning to 1 before the first index

so
s[1:3] = "el"
s[:] = "hello" (not a typo)
s[:3]="hel"
s[3:]="lo"

the function returns the input but reversed, so if input is "hello", then output is "olleh"

Is this what you were asking for?

Thanks, this helps, but it is still not clear what the definition of the reversed string is. Here are possible definitions.

(1) s' = rev(s) if |s'| = |s| and ∀i 0 ≤ i < |s| -> s'[i] = s[-(i+1)]

(2) rev("") = ""; rev(x + s) = rev(s) + x

(3) rev("") = ""; rev(s + x) = x + rev(x)

(In (2) and (3), x denotes an individual character and s denotes a string.)

Of course, these definitions are equivalent, but the proofs corresponding to them are very different.

I'm not understanding your versions of a reversed string. I thought there was only one way. So an empty string as the input would return an empty string, a string of one character, would return the same character, a string of more then one, gets reversed, like in my previous example with "hello". In any case the proof has to relate with the lines of the code. So i guess the definition of a reversed string is the code?

You want to make use of the recursive definition in your proof. I will assume the "operations" I am specifying make things clear, and when I say "+" I am meaning an appropriate concatenation. Then, what you are defining is a function that operates on a string with a length parameter. You're inducting on the length of the string. Of course, the actual input is just the string, but inductively we're concerned with the natural numbers. We can then define P(s) or P(s, n). I will use the latter for clarity instead of appending "for a string s of length n" every time. So,

P(s, 0) = ""
P(s, 1) = s
P(s, 2) = last.character(s) + P(s*, 2-1), s* = s with appropriate characters eliminated
.
.
.
P(s, n) = last.character(s) + P(s*, n-1)

Do you see how the recursive definition works here? Every string will ultimately be turned around by picking off the last character iteratively. If we induct on n or "the length of s" we get something along the lines of

Suppose P(s, n). Then P(s, n+1) = last.character(s) + P(s, n).

The complication that arises here is what is 's' referencing? In our inductive assumption we might have a string "hell" for which P(s) = "lleh". Now, the point of P(s, n+1) is that we might have "hello" which P(s) = o + P(s) = o + lleh = olleh. This doesn't work if the 's' in the first is not something related to the 's' in the second. In particular, we have to set an appropriate condition that 's' in the inductive step is an extension of the 's' in the inductive assumption. Otherwise, it makes no sense to say "because P("dog") we have P("hello") work." Right? If we understand the recursion going on and the necessary conditions, I think the induction is pretty obvious, no?

I still don't understand how to do the induction step. I was thinking to use d as the string thats one length greater for proving P(k+1) (from my first post). Then splitting it into two parts
so
rev(d) = rev(d[:-1]+d[-1])
=d[-1] + rev(d[:-1]) [by I.H.]
=reverse of d

But I think I am skipping steps or this is incorrect because it seems too short.

I think it is a short statement. You have a sentence 's' that can be reversed by P(s), for some length of s. Then suppose s* is one character extension of 's' (extended at the right-hand side). Thus, we're looking at P(s*) = P(s + c) for some extra character c (i.e., P(s*) is of length n+1, given s is of length n. To reverse it we need the reverse of s to the right of c. We get that because last.character(s*) = c, and by definition P(s*) = last.character(s*) + P(s), for which P(s) is the reverse of s, by assumption. But, last.character(s*) = last.character(s+c) = c. Thus, P(s*) = c + P(s). Therefore, if P(s) is recursively reversable, then so is P(s*) which is a length(s) + 1 extension of 's'. The point here is that we have to make 's' arbitrary and define a one character extension to replace our numeric successor operation. The numerical aspect is the same since we're dealing with P(length(s)) → P(length(s)+1), but we cannot make this general to any string (e.g., P("dog") does not mean we can get P("cake")). So we're concerned with P(s) for some string s of a given length n. The thing that is different here is that the induction is on character strings, not numbers, but I hope the approach is analogous.

Ok so I understand the theory with the recursiveness, but I can't understand how to write it up properly.

P(k): If s is a string and k is len(s), then rev(s) terminates and returns a reverse string of s.

Prove for all k in N, P(k). [PSI]

Basis: For k=0
Then rev(“”) returns “”. [line 1,2]
Therefore reverse of “” is “”, as wanted.
For k=1
Let c be a string s.t. len(c)=k
Then rev(c) returns c. [line 1,2]
Therefore reverse of c is c, as wanted.

I.S.: Let k be in N s.t. k>=1
Suppose P(k) [I.H.]
Let s' be an arbitrary string with length k+1, so |s'|>=1
Let s be s'[:-1] so |s|>=0 (*)
Let c be s'[-1] (**)
rev(s')=rev(s+c) [(*),(**)]
=c+rev(s) [I.H., (**)]
=s'[-1]+rev(s'[:-1]) [(*),(**)]
which is the reverse string of s'.
Therefore P(k+1) holds.

Quote:

---

Originally Posted by Sneaky

I'm not understanding your versions of a reversed string. I thought there was only one way.

---

There is only one concept of a reversed string, but several equivalent definitions. This is commonplace in mathematics. For example, a local extremum of a well-behaved function f is also a point where the first derivative changes sign. These are completely different definitions: one uses just comparisons of f(x) for different x while the other uses a derivative, but they end up being equivalent.

The reason this may seem strange when applied to string reversal is that we think about it almost exclusively intuitively. We have a good intuition about a sequence of objects and we don't need precise mathematical definitions to see what's going on, whether some statement about operations on sequences is true or false. I don't know the context of your problem, but it looks like verification of an algorithm. The whole point of verification, especially when it is done on a computer, is to not rely on human intuition and to come up with a low-level formal proof. To a computer, the three definitions that I gave above don't seem a priori equivalent at all.

Quote:

---

So i guess the definition of a reversed string is the code?

---

Well, then the statement borders on a tautology: if the reversal of s is rev(s) by definition, then there is nothing to prove.

Quote:

---

I.S.: Let k be in N s.t. k>=1
Suppose P(k) [I.H.]
Let s' be an arbitrary string with length k+1, so |s'|>=1 You can even say |s'| >= 2.
Let s be s'[:-1] so |s|>=0 (*)
Let c be s'[-1] (**)
rev(s')=rev(s+c) [(*),(**)]
=c+rev(s) [I.H., (**)] I think rev(s+c) = c+rev(s) holds by the definition of rev, not by I.H.
=s'[-1]+rev(s'[:-1]) [(*),(**)]
which is the reverse string of s'.

---

Why exactly is s'[-1]+rev(s'[:-1]) the reverse of s'? Here the precise definition of the reverse is indeed needed.

Let us denote the reverse of s by reverse(s), to distinguish it from rev(s) where rev is the Python code from the OP. Let's adopt definition (3) above:

reverse("") = ""
reverse(s + c) = c + reverse(s)

Then the inductive step, where the I.H. is reverse(s) = rev(s), is

rev(s + c) = c + rev(s) by the definition of rev
= c + reverse(s) by I.H.
= reverse(s + c) by the definition of reverse

Again, this borders on triviality. The situation becomes much more interesting and challenging when the definition of reverse is

reverse("") = ""
reverse(c + s) = reverse(s) + c

Then one needs an additional lemma.

Quote:

---

Originally Posted by bryangoodrich

Suppose P(s, n). Then P(s, n+1) = last.character(s) + P(s, n).

---

This is confusing: in the first sentence, P(s, n) is a proposition, which is either true or false, while in the second sentence it is a function that returns a string. Actually, I appreciate that the OP wrote clearly in the beginning what P is.

P(k): If s is a string and k is len(s), then rev(s) terminates and returns a reverse string of s.

Prove for all k in N, P(k). [PSI]

Basis: For k=0
Then rev(“”) returns “”. [line 1,2]
Therefore reverse of “” is “”, as wanted.
For k=1
Let c be a string s.t. len(c)=k
Then rev(c) returns c. [line 1,2]
Therefore reverse of c is c, as wanted.

I.S.: Let k be in N s.t. k>=1 (@)
Suppose P(k) [I.H.]
Let d be a string s.t. |d|=k+1 i.e. |d|>=2 since k+1>=2 [(@)] (*)
rev(d) = d[-1] + rev(d[:-1]) [by I.H.]

Since len(d)=k+1 (*), len(rev(d[:-1]))=k, so rev(d[:-1]) terminates and returns the reverse of the string d[:-1]. Therefore, rev(d) terminates and returns d[-1] followed by the reverse of d[:-1] [line 3]. So d[-1] plus the reverse string of d[:-1] is the reverse string of d. Therefore P(k+1) holds.


------

Is the Induction step proof OK, if I write it with this conclusion statement? Or rather, does the conclusion statement make sense and does it prove why rev(d) returns the reverse string of d?

Quote:

---

I.S.: Let k be in N s.t. k>=1 (@)
Suppose P(k) [I.H.]
Let d be a string s.t. |d|=k+1 i.e. |d|>=2 since k+1>=2 [(@)] (*)
rev(d) = d[-1] + rev(d[:-1]) [by I.H.] Not by I.H., but by the definition of rev.

Since len(d)=k+1 (*), len(rev(d[:-1]))=k, so rev(d[:-1]) terminates and returns the reverse of the string d[:-1] by the I.H. Therefore, rev(d) terminates and returns d[-1] followed by the reverse of d[:-1] [line 3]. Since d[-1] plus the reverse string of d[:-1] is the reverse string of d, P(k+1) holds.

---

Actually, this is a regular induction on natural numbers, not a structural induction (PSI). To use structural induction, one needs to start with a recursive definition of a string.

Oh sorry, when I say PSI I mean principle of simple induction, because I was taught 3 types of induction, which were psi (look above), pci (p. of complete induction) and structural induction.