<p>You might want to take a look at the compiler literature for some ideas.  What you're describing is akin to a well-known compiler optimization (virtually any modern compiler worth its salt will do it) called constant folding.  Of course, constant folding goes further in not just identifying constant expressions, but replacing them by their value.</p>

<p>In particular, compilers use a dataflow analysis to identify such constant expressions.  Any good compiler textbook will discuss this.</p>

CC BY-SA 3.0
2011-10-11T18:58:59.737Z
This sounds promising, I am going to look into that. Thanks.
beroal
CC BY-SA 3.0
2011-10-10T11:07:02.737Z
2011-10-10T11:12:35.320Z
2011-10-10T11:12:35.320Z
Dominic Mulligan
<p>Rather than making a very precise analysis at the level of pixels, which is surely undecidable, you could design a program analysis that computes bounding boxes of either the set of pixels that <em>may</em> have changed or the set of pixels that <em>definitely</em> have not been changed. Then the given set of boxes (or their complement) are the ones that need to be redrawn. </p>

<p>There might be some work in <strong><a href="http://en.wikipedia.org/wiki/Abstract_interpretation" rel="nofollow">abstract interpretation</a></strong> that deals with this topic, but a quick google search didn't reveal anything.</p>

CC BY-SA 3.0
2011-10-11T18:46:39.187Z
I already do what you are suggesting. :) The phrase “may have changed” is neither precise nor formal, and the best way to formalize it I found is “constancy” (former “constantness”) (my English still needs improvement). $\text{“may have changed”}\leftrightarrow\lnot\text{“constant”}$. An output judgement/proposition can be interpreted in the Boolean algebra of subsets of $\mathbb{Z}\times\mathbb{Z}$. There is no difference whether we consider individual pixels or sets. So I dropped these considerations.
beroal
CC BY-SA 3.0
2011-10-11T18:47:12.977Z
BTW, the Boolean algebra of boxes (2D intervals) is also interesting though secondary task.
beroal
CC BY-SA 3.0
2011-10-11T18:59:25.357Z
Most static analyses are imprecise. They ask _may_ or _must_ questions, which would translate to "this pixel may have changed" or "this pixel must have changed", respectively. The point is that you can calculate an approximation of what has changed. There's plenty of formal work that addresses this topic.
Dave Clarke
CC BY-SA 3.0
2011-10-11T19:03:36.910Z
By “imprecise” I mean “has no formal definition.” Imprecise definitions do not belong to mathematics. And to cstheory.stackexchange.com. :)
beroal
CC BY-SA 3.0
2011-10-11T19:47:34.237Z
You are dismissing whole areas of computer science. Here's a paper on may and must testing: http://research.microsoft.com/pubs/78751/smash.pdf. There are plenty of others like it. All I'm suggesting is that you can apply these formal approaches to the problem you propose, because you are unlikely to find a precise and decidable algorithm to do what you want.
Dave Clarke
CC BY-SA 3.0
2011-10-11T20:13:27.507Z
“You are dismissing whole areas of computer science.” No.
beroal
CC BY-SA 3.0
2011-10-11T20:30:00.440Z
What I mean to say is that there are whole theories for dealing with the notion of "may have changed", so it is inaccurate to say that it is imprecise and does not belong in mathematics and on cstheory.stackexchange.com. Abstract interpretation is one unifying framework for such theories.
Dave Clarke
CC BY-SA 3.0
2011-10-10T12:24:02.613Z
2011-10-11T20:30:52.607Z
2011-10-11T20:30:52.607Z
Dave Clarke
<p>Let $S$ be a multisorted algebraic <a href="http://en.wikipedia.org/wiki/Signature_%28logic%29" rel="nofollow">signature</a> with function symbols $f_0, f_1, \ldots$. For every $i$, I partially know “constantness” of $f_i$. (I have no precise definition of constantness yet.) Examples:</p>

<ul>
<li>Let $\cdot$ denote multiplication of numbers. If $x_0=0$, then $x_0\cdot x_1$ is constant.</li>
<li>Conditional operation. If $x_0=0$ and $x_2$ is constant, then  $\operatorname{if}x_0\operatorname{then}x_1\operatorname{else}x_2$ is constant.</li>
</ul>

<p>I need to find a strongest constantness judgement for any term over $S$ given constantness of its variables. Is there an established way of reasoning about constantness?</p>

<p>A purpose is that every term in $S$ defines a function from program states to a pixel on a screen. Variables of the term are components of a state, i.e. the set of states is a Cartesian product. For every pixel $p$, if its term is found to be non-constant then I need to redraw $p$.</p>

<lo.logic><pl.programming-languages>
finding constantness of a term
beroal
# finding constantness of a term

(Asked by: username_0 on 2011-10-10)

Let $S$ be a multisorted algebraic [signature](http://en.wikipedia.org/wiki/Signature_%28logic%29) with function symbols $f\_0, f\_1, \ldots$. For every $i$, I partially know “constantness” of $f\_i$. (I have no precise definition of constantness yet.) Examples:

* Let $\cdot$ denote multiplication of numbers. If $x\_0=0$, then $x\_0\cdot x\_1$ is constant.
* Conditional operation. If $x\_0=0$ and $x\_2$ is constant, then $\operatorname{if}x\_0\operatorname{then}x\_1\operatorname{else}x\_2$ is constant.

I need to find a strongest constantness judgement for any term over $S$ given constantness of its variables. Is there an established way of reasoning about constantness?

A purpose is that every term in $S$ defines a function from program states to a pixel on a screen. Variables of the term are components of a state, i.e. the set of states is a Cartesian product. For every pixel $p$, if its term is found to be non-constant then I need to redraw $p$.

**Tags:** lo.logic, pl.programming-languages

---

## 2 answers

### Answer by username_1 on 2011-10-10. Score: 3

You might want to take a look at the compiler literature for some ideas. What you're describing is akin to a well-known compiler optimization (virtually any modern compiler worth its salt will do it) called constant folding. Of course, constant folding goes further in not just identifying constant expressions, but replacing them by their value.

In particular, compilers use a dataflow analysis to identify such constant expressions. Any good compiler textbook will discuss this.

> **Comments:**
> **username_0**: This sounds promising, I am going to look into that. Thanks.  

---

### Answer by username_2 on 2011-10-10. Score: 1

Rather than making a very precise analysis at the level of pixels, which is surely undecidable, you could design a program analysis that computes bounding boxes of either the set of pixels that *may* have changed or the set of pixels that *definitely* have not been changed. Then the given set of boxes (or their complement) are the ones that need to be redrawn.

There might be some work in **[abstract interpretation](http://en.wikipedia.org/wiki/Abstract_interpretation)** that deals with this topic, but a quick google search didn't reveal anything.

> **Comments:**
> **username_0**: I already do what you are suggesting. :) The phrase “may have changed” is neither precise nor formal, and the best way to formalize it I found is “constancy” (former “constantness”) (my English still needs improvement). $\text{“may have changed”}\leftrightarrow\lnot\text{“constant”}$. An output judgement/proposition can be interpreted in the Boolean algebra of subsets of $\mathbb{Z}\times\mathbb{Z}$. There is no difference whether we consider individual pixels or sets. So I dropped these considerations.  
> **username_0**: BTW, the Boolean algebra of boxes (2D intervals) is also interesting though secondary task.  
> **username_2**: Most static analyses are imprecise. They ask _may_ or _must_ questions, which would translate to "this pixel may have changed" or "this pixel must have changed", respectively. The point is that you can calculate an approximation of what has changed. There's plenty of formal work that addresses this topic.  
> **username_0**: By “imprecise” I mean “has no formal definition.” Imprecise definitions do not belong to mathematics. And to cstheory.stackexchange.com. :)  
> **username_2**: You are dismissing whole areas of computer science. Here's a paper on may and must testing: http://research.microsoft.com/pubs/78751/smash.pdf. There are plenty of others like it. All I'm suggesting is that you can apply these formal approaches to the problem you propose, because you are unlikely to find a precise and decidable algorithm to do what you want.  
> **username_0**: “You are dismissing whole areas of computer science.” No.  
> **username_2**: What I mean to say is that there are whole theories for dealing with the notion of "may have changed", so it is inaccurate to say that it is imprecise and does not belong in mathematics and on cstheory.stackexchange.com. Abstract interpretation is one unifying framework for such theories.  

---

