Beginners

Download

beginners@haskell.org

January 2024

1 participants
1 discussions

Question about Interpretation as Least Fixed Point from Denotational semantics article
by Dmitriy Matrosov 16 Jan '24

16 Jan '24

Hi. I'm reading denotational semantics article on haskell wikibook and don't understand following statement from the ["Interpretation as Least Fixed Point" chapter][1] chapter: > However, there might be multiple fixed points. For instance, there are > several f which fulfill the specification > > f = n -> if n == 0 then 1 else f (n + 1) > > Of course, when executing such a program, the machine will loop forever on > f(1) or f(2) and thus not produce any valuable information about the value > of f(1). What is this f exactly? If it's just another recursive function, like the factorial was before, then it has a little difference from it to me: the above f is defined on n <= 0 and not defined on n > 0. Whereas factorial is defined on other part of values. Thus, both functions will not produce any results on certain values, if such program is executed: for the above f this is f(1), f(2), etc, but for factorial this is f(-1), f(-2), etc (who prevents me from executing factorial program on negative integers, after all?). Both functions can be approximated using corresponding functional g and fixed point iteration scheme, like was explained in the article earlier: x0, g(x0), g(g(x0)), .. where x0 == _|_ . So, essentially this functions looks to me exactly the same as factorial and i don't understand what this example is supposed to show? If the right hand side is functional g' defined as g'(f) = n -> if n == 0 then 1 else f (n + 1) and we try to find it's fixed point, i.e. such f, that f = g'(f) then i can't understand, why would we try to execute f(1) at all? And by the way, these "multiple fixed points of function f", are they just (const 1) for n <= 0 and any other values for n > 0? I.e. this if n <= 0 then 1 else undefined is least defined fixed point, but this one: if n <= 1 then 1 else undefined is also fixed point, just not the least defined, and this one: if n <= 0 then 1 else 3 is also a fixed point. Is this correct? Thanks. [1]: https://en.wikibooks.org/wiki/Haskell/Denotational_semantics#Interpretation…

1 0