4
$\begingroup$

Let $S$ be a multisorted algebraic signature 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$.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ This sounds promising, I am going to look into that. Thanks. $\endgroup$
    – beroal
    Oct 11, 2011 at 18:58
1
$\begingroup$

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 that deals with this topic, but a quick google search didn't reveal anything.

Improve this answer
$\endgroup$
7
  • $\begingroup$ 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. $\endgroup$
    – beroal
    Oct 11, 2011 at 18:46
  • $\begingroup$ BTW, the Boolean algebra of boxes (2D intervals) is also interesting though secondary task. $\endgroup$
    – beroal
    Oct 11, 2011 at 18:47
  • $\begingroup$ 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. $\endgroup$
    – Dave Clarke
    Oct 11, 2011 at 18:59
  • $\begingroup$ By “imprecise” I mean “has no formal definition.” Imprecise definitions do not belong to mathematics. And to cstheory.stackexchange.com. :) $\endgroup$
    – beroal
    Oct 11, 2011 at 19:03
  • $\begingroup$ You are dismissing whole areas of computer science. Here's a paper on may and must testing: 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. $\endgroup$
    – Dave Clarke
    Oct 11, 2011 at 19:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.