If we have an interactive system (quadruple):
(S,Phi) : (Sigma S : Set)S -> Fam(Fam S),
where
Phi = \s->(C(s),\c->(R(s,c),\r->s[c/r])),
then we define two relations a <= s and s < a between states s : S and
countable ordinals a:
0 <= s == N1
(a+1) <= s == (Sigma c : C(s), Pi r : R(c,s)) a <= s[c/r]
(sup_n a_n) <= s == (Pi n : Nat) a_n <= s
0 > s == N0
(a+1) > s == (Pi c : C(s), Sigma r : R(c,s)) a > s[c/r]
(sup_n a_n) > s == (Sigma n : Nat) a_n > s
Intended meaning :
a <= s : the `interactive potential' of s can be at least a
s < a : the `interactive potential' of s can be bounded by a
(If `interactive potential' means anything .. !)
***************
Perhaps there is some (pseudo-)quantifiable notion of `potential
difference' between states? (The work done in getting from one to the
other.) If one thinks of the `work' as simulating a (high-level)
state sa using a (low-level) state sc, then it seems not unreasonable
that
Sim(sa,sc) = ( Pi c : C(sa), Sigma p : C^*(sc),
Pi t : R^*(sc,p), Sigma r : R(sa,c) )Sim(sa[c/r],sc[p/t])
where Sim(sa,sc) is the set of simulations of sa using sc, and `^*'
refers to the closure of the interactive system. (So p : C^*(sc) is a
`tree with leaves', t : R^*(sc,p) is a path to a leaf, and sc[t/p] is
the leaf state.)
Such a simulation has the form:
\c->(p(c),\t->(r(c,t),m(c,t)))
where m(c,t) : Sim(sa[c/r(c,t)],sc[p(c)/t])
There is a natural reflexive and transitive order between
simulations, which seems to capture the idea that one
simulation is at least as "efficient" as another:
(p,r,m) <= (p',r',m')
== (for all c : C(sa))
the tree p'(c) is a prefix of the tree p(c), and
(for all paths t : R^*(sc,p(c)))
m(c,t) <= m'(c,t'), where t' is the prefix of t in p'(c)
(The formal definition is quite long.)
Perhaps there is some way to `bound the complexity' of a simulation
(above and below) by an ordinal?