I'm taking a class in University which involves proving the correctness of computer programs and I'm really bad a proofs, I don't really understand them at all.

Can anyone tell me if my proof actually makes any sense, I frequently think I've written a proof but usually I've proved nothing.

Given this (T1 is a function that takes another function (F) as one of its parameters):

T1(F,x,y) == if y = 0 then x else F(x−1,y−1)

I had to suggest a fixed point solution, I suggested:

f1(x,y) == x - y

Because T1 is a recursive function that implements subtraction. And below I had to prove my suggestion was correct.

To show T1(f1) = f1

T1(f1, x, y) == if y = 0 then x else f1(x−1,y−1)

if y = 0 then x
else (x-1) - (y-1)

if y = 0 then x
else x - y - 2

x - y - 2 = f1(x-1,y-1)

x - y = f1(x,y)

Does my proof have some obvious hole in it that I'm not seeing or is there some mistake I can't see, I think it works but I'm not really sure why it proves anything?


You are thinking of the map: $$T_1(f,x,y) =\begin{cases} x & \text{if } y=0 \\f(x-1,y-1) & \text{otherwise} \end{cases}, $$ and want to show that the function $$ f(x,y)=x-y $$ is a fixed point. This amounts to showing $$ T_1(f,x,y)=f(x,y)=x-y\ $$ for any $x$ and $y$.

There are only two cases one has to check, $y=0$ and $y\neq 0$. If $y=0$, then $T_1(f,x,0)=x=x-0=f(x,0)$, just as we want. If $y\neq 0$, then $T_1(f,x,y)=f(x-1,y-1)=x-1-y+1=x-y=f(x,y)$, and the proof is done.

I don't fully understand the programmatic notation you are using, but I think this is what you are trying to do. However you have evaluated $f(x-1,y-1)$ to $x-y+2$ rather than $x-1-y+1=x-y$, possibly you have forgotten to distribute the minus sign. I hope this helps!

  • $\begingroup$ Thanks for your help and for showing me where I went wrong! $\endgroup$ – Francis Mar 5 at 22:35
  • $\begingroup$ You're very welcome. $\endgroup$ – R_B Mar 5 at 22:36

Your idea is correct, but in the way it's written I don't recognize it as a proof. You want to show that $T_1(f_1,x,y)=f_1(x,y)$ for all $x$ and $y$ in whatever your domain is. So start with $x$ and $y$, distinguish cases for $y=0$ and $y\neq0$, and then show that in both cases $T_1(f_1,x,y)=f_1(x,y)$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.