<p>"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.</p>

<p>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.</p>

<p>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.</p>

<p>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.</p>

<p>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).</p>

<p>Coming back to your example:</p>

<p>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).</p>

<p>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.</p>

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

<ul>
<li><p>$P = next \circ next \circ P$</p></li>
<li><p>$P = next \circ next \circ next \circ P$</p></li>
<li><p>$P = next \circ next \circ next \circ next \circ P$</p></li>
<li><p>and so on</p></li>
</ul>

<p>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.</p>

<p>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$.</p>

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

<p>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.</p>

CC BY-SA 3.0
2016-11-28T10:37:08.777Z
"The program is a big formula" -- not a big _term_?
Basil
CC BY-SA 3.0
2016-11-28T22:35:10.350Z
A big term is probably a better terminology. Thanks.
babou
CC BY-SA 3.0
2013-06-08T11:26:01.777Z
2013-06-08T14:48:37.743Z
2013-06-08T14:48:37.743Z
babou
<p>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.</p>

CC BY-SA 3.0
2013-06-05T23:49:36.260Z
2013-06-05T23:54:59.700Z
2013-06-05T23:54:59.700Z
Ta Thanh Dinh
<p>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?</p>

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

CC BY-SA 3.0
2013-06-06T00:44:11.567Z
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
<denotational-semantics>
Meaning of program as solution of a recursive equation
sean
# Meaning of program as solution of a recursive equation

(Asked by: username_0 on 2013-06-05)

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.

**Tags:** denotational-semantics
> **Comments:**
> **username_1**: 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.  

---

## 2 answers

### Answer by username_2 on 2013-06-08. Score: 2 | Accepted answer

"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).

Coming back to your example:

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.

> **Comments:**
> **username_3**: "The program is a big formula" -- not a big _term_?  
> **username_2**: A big term is probably a better terminology. Thanks.  

---

### Answer by username_4 on 2013-06-05. Score: 0

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.


---

