# 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 ->1]
otherwise: F g s = g s[y -> y*x, x -> x -1]



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

My attempt is this:

if (s x >=1): g s = s[x -> 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 ->1]
otherwise:    F g s = g s[y -> y*x, x -> x -1]


we can equivalently write

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


since s is the same as s[x->1] in the case s x = 1.

Second, we need to be more precise. We can't write s[y -> y*x, ...] since at the left of -> 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 -> s y * s x, ...]. We get:

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


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

if (s x >=1): g s = s[x -> 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 -> s y * s x, x -> s x - 1]
= { let's call s' the last state }
if (s x = 1): s
otherwise:    g s'
where s' = s[y -> s y * s x, x -> s x - 1]
= { definition of g }
if (s x = 1): s
otherwise:    if (s' x >= 1): s'[x -> 1]
otherwise:      undefined
where s' = s[y -> s y * s x, x -> s x - 1]
= { definition of s' }
if (s x = 1): s
otherwise:    if (s x - 1 >= 1): s[y -> s y * s x, x -> 1]
otherwise:      undefined
= { arithmetics }
if (s x = 1): s
otherwise:    if (s x >= 2): s[y -> s y * s x, x -> 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 >= 1):  s[y -> (s y) * (s x)!, x -> 1]
otherwise:      undefined

• Thanks for the explanation! It clarifies things up.I'm just curious though: is g s = s[x->1, y -> 1] for all (s x) a valid fixed point? I looked at the computations and everything seems to check out – nz_21 May 16 '19 at 14:12
• @NZ_21 It is not a fixed point. Consider s0 such that s0 x = 1, s0 y = 4. If g is a fixed point, we must have F g s0 = s0 since s0 x = 1. Instead using your g we get F g s0 = s0[y -> 1]. We can't alter the value of y when s x = 1. – chi May 17 '19 at 7:42