<p>This is question is related to <a href="https://cstheory.stackexchange.com/q/8354/44297">this</a> past question.</p>
<p>I am currently studying the textbook <a href="http://faculty.sist.shanghaitech.edu.cn/faculty/songfu/cav/PPA.pdf" rel="nofollow noreferrer"><em>Principles of Program Analysis</em> by Flemming Nielson, Hanne R. Nielson, and Chris Hankin</a>. Chapter <strong>1.4 Constraint Based Analysis</strong> says the following:</p>
<blockquote>
<p><strong>1.4 Constraint Based Analysis</strong>
The purpose of <em>Control Flow Analysis</em> is to determine information about what &quot;elementary blocks&quot; may lead to what other &quot;elementary blocks&quot;. This information is immediately available for the <span class="math-container">$\mathrm{While}$</span> language unlike what is the case for more advanced imperative, functional and object-oriented languages. Often Control Flow Analysis is expressed as a Constraint Based Analysis as will be illustrated in this section.<br />
Consider the following functional program:</p>
<pre><code>let f = fn x =&gt; x 1;
    g = fn y =&gt; y + 2;
    h = fn z =&gt; z + 3
in (f g) + (f h)
</code></pre>
<p>It defines a higher-order function <code>f</code> with formal parameter <code>x</code> and body <code>x 1</code>; then it defines two functions <code>g</code> and <code>h</code> that are given as actual parameters to <code>f</code> in the body of the <code>let</code>-construct. Semantically, <code>x</code> will be bound to each of these two functions in turn so both <code>g</code> and <code>h</code> will be applied to <code>1</code> and the result of the computation will be the value <span class="math-container">$7$</span>.<br />
An application of <code>f</code> will transfer control to the body of <code>f</code>, i.e. to <code>x 1</code>, and this application of <code>x</code> will transfer control to the body of <code>x</code>. The problem is that we cannot immediately point to the body of <code>x</code>: we need to know what parameters <code>f</code> will be called with. This is exactly the information that the Control Flow Analysis gives us:
<span class="math-container">$$\text{For each function application, which functions may be applied.}$$</span>
As is typical of functional languages, the labelling scheme used would seem to have a very different character than the one employed for imperative languages because the &quot;elementary blocks&quot; may be nested. We shall therefore label all subexpressions as in the following simple program that will be used to illustrate the analysis.
<strong>Example 1.2</strong> Consider the program:
<span class="math-container">$$[[ \text{fn} \ x =&gt; [x]^1]^2 [ \text{fn} \ y =&gt; [y]^3]^4]^5$$</span>
It calls the identity function <span class="math-container">$\text{fn} \ x =&gt; x$</span> on the argument <span class="math-container">$\text{fn} \ y =&gt; y$</span> and clearly evaluates to <span class="math-container">$\text{fn} \ y =&gt; y$</span> itself (omitting all <span class="math-container">$[ \dots ]^\mathscr{l}$</span>).</p>
</blockquote>
<p>I'm unsure about this part:</p>
<blockquote>
<p>It calls the identity function <span class="math-container">$\text{fn} \ x =&gt; x$</span> on the argument <span class="math-container">$\text{fn} \ y =&gt; y$</span> and clearly evaluates to <span class="math-container">$\text{fn} \ y =&gt; y$</span> itself (omitting all <span class="math-container">$[ \dots ]^\mathscr{l}$</span>).</p>
</blockquote>
<p>Looking at the program <span class="math-container">$[[ \text{fn} \ x =&gt; [x]^1]^2 [ \text{fn} \ y =&gt; [y]^3]^4]^5$</span>, aren't the statements <span class="math-container">$\text{fn} \ x =&gt; [x]^1$</span> and <span class="math-container">$\text{fn} \ y =&gt; [y]^3]$</span> executed separately, the former first and then leading to the latter? So what do the authors mean when they say that &quot;it calls the identity function <span class="math-container">$\text{fn} \ x =&gt; x$</span> on the argument <span class="math-container">$\text{fn} \ y =&gt; y$</span> and clearly evaluates to <span class="math-container">$\text{fn} \ y =&gt; y$</span> itself (omitting all <span class="math-container">$[ \dots ]^\mathscr{l}$</span>)&quot;, because this sounds like something different? Am I misunderstanding this?</p>
<hr />
<p>EDIT:</p>
<p>This chapter's <a href="http://www.imm.dtu.dk/%7Ehrni/PPA/slides1.pdf" rel="nofollow noreferrer">slides</a> from the textbook's website.</p>

CC BY-SA 4.0
2020-12-06T04:00:19.753Z
@D.W. I'll delete the one on cs.stackexchange, since someone asked a highly related question from the same textbook on cstheory in the past.
The Pointer
CC BY-SA 4.0
2020-12-06T09:54:41.147Z
This is a duplicate of https://cs.stackexchange.com/questions/132947/constraint-based-analysis-understanding-the-program-textfn-x-x1, please delete this instance as it is not research-level.
Andrej Bauer
CC BY-SA 4.0
2020-12-06T09:55:50.540Z
Ah ok, not quite a duplicate, but certainly this question does not belong here, because it is not research-level. It is about understanding how functional programs work.
Andrej Bauer
CC BY-SA 4.0
2020-12-06T15:25:45.243Z
Hi @AndrejBauer. Are you sure? I asked it here because I saw this https://cstheory.stackexchange.com/q/8354/44297 question, which is from the same section of the same textbook, so I thought that it would be appropriate.
The Pointer
CC BY-SA 4.0
2020-12-06T16:51:41.360Z
Yeah, I downvoted that one as well :-)
Andrej Bauer
CC BY-SA 4.0
2020-12-06T16:52:58.617Z
@AndrejBauer Oh, ok. My apologies. I will flag this to have it moved to cs.stackexchange. I also replied to your comment on the other (bountied) question.
The Pointer
<functional-programming><program-analysis>
$[[ \text{fn} \ x => [x]^1]^2 [ \text{fn} \ y => [y]^3]^4]^5$ calls the identity function $\text{fn} \ x => x$ on the argument $\text{fn} \ y => y$?
The Pointer
# $[[ \text{fn} \ x => [x]^1]^2 [ \text{fn} \ y => [y]^3]^4]^5$ calls the identity function $\text{fn} \ x => x$ on the argument $\text{fn} \ y => y$?

(Asked by: username_0 on 2020-12-05)

This is question is related to this past question.
I am currently studying the textbook Principles of Program Analysis by Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Chapter 1.4 Constraint Based Analysis says the following:

1.4 Constraint Based Analysis
The purpose of Control Flow Analysis is to determine information about what "elementary blocks" may lead to what other "elementary blocks". This information is immediately available for the $\mathrm{While}$ language unlike what is the case for more advanced imperative, functional and object-oriented languages. Often Control Flow Analysis is expressed as a Constraint Based Analysis as will be illustrated in this section.
Consider the following functional program:
let f = fn x => x 1;
    g = fn y => y + 2;
    h = fn z => z + 3
in (f g) + (f h)

It defines a higher-order function f with formal parameter x and body x 1; then it defines two functions g and h that are given as actual parameters to f in the body of the let-construct. Semantically, x will be bound to each of these two functions in turn so both g and h will be applied to 1 and the result of the computation will be the value $7$.
An application of f will transfer control to the body of f, i.e. to x 1, and this application of x will transfer control to the body of x. The problem is that we cannot immediately point to the body of x: we need to know what parameters f will be called with. This is exactly the information that the Control Flow Analysis gives us:
$$\text{For each function application, which functions may be applied.}$$
As is typical of functional languages, the labelling scheme used would seem to have a very different character than the one employed for imperative languages because the "elementary blocks" may be nested. We shall therefore label all subexpressions as in the following simple program that will be used to illustrate the analysis.
Example 1.2 Consider the program:
$$[[ \text{fn} \ x => [x]^1]^2 [ \text{fn} \ y => [y]^3]^4]^5$$
It calls the identity function $\text{fn} \ x => x$ on the argument $\text{fn} \ y => y$ and clearly evaluates to $\text{fn} \ y => y$ itself (omitting all $[ \dots ]^\mathscr{l}$).

I'm unsure about this part:

It calls the identity function $\text{fn} \ x => x$ on the argument $\text{fn} \ y => y$ and clearly evaluates to $\text{fn} \ y => y$ itself (omitting all $[ \dots ]^\mathscr{l}$).

Looking at the program $[[ \text{fn} \ x => [x]^1]^2 [ \text{fn} \ y => [y]^3]^4]^5$, aren't the statements $\text{fn} \ x => [x]^1$ and $\text{fn} \ y => [y]^3]$ executed separately, the former first and then leading to the latter? So what do the authors mean when they say that "it calls the identity function $\text{fn} \ x => x$ on the argument $\text{fn} \ y => y$ and clearly evaluates to $\text{fn} \ y => y$ itself (omitting all $[ \dots ]^\mathscr{l}$)", because this sounds like something different? Am I misunderstanding this?

EDIT:
This chapter's slides from the textbook's website.

**Tags:** functional-programming, program-analysis

> **Comments:**
> **username_0**: @D.W. I'll delete the one on cs.stackexchange, since someone asked a highly related question from the same textbook on cstheory in the past.  
> **username_1**: This is a duplicate of https://cs.stackexchange.com/questions/132947/constraint-based-analysis-understanding-the-program-textfn-x-x1, please delete this instance as it is not research-level.  
> **username_1**: Ah ok, not quite a duplicate, but certainly this question does not belong here, because it is not research-level. It is about understanding how functional programs work.  
> **username_0**: Hi @AndrejBauer. Are you sure? I asked it here because I saw this https://cstheory.stackexchange.com/q/8354/44297 question, which is from the same section of the same textbook, so I thought that it would be appropriate.  
> **username_1**: Yeah, I downvoted that one as well :-)  
> **username_0**: @AndrejBauer Oh, ok. My apologies. I will flag this to have it moved to cs.stackexchange. I also replied to your comment on the other (bountied) question.  

---

## 0 answers

