# lambda calculus – PCF encoding and denotational semantics of simple recursive function

Let $$f$$ be the function:

$$f(n: mathbb{N}) = text{if }(n > 0) text{ then } 0 text{ else } f(n-1)$$

I encode it in PCF following the notations in a standard text in denotational semantics:

$$f = Y_{sigma}(lambda f: nat to nat. lambda n: nat. text{ifz}(n,0,pred(n))$$

Then I try to compute its semantics:

$$((vdash f ))5 = mu(((lambda f. lambda n. text{ifz}(n,0,pred(n))))) = mu(Lambda (f vdash ((lambda n. text{ifz}(n,0,pred(n))))5))$$

However, from here the computation seems confusing. For instance, what value should $$f$$ have according to the annotated environment (in this case $$5$$).

Denotational semantics rules: