0
$\begingroup$

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 ?

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – bellpeace Jun 3 '13 at 22:38
  • $\begingroup$ In my thinking the program is stored in a memory space, and State is just value of this memory space. $\endgroup$ – Ta Thanh Dinh Jun 3 '13 at 22:45
  • $\begingroup$ Maybe another equivalence view is to consider that at each step program will print out a value, and State is this value. $\endgroup$ – Ta Thanh Dinh Jun 3 '13 at 23:01
3
$\begingroup$

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, 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, Mila Dalla Preda, Roberto Giacobazzi, Saumya K. Debray, Kevin Coogan, Gregg M. Townsend

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Ta Thanh Dinh Jun 7 '13 at 17:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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