(Taken from Semantics with Applications)
As I see it, the functional F will be defined like so:
(F g)s = s if s x == 0 (F g)s = gs[x -> x -1] if s x!=0
So, the first function is
g1 s = undefined for all s
I don't think this is a fixed point, because when
s x = 0 , the function would output
undefined when it really should be
Am I on the right track?
By that logic, g2 and g3 would be fixed points since they terminate at a state where x = 0.