<p>Landin's SECD machine, originally described in <a href="http://comjnl.oxfordjournals.org/content/6/4/308.abstract">The mechanical evaluation of expressions</a> in 1964, is a transition system in the form of an abstract machine, later inspiring lots of of other abstract machines such as the CESK machine.</p>

CC BY-SA 3.0
2012-07-20T13:11:24.140Z
2012-07-20T13:11:24.140Z
Sam Tobin-Hochstadt
<ol>
<li><p>There's Amir Pnueli's 1977 <a href="http://www.cs.nyu.edu/pnueli/focs77.ps.gz"><em>The Temporal Logic of Programs</em></a>, where (as you doubtless know) the transition system is viewed as a Kripke frame. He cited the Keller paper you mention as his source of the idea that programs are transition systems. (I've never seen that one though.) </p></li>
<li><p>Christopher Strachey gave semantics to stateful programs as state transformers on domains (i.e., a command is a partial function $S \to S_\bot$). This has an obvious reading as a transition function. This semantics is described in his amazing 1967 lecture notes <a href="http://dx.doi.org/10.1023/A:1010000313106"><em>Fundamental Concepts in Programming Languages</em></a>. </p></li>
</ol>

CC BY-SA 3.0
2012-07-23T05:09:47.827Z
Thanks. I did know Pnueli's paper. Strachey's notes look promising.
Vijay D
CC BY-SA 3.0
2012-07-18T06:41:46.127Z
2012-07-18T06:41:46.127Z
Neel Krishnaswami
<p>If you enlarge the idea of "programs" to include Turing machines, then the original Turing's description of their semantics was as transition systems.  So, I think transition systems have always been with us!</p>

CC BY-SA 3.0
2012-07-26T20:41:18.653Z
Since biblical times?
Dave Clarke
CC BY-SA 3.0
2012-07-26T22:38:38.437Z
@Dave Clarke.  Well, I can't say.  Even though algorithms have always been written in an imperative style (long before biblical times!), they were designed for humans to execute with pencil and paper and, so, didn't involve genuine state change.  Turing seems to have been the first one.  I don't know if he realized how big a step he was taking by writing a new bit into a tape cell overwriting an old bit.  Perhaps he did!
Uday Reddy
CC BY-SA 3.0
2012-07-26T13:21:36.800Z
2012-07-26T13:21:36.800Z
Uday Reddy
<p>Go read Knuth, The Art of Computer Programming, where he gives definitions similar to what you mention.  It appears that he gives exactly one reference, namely to a book by A. A. Markov from 1951 called Theory of Algorithms.  This may or may not be what you want.  </p>

CC BY-SA 3.0
2012-07-27T09:24:11.853Z
2012-07-27T09:24:11.853Z
Zsbán Ambrus
<p>I am trying to trace back the origins of transition system semantics for imperative programs. I am assuming a transition system is a tuple $(\mathit{States}, \mathit{Trans})$ consisting of a set of states and a (binary) transition relation over states. By transition system semantics, I mean that there should be a mapping from programs to transition systems. </p>

<p>The presentation need not be exactly as I describe above and the mapping from programs to transition systems need not be completely explicit. For example, I would consider Plotkin's Structural Operational Semantics as providing transition system semantics to a formal language. Other early references I know of are due to Cousot &amp; Cousot, and even earlier, due to Robert Keller in <em>Formal Verification of Parallel Programs.</em> There is earlier work by Richard Karp and Raymond Miller on reasoning about parallel programs, but their model is closer to Petri Nets and I am unsure about whether to read their paper as giving transition system semantics to programs.</p>

<p>Does anyone know of references from the early 80s or earlier where transition system semantics are provided for programs? Please add a few lines about the semantics and whether it is used today, and in what form. </p>

<reference-request><pl.programming-languages><ho.history-overview><semantics>
Early References for Transition System Semantics of Programs
Vijay D
# Early References for Transition System Semantics of Programs

(Asked by: username_0 on 2012-07-18)

I am trying to trace back the origins of transition system semantics for imperative programs. I am assuming a transition system is a tuple $(\mathit{States}, \mathit{Trans})$ consisting of a set of states and a (binary) transition relation over states. By transition system semantics, I mean that there should be a mapping from programs to transition systems.

The presentation need not be exactly as I describe above and the mapping from programs to transition systems need not be completely explicit. For example, I would consider Plotkin's Structural Operational Semantics as providing transition system semantics to a formal language. Other early references I know of are due to Cousot & Cousot, and even earlier, due to Robert Keller in *Formal Verification of Parallel Programs.* There is earlier work by Richard Karp and Raymond Miller on reasoning about parallel programs, but their model is closer to Petri Nets and I am unsure about whether to read their paper as giving transition system semantics to programs.

Does anyone know of references from the early 80s or earlier where transition system semantics are provided for programs? Please add a few lines about the semantics and whether it is used today, and in what form.

**Tags:** reference-request, pl.programming-languages, ho.history-overview, semantics

---

## 4 answers

### Answer by username_1 on 2012-07-20. Score: 7

Landin's SECD machine, originally described in [The mechanical evaluation of expressions](http://comjnl.oxfordjournals.org/content/6/4/308.abstract) in 1964, is a transition system in the form of an abstract machine, later inspiring lots of of other abstract machines such as the CESK machine.


---

### Answer by username_2 on 2012-07-18. Score: 5

1. There's Amir Pnueli's 1977 [*The Temporal Logic of Programs*](http://www.cs.nyu.edu/pnueli/focs77.ps.gz), where (as you doubtless know) the transition system is viewed as a Kripke frame. He cited the Keller paper you mention as his source of the idea that programs are transition systems. (I've never seen that one though.)
2. Christopher Strachey gave semantics to stateful programs as state transformers on domains (i.e., a command is a partial function $S \to S\_\bot$). This has an obvious reading as a transition function. This semantics is described in his amazing 1967 lecture notes [*Fundamental Concepts in Programming Languages*](http://dx.doi.org/10.1023/A:1010000313106).

> **Comments:**
> **username_0**: Thanks. I did know Pnueli's paper. Strachey's notes look promising.  

---

### Answer by username_3 on 2012-07-26. Score: 4

If you enlarge the idea of "programs" to include Turing machines, then the original Turing's description of their semantics was as transition systems. So, I think transition systems have always been with us!

> **Comments:**
> **username_4**: Since biblical times?  
> **username_3**: @Dave Clarke.  Well, I can't say.  Even though algorithms have always been written in an imperative style (long before biblical times!), they were designed for humans to execute with pencil and paper and, so, didn't involve genuine state change.  Turing seems to have been the first one.  I don't know if he realized how big a step he was taking by writing a new bit into a tape cell overwriting an old bit.  Perhaps he did!  

---

### Answer by username_5 on 2012-07-27. Score: 1

Go read Knuth, The Art of Computer Programming, where he gives definitions similar to what you mention. It appears that he gives exactly one reference, namely to a book by A. A. Markov from 1951 called Theory of Algorithms. This may or may not be what you want.


---

