# Meaning of program as solution of a recursive equation

I would like to ask you a question about (denotational?) semantic of program. After defining program as a transition system, and the semantics as a transition function: $$next: States \rightarrow States$$ the author stated that the meaning of program is the solution of the equation: $$P = next \circ P$$ which is given by: $$fix(\lambda f.next \circ f)$$ I could not get the idea here, what is the "meaning"? and why it is the solution of that equation? How it is related to Tarski's fixpoint theorem?

Could anyone explain for me or give me some references to read about it? Thanks in advance.

• I think you may have more luck with cs.stackexchange because this is a basic question in program semantics and this site prefers research level questions. – Vijay D Jun 6 '13 at 0:44

"Meaning", or "semantics" to use the more technical term, is only the understanding you wish to associate with the text of the program. It can be a mathematical function that specifies abstractedly what the program computes (denotational semantics), or it can be a formal description of how the computation is conducted by a formally defined machinery (operational semantics). It is really a matter of what you are interested in expressing. The program is a big formula, and there are many way in which you may want to interpret it.

You may even be interested in so-called non-standard interpretation that may express specific properties of the program, such as well typedness. Even a prettyprinter, that gives you a string of characters corresponding to a nicely presented version of the program text can be seen as an interpretation, a meaning for it (however trivial). It is much in the eyes of the beholder.

However, the definition of a meaning cannot be arbitrary. It is expected to obey some rules so that it can be used constructively. In particular, a program or formula is produced by composition, by using formal operators to build larger formulae from smaller parts. A meaning, or semantics is expected to follow these compositional rules, so that you can somehow define the meaning of the whole from the meaning of the components. The use high order functions makes the constraint more manageable than appears.

The concept is applicable to other formal structures. For example, the syntax of a programming language is usually defined by a grammar. The grammar can have a meaning that is the set of program (strings) that can be written according to that grammar. It could also be the set of parse-trees for those programs.

Now a standard meaning of program is what it computes, or how it does it (again, partly for consistency reasons, the distinction is often in the eyes of the beholder, depending somewhat on what you do with that formal meaning).

The function $next$ defines what it is to execute one step of the program. Its meaning is a function (on a mathematical domain of states) that gives you the next state after a step of computation given the current state. By applying this function repeatedly, starting from the initial state of your computation, you will ultimately get to a final state that gives you the result ... or computes indefinitely (depending on whether that computation is supposed to terminate).

This means that the effect of running your program is to apply the function : $next \circ next \circ next \circ next \circ ...$ this composition being as long as necessary for all steps of the calculation at hand, possibly infinitely many.

This is better expressed by the fixed-point equation: $P = next \circ P$
since from it you can derive :

• $P = next \circ next \circ P$

• $P = next \circ next \circ next \circ P$

• $P = next \circ next \circ next \circ next \circ P$

• and so on

It shows that any function $P$ satisfying this equation will provide as many steps as needed, applying the function $next$, to get the computation you want to describe.

Now, this requires a minimum of mathematical apparatus to work properly, for the equation to have a mathematical meaning. The mathematical domains used are supposed to allow you to talk about approximating a function. For example a finite composition of $n$ application of the function $next$ is an approximation of $P$ for when the program needs no more than $n$ steps to do its work. Typically, a lattice of ever better approximations will do that (this is what monotonicity is about: getting ever better approximations, as you increase the number of applications). Furthermore, you need this lattice to be continuous, so that the monotonically increasing infinite sequence of approximations of $P$ will have a limit, which is actually the meaning of $P$.

In practice, all this is usually described in a more formal mathematical way, as done for example in the answer of @tathanhdinh.

This technique of approximations can be used as well to describe data structures that contain loops, actually implemented with pointers, though the semantics may not want to know about pointers.

• "The program is a big formula" -- not a big term? – Basil Nov 28 '16 at 10:37
• A big term is probably a better terminology. Thanks. – babou Nov 28 '16 at 22:35

In this case, I guest that "meaning" is "semantics". You can consider the set $\mathcal{P}$ of all partial functions $States \to States$ and the function $Next \colon \mathcal{P} \to \mathcal{P}$ defined by: $$Next(P) = next \circ P$$ for all $P \in \mathcal{P}$. On $\mathcal{P}$ with the ordering by function extension, $Next$ is monotonic, so it has least fixed-point by Kleene theorem. Moreover $Next$ is nothing but $\lambda f.next \circ f$ written in $\lambda$-notation.