<p>There are many ways to define the semantics of a program. If we consider operational semantics, a simple imperative program defines a relation $R \subseteq \mathit{State}\times \mathit{State}$. I'm using "simple imperative" here to mean something that does not modify itself. There is a standard way to view $R$ as a function $\wp(\mathit{State}) \to \wp(\mathit{State})$ that maps a set of states to their successors in $R$.</p>

<p>If a program can modify itself you can consider a pair $\wp(\mathit{State})\times(\wp(\mathit{State})\to \wp(\mathit{State}))$, in which each element $(S,F)$ represents a current set of states in $S$ and a transformer $F$ representing the behaviour of the program. A program of the form you describe can modify either $S$ or $F$. </p>

<p>You may find the following paper useful.</p>

<blockquote>
  <p><a href="http://arxiv.org/abs/1003.5954" rel="nofollow">Multi-Stage Programs are Generalized Arrows</a>, Adam Megacz.</p>
</blockquote>

<p>If you are interested in a formalisation oriented towards automatic analysis of such programs, the following paper may interest you.</p>

<blockquote>
  <p><a href="http://www.cs.arizona.edu/~debray/Publications/metamorphic.pdf%E2%80%8E" rel="nofollow">Modelling Metamorphism by Abstract Interpretation</a>, Mila Dalla Preda, Roberto Giacobazzi, Saumya K. Debray, Kevin Coogan, Gregg M. Townsend</p>
</blockquote>

CC BY-SA 3.0
2013-06-07T17:46:16.947Z
Your answer is truly precious, though my initial goal (understanding what happens for a set of traces which is generated by a static structure) is different from the goals in these papers but the context is actually the same.
Ta Thanh Dinh
CC BY-SA 3.0
2013-06-04T01:59:01.907Z
2013-06-04T01:59:01.907Z
Vijay D
<p>Firstly, I admit that my question is just something very blurred but I hope someone please give me some documents to read.</p>

<p>The execution of a program $P$ can be considered as a sequence of state transitions $State \to State $ (this sequence should be finite if the program halts). By that way we get execution traces of program. Now, we may note that these traces (denoted as a set $T$) are generated by a static structure, that is the syntax of $P$. So we receive the <strong>first constraint</strong>: the set $T$ can not be arbitrary, instead <em>$T$ must be result of some static rewriting rules applied on the static syntax of program</em>.</p>

<p>Continue this way, if $P$ is a self-modifying program, roughly speaking $P$ can firstly generate other programs $Q_{1}, Q_{2}, \dotsc$, and these programs, at their turns, will generate other traces $T_{1},T_{2}, \dotsc$, so $T = T_{1} \cup T_{2} \cup \dotsc$. And we receive the <strong>second constraint</strong>: <em>the set $T$ must be result of some static rewriting rules applying on some static rewriting rules applying on the static syntax of programs</em>.</p>

<p>We can continue this construction to some level (may be there exists a limit ?). But a similar view I get is in the high order category theory where there exist morphisms between morphisms, and morphisms between morphisms between morphisms, etc.</p>

<p>So my question is: Do exist some reseaches on that or my thinking is just a stupid nonsense thing ?</p>

CC BY-SA 3.0
2013-06-03T22:38:21.297Z
What is actually the state of a program in your setting? From your definition, it seems to me that a state is the program source where variables are replaced with their corresponding values, i.e., state is a syntactic structure.
zpavlinovic
CC BY-SA 3.0
2013-06-03T22:45:59.200Z
In my thinking the program is stored in a memory space, and State is just value of this memory space.
Ta Thanh Dinh
CC BY-SA 3.0
2013-06-03T23:01:07.593Z
Maybe another equivalence view is to consider that at each step program will print out a value, and State is this value.
Ta Thanh Dinh
<pl.programming-languages><ct.category-theory>
Static structure of program
Ta Thanh Dinh
# Static structure of program

(Asked by: username_0 on 2013-06-03)

Firstly, I admit that my question is just something very blurred but I hope someone please give me some documents to read.

The execution of a program $P$ can be considered as a sequence of state transitions $State \to State $ (this sequence should be finite if the program halts). By that way we get execution traces of program. Now, we may note that these traces (denoted as a set $T$) are generated by a static structure, that is the syntax of $P$. So we receive the **first constraint**: the set $T$ can not be arbitrary, instead *$T$ must be result of some static rewriting rules applied on the static syntax of program*.

Continue this way, if $P$ is a self-modifying program, roughly speaking $P$ can firstly generate other programs $Q\_{1}, Q\_{2}, \dotsc$, and these programs, at their turns, will generate other traces $T\_{1},T\_{2}, \dotsc$, so $T = T\_{1} \cup T\_{2} \cup \dotsc$. And we receive the **second constraint**: *the set $T$ must be result of some static rewriting rules applying on some static rewriting rules applying on the static syntax of programs*.

We can continue this construction to some level (may be there exists a limit ?). But a similar view I get is in the high order category theory where there exist morphisms between morphisms, and morphisms between morphisms between morphisms, etc.

So my question is: Do exist some reseaches on that or my thinking is just a stupid nonsense thing ?

**Tags:** pl.programming-languages, ct.category-theory

> **Comments:**
> **username_1**: What is actually the state of a program in your setting? From your definition, it seems to me that a state is the program source where variables are replaced with their corresponding values, i.e., state is a syntactic structure.  
> **username_0**: In my thinking the program is stored in a memory space, and State is just value of this memory space.  
> **username_0**: Maybe another equivalence view is to consider that at each step program will print out a value, and State is this value.  

---

## 1 answers

### Answer by username_2 on 2013-06-04. Score: 3 | Accepted answer

There are many ways to define the semantics of a program. If we consider operational semantics, a simple imperative program defines a relation $R \subseteq \mathit{State}\times \mathit{State}$. I'm using "simple imperative" here to mean something that does not modify itself. There is a standard way to view $R$ as a function $\wp(\mathit{State}) \to \wp(\mathit{State})$ that maps a set of states to their successors in $R$.

If a program can modify itself you can consider a pair $\wp(\mathit{State})\times(\wp(\mathit{State})\to \wp(\mathit{State}))$, in which each element $(S,F)$ represents a current set of states in $S$ and a transformer $F$ representing the behaviour of the program. A program of the form you describe can modify either $S$ or $F$.

You may find the following paper useful.

> [Multi-Stage Programs are Generalized Arrows](http://arxiv.org/abs/1003.5954), Adam Megacz.

If you are interested in a formalisation oriented towards automatic analysis of such programs, the following paper may interest you.

> [Modelling Metamorphism by Abstract Interpretation](http://www.cs.arizona.edu/~debray/Publications/metamorphic.pdf%E2%80%8E), Mila Dalla Preda, Roberto Giacobazzi, Saumya K. Debray, Kevin Coogan, Gregg M. Townsend

> **Comments:**
> **username_0**: Your answer is truly precious, though my initial goal (understanding what happens for a set of traces which is generated by a static structure) is different from the goals in these papers but the context is actually the same.  

---

