Proving a function is a fixed point

Question

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?

Answer 1

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!

Answer 2

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)$.