I can't post yet, but if anyone is reading this, I have a comment about cactus's article about A Relational Model of Programming:

First of all, what does "red" mean, as in "alpha = red(alpha)"? It appears to be used to assert some kind of closure/fixpoint.

Secondly, it appears to me that A is a *state space* and A** the set of countable sequences of states, i.e. *traces*. Furthermore, in the definition of a *program*, it looks like the requirement is made that if a state is visited more than once, then it's visited infinitely many times. The way I interpret it, this seems to mean if the trace contains the sub-sequence "abcd...xyza", then the trace must be of the form "FSabcd...xyzabcd...xyzabcd..." where FS is a finite sequence of states. If we think of the trace as that of an evolving process, this sounds sort of like a memoryless property, i.e. no information other than the current state is used to choose the next state, but in this case, both the current state and the initial state are used (if my notion of infinite repitition is correct).

The above seems like the most natural interpretation to me as a computer scientist, but maybe you meant something else. Based on these assumptions, it seems clear that this program model is more powerful than a Turing machine. Consider your definition of p(S): a set of pairs (a, b) where a, b \in A. Fix some arbitrary b \in A. Now for any a \in A, we can construct a trace s.t. (a, b) \in p(S): simply let the sequence "ab" \in S (if a == b, let "a" \in S). Similarly, for any a \in A, we can construct another trace s.t. (a, b) \ni p(S): now let the sequence "aaa..." \in S (note that "aaa..." \ni A^*). Since your definitions don't specify any dependence between traces of S, this means that for each C \subseteq A, we can construct a program S[C] s.t. a \in C \iff p(S[C]) == b. Although A is countable, it immediately follows that the number of programs S[C] of this form is uncountable, and hence this relational model includes programs which cannot be described by a finite program or implemented in a Turing machine.

What to do about it? If you want to restrict your programs to those which are computable, you need more constraints on what it means for a relation to be a program. In particular, you either need more constraints on how states can be sequenced in a trace (much like the transition rules of a Turing machine) or some kind of constraints on what kinds of traces can appear together in the same program. If your goal is to construct a new Turing-equivalent model of computation, I think this second approach is more interesting, but I have no clue at this moment how to go about it.