Fixed Points of Factorial Function (This is taken from the book Semantics with Applications)

I'm trying to determine the fixed points for the following block:


while (x!=1)  { y = y *x; x = x -1; }



As I understand, a fixed point g has to satisfy the following: 

F g s = g s



where s is a state, F is a functional.

The functional F, in this context, would be defined like so:

if (s x = 1): F g s = s[x -&gt;1]
otherwise: F g s = g s[y -&gt; y*x, x -&gt; x -1]



So now I'm trying to come up with a valid fixpoint g. 

My attempt is this:

if (s x &gt;=1): g s = s[x -&gt; 1]
otherwise: g s = undefined 



I think it's valid since it satisifes  F g s = g s  

Am I on the right track and thinking correctly?

(I'm reading the books Semantic with Applications and the lack of solutions has made it very difficult to verify my thinking)
First, let's simplify your F a bit. Instead of

if (s x = 1): F g s = s[x -&gt;1]
otherwise:    F g s = g s[y -&gt; y*x, x -&gt; x -1]


we can equivalently write

if (s x = 1): F g s = s
otherwise:    F g s = g s[y -&gt; y*x, x -&gt; x -1]


since s is the same as s[x-&gt;1] in the case s x = 1.

Second, we need to be more precise. We can't write s[y -&gt; y*x, ...] since at the left of -&gt; we need a value, and y*x is not a value but an expression. More in detail, y is a variable name whose value (in the current state) is s y. So, we should write instead s[y -&gt; s y * s x, ...]. We get:

if (s x = 1): F g s = s
otherwise:    F g s = g s[y -&gt; s y * s x, x -&gt; s x - 1]


Now, let's check your fixed point claim. Let g be defined as follows:

if (s x &gt;=1): g s = s[x -&gt; 1]
otherwise:    g s = undefined


and let's compute F g s, aiming to check whether F g s = g s for all s.

F g s
= { definition of F }
if (s x = 1): s
otherwise:    g s[y -&gt; s y * s x, x -&gt; s x - 1]
= { let's call s' the last state }
if (s x = 1): s
otherwise:    g s'
      where s' = s[y -&gt; s y * s x, x -&gt; s x - 1]
= { definition of g }
if (s x = 1): s
otherwise:    if (s' x &gt;= 1): s'[x -&gt; 1]
              otherwise:      undefined
      where s' = s[y -&gt; s y * s x, x -&gt; s x - 1]
= { definition of s' }
if (s x = 1): s
otherwise:    if (s x - 1 &gt;= 1): s[y -&gt; s y * s x, x -&gt; 1]
              otherwise:      undefined
= { arithmetics }
if (s x = 1): s
otherwise:    if (s x &gt;= 2): s[y -&gt; s y * s x, x -&gt; 1]
              otherwise:      undefined


This looks quite different to g s! Indeed, your g is not a fixed point.

Intuitively, that code computes the factorial of x (times the original value of y) inside y, 
and loops forever on nonpositive x,
so I would expect a fixed point to be

g s = if (s x &gt;= 1):  s[y -&gt; (s y) * (s x)!, x -&gt; 1]
      otherwise:      undefined