2
$\begingroup$

Computing differs from math by its dependence on state changes, among other things. A program can be seen as a composition of state transitions, and it would be nice to have an inverse function to map a program text back to mathematics. You might also compare with transformations caused by changes of coordinate system. So:

How does one argue mathematically about equality of one expression's value in state $\sigma_{i+1}$ to another's in state $\sigma_i$, i.e. $\sigma_i(E)=\sigma_{i+1}(E')$, and relate it to properties of the state transition $\sigma_i\mapsto\sigma_{i+1}$?

Do not just refer to functional programming, because it circumvents the need to discuss state changes. I am familiar with it and have reasons to look for alternatives.

Specifically I would like to argue in terms of informal expressions like $f(S)(\sigma)(\lambda \nu.E)$ with $S$ varying over program expressions, $\sigma$ over states, and both $\nu$ and $E$ over expressions. Similar expressions are used for model-based semantics of programming languages, only with $\lambda \nu.E$ as a notation for an ordinary function (i.e. with $\nu$ varying over a domain of values).

The problem concerns arguing about an expression, rather than its interpretation 'in any state'. Is it appropriate to talk about functions with a domain of expressions? Differential and integral calculus concern expressions, but still presumes a fixed state. I am looking for a foundation for sound arguments when a current state changes, as in programming with assignments.

E.W. Dijkstra's transformation rules for a predicate valid in state $\sigma_{i+1}$ back to a predicate valid in state $\sigma_i$ is an attempt of the kind I'm looking for. His transformations depends on substitution of a program expression into a mathematical expression -- which is not generally acceptable.

Improve this question
$\endgroup$
5
  • $\begingroup$ Why must we not refer you to monads and the way functional programs carry around state? Isn't that a bit like saying "I'd like to solve this problem about symmetries, but please don't refer to group theory"? $\endgroup$
    – Andrej Bauer
    Commented Jan 21, 2012 at 20:08
  • $\begingroup$ Also, I don't understand what you'd like to do, the wording in the fourth and fifth paragraphs is confusing. I could write a general answer which lists three or four ways of dealing with stateful computations (monad being just one of them), but that would be a bit pointless. Can you give a very specific example of the thing you have in mind. Do you want state to appear explicitly in your expressions, or should it be "hidden under the carpet"? Do you want to argue in a model, or are you looking for valid inference rules that let you prove things about stateful computations? $\endgroup$
    – Andrej Bauer
    Commented Jan 21, 2012 at 20:14
  • $\begingroup$ The reference to Dijkstra's transformation rules indicates what I want to do. More explicitly I want to transform expressions in general, not just predicates. Also it 'hides states under the carpet' as I want. My interest is in programming language semantics and design. Model-based semantics strives to explain states, transformation-based strives to eliminate states. The latter potentially allows programs (including imperatives ones) to be transformed to pure mathematics. $\endgroup$
    – J Steensgaard
    Commented Jan 22, 2012 at 8:25
  • $\begingroup$ Please accept my reasons for asking the question, even if you disagree. I do not want this to evolve into a discussion about programming language design issues. Despite some familiarity with monads and the Haskell language, I am still of the opinion that alternatives should be explored. $\endgroup$
    – J Steensgaard
    Commented Jan 22, 2012 at 8:34
  • 1
    $\begingroup$ I am just trying to understand your question. A great deal is known on how to "transform programs to pure mathematics", what's wrong with the existing approaches? Are you familiar with them? The most obvious ones for state are the state monad, where a function $A \to B$ which also uses state $S$ is viewed as a function $S \times A \to S \times B$, or equivalently $A \to (S \times B)^S$, or the algebraic approach where operations on state are algebraic operations satisyfing certain equations(as in "universal algebra"). $\endgroup$
    – Andrej Bauer
    Commented Jan 22, 2012 at 9:57

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .