Timeline for How to argue about state transitions?
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 22, 2012 at 9:57 | comment | added | Andrej Bauer | 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"). | |
| Jan 22, 2012 at 8:34 | comment | added | J Steensgaard | 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. | |
| Jan 22, 2012 at 8:25 | comment | added | J Steensgaard | 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. | |
| Jan 21, 2012 at 20:14 | comment | added | Andrej Bauer | 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? | |
| Jan 21, 2012 at 20:08 | comment | added | Andrej Bauer | 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"? | |
| Jan 21, 2012 at 16:41 | history | asked | J Steensgaard | CC BY-SA 3.0 |