9512.net
甜梦文库
当前位置:首页 >> >>

Symmetries and transitions of bounded Turing machines


arXiv:cs/9812019v1 [cs.LO] 16 Dec 1998

Symmetries and transitions of bounded Turing machines
Peter Hines January 15, 2008
Abstract We consider the structures given by repeatedly generalising the de?nition of ?nite state automata by symmetry considerations, and constructing analogues of the transition monoid at each step. This approach ?rst gives us non-deterministic automata, then (non-deterministic) two-way automata and bounded Turing machines — that is, Turing machines where the read / write head is unable to move past the end of the input word. In the case of two-way automata, the transition monoids generalise to endomorphism monoids in compact closed categories. These use Girard’s resolution formula (from the Geometry of Interaction representation of linear logic) to construct the images of singleton words. In the case of bounded Turing machines, the transition homomorphism generalises to a monoid homomorphism from N to a monoid constructed from the union of endomorphism monoids of a compact closed category, together with an appropriate composition. These use Girard’s execution formula (also from the Geometry of Interaction representation of linear logic) to construct images of singletons. AMS Classi?cation: 68Q05, 86Q70, 18D15

1

Introduction

In what follows, we take one of the simplest possible de?nitions in the theory of computation — that of a deterministic ?nite state automaton without speci?ed initial or terminal states — and repeatedly generalise the de?nition by symmetry considerations. Each successive generalisation leads to a more complicated structure, albeit already known, if not widely studied. However, the way in which the algebraic models follow the generalisations is of more interest. This procedure allows us to form algebraic models of each of the structures under consideration, which appear to be, in each case, important tools in answering questions about these structures. It is also of interest to note that the

1

algebraic structures used are similar both to those used by theoretical physicists in their algebraic models of symmetries, and those used by logicians for representing the process of deduction.

2

Generalising ?nite state automata

We take as the starting point of our generalisation process the idea of a ?nite set of functions from a ?nite set to itself — that is, we consider a set Q, and a set of functions Σ from Q to Q. Algebraic models arise when we consider multiple function applications, hgf (a) = hg (b) = h(c) = d. We wish keep a track of this process, so we draw the above as hgf (a) → hg (b) f → h(c) gf →
(d )

hgf.

Note that when we draw it this way, we do not forget the function we have just applied. This is because, intuitively, we consider forgetting information to be a computational step. Consider the following graphical representation of the action of the functions {f, g } on the set {a, b, c}
f f g

'& %$o !a "# @A

GFED BC / o '&%$ !"# !"# c b f,g '&%$ BCO
g

Using a graphical representation, the action of string of function symbols can be thought of as ‘following a labelled path through a diagram’. This is, of course, a ?nite state automaton; we refer the reader to [15] for the basic theory. The set Σ is the input alphabet, and the set Q is the set of states. As the name suggests, these are both ?nite. There is also a next state function, ? : Σ × Q → Q which we have been representing by function application. In [7], the following model is given: The set of all words of Σ form a monoid, with composition given by concatenation of strings, and the identity element given by the empty word, λ. This monoid is denoted Σ? . Similarly, the set of all functions on Q, denoted P T (Q), is also a monoid. Formally, we identify a function f : Q → Q with the subset of Q × Q given by {(f (q ), q ) : q ∈ Q}. The composition of this monoid is given by: (c, a) is a member of SR if and only if there exists some b with (c, b) a member of S and (b, a) a member of R; it is immediate that this composition is associative, and the identity of P T (Q) is the diagonal relation I = {(q, q ) : q ∈ Q}. The transition function t : Σ? → P T (Q) is de?ned as follows: Let w be a string of function symbols from Σ. Then the pair (b, a) is a member of t(w) if and only if w(a) = b. From the computational interpretation of the function t, it is clear that t(u)t(v ) = t(uv ) and t(λ) = I . Hence t is a monoid homomorphism. This, together with the fact that we know t(f ) for all f in Σ allows us to describe t(w) for any w in Σ? . This then allows a characterisation of the words of Σ? 2

(i.e. composites of functions) that have the same action on the set Q. Hence we can identify words over the input alphabet to form a ?nite quotient of Σ? , called the transition monoid. The homomorphism t uniquely determines, and is uniquely determined by the transitions of the ?nite state automaton. Also, every monoid homomorphism from a ?nitely generated free monoid to a monoid of functions on a set determines a ?nite state automaton.

2.1

Generalising to non-deterministic automata
f,g

Consider the following transition diagram,

GF @AED '& %$o !a "#

f,g

'&%$ !"# b . As the ?rst step

in our ‘generalising by symmetry’ process, we would like to have an operation that reversed all the arrows in this transition diagram, to de?ne another ?nite '& %$ /'&%$ ! "# !"# a b state automaton, which would be speci?ed by . However, as @A GFBCO f,g
f,g

it stands, this is not a ?nite state automaton. We required Σ to be a set of functions, and in the second diagram f (a) can be either a or b, and g (b) is not de?ned. We replace the requirement that members of Σ de?ne functions on the set Q with the more general requirement that they de?ne relations on Q — that is, they are arbitrary sets of pairs of elements of Q (an alternative, but equivalent, requirement is that members of Σ de?ne functions from Q to the set of all subsets of Q, denoted P (Q) ). This is the generalisation from deterministic automata to non-deterministic automata. With a deterministic automaton, there is exactly one next state, for any x ∈ Σ and q ∈ Q. With a non-deterministic automaton, there is a set of next states (which may be empty). We replace the next state function ? : Σ × Q → Q by the next-set-of-states function ? : Σ × Q → P (Q), where P (Q) denotes the set of all subsets of Q. We can de?ne the transition homomorphism, as before; the transition homomorphism for a non-deterministic automaton is given by a homomorphism from Σ? to B (Q), the monoid of relations on Q. Note that every monoid homomorphism from a ?nitely generated free monoid to a ?nite monoid of relations uniquely determines a (non-deterministic) ?nite state automaton. The mathematical representation of the ‘reversing arrows’ symmetry is an operation de?ned on monoids of relations, given by R → R, where (a, b) is in R if and only if (b, a) is in R. Now consider the relation t(x) for some x ∈ Σ. The pair (b, a) is in t(x) if there is an arrow from state a to state b labelled by x, and the connection between the ‘reversing arrows’ operation, and the symmetry ( ) is then apparent.

3

Generalising to two-way automata

Recall that we drew transitions of a ?nite state automaton as a pointer labelled by a state moving from left to right over a string of symbols. This convention

3

was chosen because we were writing function application on the left, which is in turn due to the Arabic basis of our number system. We would like to eliminate the asymmetry given by the arbitrary choice of direction; that is, we would also like to be able to consider transitions of the form (d) hgf → h(c) gf → hg (b) f → hgf (a) , so that in terms of a pointer moving over words, the direction of movement is reversed. Consider a (non-deterministic) automaton A with state set Q, input alphabet Σ, and next state function ?l : Σ × Q → P (Q). We eliminate the directional asymmetry by introducing a right-moving next state function ?r : Q × Σ → P (Q). The interpretation of this is that the pointer labelled by a state may move either left or right on a word (or both — we allow for the possibility of non-determinism), and change state accordingly. So, the evolution of the system under time proceeds as follows: Consider a point in a computational process, . . . xi?2 xi?1 (a) xi xi+1 . . . The set of next con?gurations is the union of . . . xi?2 (b) xi?1 xi . . . where b is in xi?1 ?l a and . . . xi?1 xi (c) xi+1 . . . where c is in a ?r xi . This structure is a two-way automaton. It is not described in the same way as the usual model, due to J.-C. Birget (see [5]); he labels the states as either left-moving, or right-moving (or both; the sets of left and right moving states are not assumed to be disjoint) and has a single next-state function. The movement of the pointer is then to the left or the right, depending on whether the current state is left or right moving. The two di?erent descriptions are not quite the same; consider the computa′ ′′ tions (q) x → x(q ) and x(q) → (q ) x. In Birget’s model, q ′ must be the same as q ′′ . Using our model, they may di?er. However, they can be seen to be equivalent; our model clearly contains Birget’s model as a special case (the left and right moving state sets are the domains of ?l and ?r respectively). Conversely, consider a model de?ned in our terms, together with a state q that is both left and right moving. We can then ‘split q into 2 parts’, ql and qr , and adjust the next state functions accordingly. Then Birget’s single next state function is de?ned to be the union of our left moving and right moving next state functions (This construction is used in a ‘non-determinism is (almost) equivalent to determinism’ proof of J.-C. Birget for two-way automata [4], and a full proof of the equivalence of the above model with his can be found in [14]). To generalise the transition homomorphism t, we need to know when a computation is ?nished. In the one-way case it was immediate; a computation is ?nished when it reaches the left of the word of symbols from Σ. In the two-way case, there are four possibilities, depending on whether the pointer starts on the left or the right, and whether it ?nishes on the left or the right. Using this basic idea, J.C. Birget constructs algebraic models of two-way automata. For every word of the input alphabet, he de?nes four relations on Q: ? [? ? w], consisting of the set of pairs (q ′ , q ) for which there exists a compu′ tation starting in con?guration (q) w and ?nishing in con?guration (q ) w, with q rightmoving, and q ′ leftmoving. ? [?w →], consisting of the set of pairs (q ′ , q ) for which there exists a com4

putation starting in con?guration (q) w and ?nishing in con?guration w(q ) , with q and q ′ rightmoving. ? [← w?], consisting of the set of pairs (q ′ , q ) for which there exists a com′ putation starting in con?guration w(q) and ?nishing in con?guration (q ) w, with q and q ′ leftmoving. ? [w ? ?], consisting of the set of pairs (q ′ , q ) for which there exists a compu′ tation starting in con?guration w(q) and ?nishing in con?guration w(q ) , with q left-moving and q ′ rightmoving. These relations, which he calls global transition relations, also feature implicitly in the earlier work, ‘[25], by J. Shepardson. The point of J.-C. Birget’s de?nitions is that, for any two words of Σ? , the global transition relation of their composite can be written in terms of their global transition relations, and composition in the monoid of relations. This is as follows: Theorem 1 Given a two-way automaton A = (Q = Ql ∪ Qr , Σ, ?), and u, v ∈ Σ? , then the global transition relations of the composite uv are de?ned in terms of the global transition relations of u and v , as follows: ? [?uv →] = [?v →]([u ? ? v ])? [?u →], ?][? ? [uv ? ?])? [← v ?], ? v ][u ? ?]([? ?] ∪ [?v →][u ? ?] = [v ? ? [? ? v ])? [?u →], ?][? ? v ]([u ? ? u] ∪ [← u?][? ? uv ] = [? ? [← uv ?] = [← u?]([? ?])? [← v ?]. ? v ][u ? Where, for a relation R, its Kleene star is de?ned by R? = I ∪ R ∪ R2 ∪ R3 ∪ . . . 2 The algebraic framework for these composition rules is a special case of a construction of Joyal, Street, and Verity, [20], which they refer to as the Int construction1 In this construction, the category Rel, that has all sets as objects and relations between sets as arrows (so that the endomorphism monoid of an object X is the monoid B (X ) of relations), is ‘dualised’ to form a category IntRel. This category has pairs of sets as objects. An arrow between two objects, say (X, U ) and (Y, V ), consists of four arrows in the category of relations, as follows: X
a c



/U O
d

 Y o
1 Although

b

V

we follow the examples and notation of Joyal, Street and Verity (because they give the example of the category of relations as a special case), the Int construction was ?rst presented (in a di?erent manner) in terms of logical models, in Abramsky and Jagadeesan’s ‘New Foundations for the Geometry of Interaction’ [2]. The equivalence of the two constructions, together with the intuitive ideas behind the categorical construction - including the close connection with iteration - appeared in Abramsky’s ‘Retracing some paths in process algebra’ [1].

5

Composition of relations is then giving by a ‘taking the union over all possible paths’ construction. Two squares, as above, are composed vertically, and the union over all possible paths between bottom and top is constructed, as follows: X
c

/U O
d

a b

X

c∪d(gb)? ga

/U O
d(gb)? h

GF Y @A
g e

ED V BCO
h

becomes

e(bg)? a

 Zo

f ∪e(bg)? bh

W

 Zo

f

W

This can also be written more concisely in matrix form as e g f h a c b d = e(bg )? a f ∪ e(bg )? bh ? c ∪ d(gb) ga d(gb)? h

This then gives context for Birget’s equations for two-way automata. De?ne a function [ ] from the set of words on the input alphabet, Σ? , to the endomorphism monoid of (Q, Q) in IntRel, by [w] = [← w?] [w ? ?] [? ? w] [?w →]

Theorem 2 The composition of [v ] and [u] in IntRel is given by Birget’s equations, so [vu] = [v ][u]. Proof This follows immediately by comparing the composition of IntRel with Birget’s equations. 2 The above construction shows that the map [ ] is a semigroup homomorphism - it is not a monoid homomorphism; the empty word λ is mapped to the idempotent 0 1Ql . This makes the image of Σ? under [ ] what [17] refers to as a 0 1Qr local submonoid of the endomorphism monoid of (Q, Q). Unlike the one-way case, the value of [ ] for words of length 1 (that is, members of Σ) is not immediate from the de?nition. These can be found using a tool developed by J.-Y. Girard for linear logic, in [11].

6

3.1

Girard’s resolution formula, and two-way automata

In [11, 12, 13], J.-Y. Girard constructed a novel series of representations of linear logic (see [10] for an introduction to this logical system), called the Geometry of Interaction. This representation was in terms of matrices over monoids of relations. A common feature of all these was the resolution formula. This was de?ned in terms of matrices of relations (where, in the composition of matrices of relations, multiplication is interpreted by monoid composition, and addition is interpreted by union), to be Res(U, σ ) = πU (1 ? σU )?1 π = πU (σU )? π, where π is an idempotent given by a {(a, a) : a ∈ A}, for some A ? N. The matrix of relations σ was also assumed to be (in the simplest case) the anti0 1 diagonal matrix , where 1 and 0 are, respectively, the identity and 1 0 nowhere-de?ned relations on B (N). The connection of this formula with the theory of two-way automata is then as follows: Theorem 3 Let A = (Q, Σ, ?l , ?r ) be a two-way automaton, and consider x ∈ Σ. De?ne Ql = dom(?l ) , Qr = dom(?r ) , j = tl (x) , k = tr (x) where tl and tr are the transition homomorphisms for (Q, Σ, ?l ) and (Q Σ, ?r ) respectively. A matrix consisting of the global transition relations of x is given by the following version of Girard’s resolution formula over the monoid of relations on Q : Res(U, σ ) = 1Ql 0 0 1Qr k 0 0 j 0 1 1 0 k 0 0 j
?

1Ql 0

0 1Qr

Proof First note that a direct calculation will give Res(U, σ ) = 1Ql k (jk )? 1Ql 1Qr (jk )(jk )? 1Ql 1Ql (kj )(kj )? 1Qr 1Qr j (kj )? 1Qr .

Conversely, the transitions of a two-way automaton on the symbol x can be represented as follows:
j =tr (x)

(q )

GF x O@A
k=tl (x)

ED ′ x(q ) BC

All possible transitions from con?gurations of the form (q) x to con?gurations of ′ the form (q ) x are given by kj , (kj )2 , (kj )3 , . . . Hence, [? ? x] is the intersection of (kj )(kj )? with Ql × Qr , and so [? ? x] = 1Ql (kj )(kj )? 1Qr . This is the top right entry of Res(U, σ ), as required. Similar considerations will give the other three global transition relations, [← x?], [x ? ?], and [?x →] as the top left, bottom left, and bottom right entries respectively. 2

7

3.2

Interpretation of the ‘reversing directions’ symmetry

The category IntRel is a compact closed category — the point of the Int operator is a canonical construction of compact closed categories. These are special cases of symmetric monoidal categories (we refer to [23] for the theory of symmetric monoidal categories, and their coherence equations), where for every object A, there exists another object A∨ , called its (left) dual, satisfying: there exists an arrow from I to A ? A∨ , and an arrow from A∨ ? A to I (together with natural coherence conditions which were mathematically analysed in [21].)2 These de?nitions imply the existence of duals on arrows, so that, for any arrow f : A → B , there exists its dual f ∨ : B ∨ → A∨ . In the category IntRel, the dual on objects is (X, U )∨ = (U, X ) and the dual on arrows is given by a c b d


=

d b

c a

The dual on arrows of this category then has the simple interpretation of interchanging the left and the right moving parts of a two-way automaton (i.e. taking ?r as the left-moving next state function, and dually for ?r ). Hence, if [w] is the global transition relation of w for the automaton A, then [w]∨ is the global transition relation of w for the automaton given by swapping the left and right moving parts of A.

3.3

Summary of algebraic models of two-way automata

It is worthwhile just to summarise the di?erences between algebraic models of one-way and two-way automata. They are both functions from the set of all words on the input alphabet; in the one-way case, a monoid homomorphism to the monoid of relations on the set of states Q and in the two-way case, a homomorphism to the endomorphism monoid of (Q, Q) in the compact closed category IntRel. What allows us to calculate them explicitly is that we know values for members of Σ; in the one-way case, these are immediate from the de?nition, and in the two-way case, these are given by Girard’s Resolution formula. Note that a one-way (non-deterministic) automaton is uniquely speci?ed by a monoid homomorphism, as above. However, a two-way automaton is not uniquely speci?ed by such a homomorphism; the images of members of Σ are of a very special form. The de?nition of a one-way automaton has one symmetry, given by reversing the direction of arrows in a transition diagram. The mathematical representation of this is the ( ) operation in the category of relations. The de?nition of a two-way automaton also has the symmetry given by reversing the direction of movement. The mathematical representation of this is the dual operator in a compact closed category. The ‘reversing arrows’ operation on the category of
2 As could be deduced from this very suggestive notation, compact closed categories have been heavily used in theoretical physics — see [3] for more details.

8

relations generalises directly (by the Int construction) to the compact closed category IntRel. This makes IntRel what J. Baez refers to as a ‘compact closed category with duality’; see [3] for more details.

4

Generalising to bounded Turing machines

The next observation that allows us to continue our generalisation process is that in the de?nition of a ?nite state automaton, the set of states has a distinguished r? ole. Given a state and a symbol, we have a function that gives us another state. So, what we require in order to make this de?nition symmetric with respect to states and alphabets is another function (or two new functions in the two-way case) that takes a state and a symbol, and gives us a new symbol. We ?rst consider how this generalises the de?nition of one-way ?nite state automata, and then extend to the two-way case.

4.1

Generalising one-way automata to Mealy machines

Given a (non-deterministic) automaton A = (Q, Σ, ? : Σ × Q → P (Q)), we wish to make this de?nition symmetrical between the state set, and the input alphabet. To do this, we introduce the output function ? : Σ × Q → P (Σ). The interpretation is that each state change has an output associated with it, so an input word of length n will give a set of output words of length n. Consider the following example, with state set {n, c} and alphabet {0, 1}, where ? and
0 1 1 0 n c n c

@AED ? are speci?ed by GF %$o /'& !n "#

BC and GF @AED GFED / !"#o '&%$ /'&%$ !"# c 0o

GFED BC respectively. The / o '&%$ !"# 1

computation of R on the input 101101 starting in state n is then 1 1 1 1 1 1
(c )

0 0 0 0 0
(n)

1 1 1 1
(c )

1 1 1
(c )

0 0
(n)

1
(c )

(n)

1

0 0

1 1 1

1 1 1 1

0 0 0 0 0

1 1 1 1 1 1

output:0 output:1 output:0 output:1 output:1 output:0

This gives the output word 011010, and ends in state c. As can be seen from this example, the action of this machine is to left-shift a binary string (i.e. multiply by two), and record if there is over?ow (where c =‘carry bit set’ and n =‘no carry’). Note that the above pair of transition diagrams de?ne two ‘automata with output’, one with state set Q and input/output alphabet Σ, and the other with state set Σ, and input/output alphabet Q. In fact, the above example is equivalent to itself under this symmetry. Automata with output are know as Mealy Machines, or Mealy-type automata (see [7] for the general theory, and the related Moore machines, which are au9

tomata with output, where every state has an associated output, rather than every transition). The examples we have been considering above are the special cases where the input alphabet is the same as the output alphabet.

4.2

Generalising two-way automata to bounded Turing machines

In the above sections, we took a model of applying ?nite functions to a ?nite set and considered in which ways the de?nition was asymmetric. We ?rst generalised to non-determinism by requiring that a ‘reversing arrows’ operation be well-de?ned, and then demonstrated how we could either generalise to two-way automata (by left / right movement symmetry), or to Mealy machines (by state / alphabet symmetry). We now wish to generalise by both at the same time, to get a model of a computing device that can move left and right, and overwrite its input as it goes. This will give us a model of computation which we refer to as a bounded Turing machine, which is a Turing machine where the read/write head is unable to move over the end-marker of the tape. In the following section, we use a signi?cantly di?erent model of Turing machines to the usual, as found in, for example [7]. The main di?erence is that we require the pointer to be positioned between cells on a tape, rather than pointing at a cell on a tape, as is usual (see [7] for an explanation of the usual description). However, our description follows inevitably from the generalisation process, and we feel justi?ed in this approach, because the resulting model is algebraically tractable. De?nition We de?ne (our model of) a bounded Turing machine to be speci?ed by ? a state set, ? Q, a set of symbols Σ, ? two next state functions, ?l : Σ × Q → P (Q) and ?r : Q × Σ → P (Q) that specify the left and right moving state changes, ? two rewrite functions, ?l : Σ × Q → P (Σ) and ?r : Q × Σ → P (Σ), that specify the left and right moving rewrites. The action of this machine is as follows: Consider a point in a computational process (a con?guration, or instantaneous description), . . . xi?2 xi?1 (a) xi xi+1 . . . Then the set of next possible con?gurations is the union of all con?gurations of the form . . . xi?2
(b)

yxi . . . where b ∈ xi?1 ?l a , y ∈ xi?1 ?l a 10

and all con?gurations of the form . . . xi?2 xi?1 z
(c )

xi+1 . . . where c ∈ a ?r xi , z ∈ a ?r xi

4.3

Algebraic models of bounded Turing machines

We now construct algebraic models of the computations of bounded Turing machines. We cannot directly copy Birget’s formul? in an attempt to construct algebraic models of bounded Turing machines - it makes no sense to write a composite like [w ? ?][← w?] in the context of bounded Turing machines; once the pointer has passed over the word w (that is the [← w?] part), then another word has been written on the tape, so we cannot consider [? ? w] as a next step of the computation. Another, less serious, objection to copying Birget’s model directly is the restriction of members of global transition relations to left-moving or rightmoving states (recall that [← w?] was de?ned to be the set of pairs (b, a) satisfying a computational condition, subject to the restriction that a and b were both left-moving). This is because, in our formalisation, it is the next state function that is split into two, rather than the set of states. Because of the above points, we pair words and states, and consider relations consisting of them, as follows: De?nition For a bounded Turing machine T, and a natural number n, we de?ne ← n? to be the relation on Σn × Q given by ← n? = b v , a u

where there exists a computation of T starting in con?guration ua , and leading to con?guration b v , where words u and, by implication, v are of length n. We make the dual de?nition for ?n → . We also require the other two possibilities: we de?ne ? ?n = b v , a u

where exists a computation of T starting in con?guration a u, and leading to con?guration b v ’, where words u and v are again of length n. Of course, we make the dual de?nition for n ? ?. We call these the computation relations for the bounded Turing machine T. Note that these relations give, for a bounded Turing machine T and a ?xed tape length n, all possible computations of T that start and end at a boundary of the tape. What is then required is a description of how algebraically tractable these objects are. The ?rst point is that we can write the computation relations in terms of themselves. This is not as trivial as it ?rst appears; consider the following: 11

Proposition 4 Let T be a bounded Turing machine with state set Q and alphabet Σ. Then the computation relations for words of length n satisfy the following: ? ← n? = ? ? ? n ← n? ( ?n → ← n? )? n ? ? ?n → = ? ? ? n ?n → ( ← n? ?n → )? n ? ? ? ?n ? n ( ← n? ?n → )? ? ?n = ? ? n? ? ? ( ?n → ← n? )? n ? ? = n? Proof Consider q′ v , q u ∈ ← n? , q ′′ w , q′ v ∈ n? ?

By de?nition of compostion in the category of relations, q ′′ w , q u ∈ n? ? ← n?

However, by de?nition of ← n? as the set of all right to left computations, q ′′ w , q u ∈ ← n?

Hence ← n? n ? ? ? ← n? . However, as we are not restricting by leftmoving or right-moving states, the identity relation I is contained in n ? ?. Therefore, we can also write ← n? n ? ? = ← n? Similar reasoning applies to right to left and left to right computations, so that ← n? ? ( ?n → ← n? )? and as the identity relation is a member of R? for any relation R, ← n? = ← n? ( ?n → ← n? )? . Finally, dual reasoning to the ?rst identity will give us ← n? = ? ? n ← n? . Putting these together will give us the identity ← n? = ? ?. ? n ← n? ( ?n → ← n? )? n ? The symmetry of the bounded Turing machine with respect to left / right movement will then give us the dual of this for free, so that ?n → = ? ? n ?n → ( ← n? ?n → )? n ? ? . This gives us the left to right and the right to left movements in terms of themselves and the other computation relations. It can then be shown by similar methods that ? ?n = ? ? n ( ← n? ? n → ? ? ) ? n , and duality with respect to left / right movement gives us n ? ? = n? ? . This then completes our proof. 2 ? ( ?n → ← n? )? n ?

12

De?nition As in the two-way automaton case, we can use these four computation relations to construct a member of the endomorphism monoid of (Q × Σn , Q × Σn ) in IntRel as follows: Q × Σn n =
←n? ? ?n

/ Q × Σn O
?n→

 Q × Σn o

n? ?

Q × Σn

We also make the formal de?nition that 0 is the identity at (Q × {λ}, Q × {λ}). We refer to n as the computation relation of the machine T on words of length n. As expected, we can write Theorem 4 as another ‘summing over all paths’ construction; this demonstrates a symmetry in the the de?nition of IntRel. In the de?nition of the composition of the endomorphism monoid of (X, X ) in IntRel, there was no a priori reason to give vertical composition special status. For squares of this form, horizontal composition and summing over all possible paths is also a possibility. That is, the following is an alternative (and equivalent) de?nition of composition: X
c

GF
d

/X

t

ED
r

/X O
u

X =

t(dr )? c

/X O
u∪t(dr )? ds

a

a∪b(rd)? rc

 Xo

@A
b

Xo

BC
s

X

 Xo

b(rd)? s

X

We now have two distinct compositions on endomorphism monoids of compact closed categories. Of course, taking the union over the set of all possible paths between points is independent of the way the paths were constructed, so given a b members a, b, c, d of the endomorphism monoid of (X, X ), then = c d (a b) So, if we (temporarily) write compositions linearly, and denote the (c d) vertical and horizontal compositions by ? and · respectively, then the above becomes (a · b) ? (c · d) = (a ? c) · (b ? d). This is the interchange law, and is a one-dimensional way of representing a two-dimensional equation3 . Proposition 4 then states that Theorem 5 Computation relations of a bounded Turing machine are idempotent with respect to the horizontal composition.
3 We refer to [6] for examples and applications to topology, and [3] for applications to quantum ?eld theories - in particular, using compact closed categories.

13

4.4

Calculating computation relations

In the above section we derived, in terms of compact closed categories, formul? that computation relations must satisfy; however, we have not yet found any way of constructing computation relations, or of writing the computation relations of words in terms of computation relations of shorter words. We ?rst need these relations for words of length one. This can be done using the same tools as the calculation of global transition relations for two-way automata: Theorem 6 The computation of a bounded Turing machine on words of length 1 can be calculated in terms of a two-way automaton computation. Proof We de?ne a two-way automaton that has a single character, say 1, for its input alphabet, has Q × Σ as its set of states, and next state functions ·l and ·r given by 1 ·l (x, q ) = (x ?l q, x ?l q ) and (x, q ) ·r 1 = (q ?r x, q ?r x). It can be seen from the construction of this two-way automaton that if the pair ((y, p), (x, q )) is in [← 1?], then there is a computation of our bounded Turing machine that starts in the con?guration xq and goes to in the con?guration p y . Similar results apply for [?1 →], [? ?]. So we can calculate the computation ? 1], and [1 ? relations for words of length 1 using a version of Girard’s resolution formula (see the discussion of algebraic models of two-way automata) that does not use the idempotent π (since we do not restrict to ‘leftmoving’ or ‘rightmoving’ states)4 . 2 What the above trick does, intuitively, is to ‘push all the computation onto the set of states and the next state function’. However, we cannot immediately reconstruct the behaviour of a bounded Turing machine using Birget’s composition. The above assumes that we are considering words of length 1, and any composition using Birget’s formul? will at most give us more information about the behavior of words of length 1. To calculate the computation relation of m + n in terms of n and m , note that in general, m and n are members of two di?erent monoids, and we require a result that is in a third monoid. For clarity, we denote the set Σn × Q by Cn , and refer to the monoid B (Cn ) What we require is functions that take relations in B (Cn ) to relations in B (Cm+n ), for all n ∈ N. We de?ne two functions, as follows: rm : B (Cn ) → B (Cm+n ) is de?ned by rm (S ) = q′ wv , q wu : q′ v , q u ∈ S , w ∈ Σm

and dually, ln : B (Cm ) → B (Cm+n ) is de?ned for all m ∈ N by ln (T ) = q′ vw , q uw : q′ v , q u ∈ T , w ∈ Σn

4 This variation on the resolution formula is also used in the Geometry of Interaction series of papers, where it is called the execution formula. However, a discussion of the similarities will take us too far from our original aim, so we refer to [12].

14

Lemma 7 (i) The functions ln : Ca → Ca+n and rm : Ca → Cm+a are homomorphisms for all a ∈ N. (ii) Let Y be a relation in B (Cn ) and let X be a relation in B (Cm ). Then lm (Y )rn (X ) = q ′′ zv , q yu : q ′′ z , q′ y ∈Y , q′ v , q u ∈X .

Proof Both the above results follow directly from the de?nition of composition in monoids of relations, and from the de?nitions of lm and rn . 2 Now consider two right-to-left computations of a bounded Turing machine; the ?rst on a word of length m, and the second on a word of length n. Assume ′ ′′ the ?rst one takes con?guration y q to con?guration q z . Similarly, the second q q′ takes con?guration u , to con?guration v . Then it is immediate that there exists a computation of our bounded Turing machine, on a word of length m + n ′′ that from con?guration yuq to con?guration q zv . We draw this as
q′ q′′

ym . . . y1 zm . . . z1

? un . . . u1 q ′ ? vn . . . v1 q

q′′

zm . . . z1 vn . . . v1

? ym . . . y1 u n . . . u 1

q

Comparing this with Lemma 11 above then gives the computational interpretation of the l and r functions. We can apply ln and rm to the 4-tuples of relations of B (Cn ) that make up members of IntRel(Cn , Cn ) to form two functions Rm : IntRel(Cn , Cn ) → IntRel(Cm+n , Cm+n ) and Ln : IntRel(Cm , Cm ) → IntRel(Cm+n , Cm+n ), in a natural way, as follows: Cm+n
rm ( ? ?n )

? ? Rm ? ?

?

Cn
←w ?

? ?n

/ Cn O
?w →

?

/ Cm+n O
r m ( ?w → )

 Cn o

w? ?

Cn

? ? ?= ?

rm ( ←w ? )

 Cm+n o

rm ( w ? ? )

Cm+n

The de?nition for Ln is similar. The main result of this paper then follows from these two de?nitions: Theorem 8 Consider a bounded Turing machine T, and let its computation relations for words of length m and n be given by m and n respectively. Then its computation relations for words of length m + n are given by m + n = Rm ( n ) ? Ln ( m ) where ? denotes the vertical composition in the monoid of (Cm+n , Cm+n ) in IntRel. 15

Proof In the following proof, we denote rm ( ← n? ) by r( ← n? ), for simplicity, and similarly for l. We ?rst consider the case of ← m + n? . By the above example, l( ← m? )r( ← n? ) ? ← m + n? However, we can say more; consider a bounded Turing machine computation on a word of length m + n, and mark the intersection between cell m and cell m + 1 (counting from the left) by the symbol @. So, our cells are numbered 1 2 3 ...m
@

m+ 1 ... m + n

Now consider a computation of T on this tape that starts on the right and ?nishes on the left, and count the number of times the read / write head passes through the point @ (The crossing number). Also assume that this computation starts in state p and ends in state q , and takes an input word yu to an output word zv . By the above example, if the read / write head passes through the point @ once, then q zv , p yu ∈ l( ← m? )r( ← n? ).

Similarly, using lemma7, if the read head passes through the point @ three times (clearly, it cannot pass through an even number of times on its way from the right hand side to the left hand side) then we must have that q zv , p yu ∈ l( ← m? )r( ? ? )r( ← n? ). ? n )l( m ?

Then if the read head passes through the point @ ?ve times q zv , p yu ∈ l( ← m? )(r( ? ? ))2 r( ← n? ). ? n )l( m ?

In general, whatever the crossing number of the point @, q zv , p yu ∈ l( ← m? )(r( ? ? ))i r( ← n? ) ? n )l( m ?

for some natural number i. Therefore, ← m + n? = l( ← m? )(r( ? ? ))? r( ← n? ) ? n )l( m ? The left / right moving symmetry gives us the dual of this with no further calculation, so ?m + n → = r( ?n → )(l( ? ? ))? l( ?m → ) ? m )r( n ? Right to right movement is dealt with in a similar way; the main point to note is that if the read head does not pass through the point @, then the contents 16

of the tape to the left of the point @ cannot change (this is the interpretation of the set of all possible words of Σm being put on the left of words of Σn by the rn homomorphism). The case when the read head does pass through this point is then dealt with by a similar crossing number argument, to give m+n? ? ))? r( ← n? ) ? n )l( m ? ? )(r( ? ? ) ∪ r( ?n → )l( m ? ? = r( n ? Again, duality gives the left to left movement as ? ? n ))? l( ?m → ). ? )r( ? ? n )(l( m ? ? m ) ∪ l( ← m? )r( ? ? m + n = r( ? Comparing the above four terms with the vertical composition, ?, of IntRel gives m + n = Rm ( n ) ? Ln ( m ), as required. 2 Corollary 9 From the computational interpretation, it is immediate that if A ∈ IntRel((Cn , Cn ), (Cn , Cn )) , B ∈ IntRel((Cm , Cm ), (Cm , Cm )) are computation relations for a bounded Turing machine T, then Lm (A)Rn (B ) = Ln (B )Rm (A). That is, they both give the computation relations for the behavior of T on a tape of length m + n. 2 Although this is a necessary condition for computation relations to satisfy, it is not known whether this is a characterisation of computation relations.

4.5

Bounded Turing machine models as monoid homomorphisms
can be considered to be a monoid homomor-

We demonstrate that the map phism, as follows: De?nition We de?ne


T∞ =
i=0

Intrel((Ci , Ci ), (Ci , Ci )) × {i}

and de?ne a composition on T∞ by (B, m) ? (A, n) = (Rm (A) ? Ln (B ), m + n) where ? is the vertical composition of Intrel((Cm+n , Cm+n ), (Cm+n , Cm+n )). Lemma 10 (T∞ , ?) is a monoid. Proof it is immediate by Lemma 7 that ? is associative. Also, the identity of the monoid at (Q × λ, Q × λ) is an identity for this composition. Our result then follows. 2 17

Theorem 11 Let T denote a bounded Turing machine. The map t : N → T∞ de?ned by t(n) = n is a monoid homomorphism. Proof By de?nition, t(λ) is the identity of T∞ , and associativity follows from theorem 8. 2

4.6

Extracting information from computation relations

An objection that could be raised to the de?nitions of this paper is that the computation relations for a bounded Turing machine give no information about speci?c computations, as they describe all possible computations on a given tape length. We now demonstrate how information about speci?c computations can be extracted from computation relations. Let T be a bounded Turing machine, and consider its computation relations on a tape of length n. Information about computation that go from left to right can be extracted from the relation ← n? . Consider q ∈ Q and u ∈ Σn . By construction, q′ v


,

q u

∈ ← n?

q u

,

q u

implies that uq → q v is a computation of T. Similarly the composition ?n → will be the set of pairs q′ v q u u q , u q
q

. u → v q is a computation


,

satisfying

of T. If we restrict by an idempotent on the left hand side, instead of the right, then the composite q q , ← n? u u
′ q q′ , satisfying q v → uq is a compuu v tation of T. So, we can also specify the ?nal state of a computation, and use the computation relation to calculate the set of initial states that lead to it. We can, of course, calculate with the other computation relations in a similar way.

will be the set of pairs

5

Conclusion, and discussion of methods

In the above sections, we have demonstrated how symmetry ideas are useful in the basic level of theoretical computing. It is encouraging to see the emergence 18

of the same mathematical tools that are used in both linear logic and theoretical physics. A natural point that is missing for the above is any discussion of generalisations of the syntactic monoid of an automaton – that is, of the languages recognised by bounded Turing machines. However, this appears to be a signi?cantly more complicated subject; the question of whether bounded Turing machines have the same recognising power in the deterministic and nondeterministic case is still undecided (See [15], p.229), and a solution, whether positive or negative, appears to have important consequences. Constructing algebraic models of transitions is just the ?rst step in answering this question. The way in which the mathematical symmetries follow the intuitive ideas of dualising automata is apparent in the ?rst two cases. For the generalisation to non-deterministic automata, every relation R can be written as G?1 F for functions F, G. For the generalisation to two-way automata, the mathematical representation is Joyal, Street, and Verity’s Int construction, where every object A is given a dual A∨ . However, there is no analogous mathematical representation for the generalisation to either Mealy machines, or bounded Turing machines. Not only that, but the monoid T∞ can be thought of as taking a copy of the endomorphism monoid of (Q, Q) at each word in Σ? — this is much more that a dualising process. In the above generalisations of ?nite state automata, we were (at least partially) motivated by our end-point; we already knew which models of computation we expected to construct. However, there were other possible routes to take: ? For the ’reversing arrows’ symmetry, the replacement of functions by relations was possibly too much of a generalisation. An alternative possibility would be to allow partial injections — see [22] for the resulting algebraic theory, under the name of inverse semigroups — and restrict them as follows: partial injections from the same state would have distinct domains, and partial injections to the same state would have distinct images (in the deterministic case, we would also require the union of the domains and of images of partial functions at a state be full). The two-way case would be slightly more complex, but the conditions required (that is, the conditions for an inverse compact closed category of partial injections) have already been found, in the context of the Geometry of Interaction, in [14]. ? For the state / alphabet symmetry, an alternative possibility would be to have the same set for the states, and the alphabet. However, although this is at ?rst sight simpler, it means that a string of function symbols f gh is ambiguous; if f (g ) = k , and g (h) = l, this could denote either k (h) or f (l). Alternatively, it could denote the function given by applying h, then g , then f . Abandonment of associativity would make mathematical models signi?cantly more complex. ? It would also be reasonable to require, not only a function ? : Σ × Q → Q, but also a function from Q to Σ × Q, and similarly for ? : Σ × Q → Σ. Unexpectedly, I recently became aware of an application of this (in the 19

one-way case) in the context of functional programming and automatic program transformation, in the work of Martin Erwig, [9].

5.1

Acknowledgments

I am very grateful to John Baez for several impromptu tutorials on the theory of duality and compact closure, as used in quantum mechanics, and to Ronnie Brown for introducing me to the interchange law and higher dimensional algebra. Thanks are also due to Ian France for a critical non-specialist reading of a preliminary version of this paper, and to Jon Hillier, for encouraging me to generalise two-way automata models to bounded Turing machines and pointing out some of the ways in which it was a non-trivial exercise. Finally, I would also like to thank Mark Lawson for referring me to J.-C. Birget’s equations, when I was studying compact closure in a di?erent context, and for suggesting that computation relations could be writtten in terms of a monoid, rather than a category.

References
[1] S. Abramsky, Retracing some paths in Process algebra, CONCUR 96. [2] S. Abramsky, R. Jagadeesan, New Foundations for the Geometry of Interaction, Proc. Seventh IEEE Symposium on Logic in Computer Science, 211-222 (1992) [3] J. Baez, Higher-dimensional algebra II: 2-Hilbert spaces, Adv. Math. 127 (1997), 125-189 [4] J.-C. Birget, Basic Techniques for Two-way Finite Automata, in : J.E. Pin (ed.), Formal Properties of Finite Automata and Applications, SLNCS, Springer-Verlag (1989) 56-64 [5] J.-C. Birget, Concatenation of inputs in a two-way automaton, Theoretical Computer Science 63 (1989) 141-156 [6] R. Brown, Higher dimensional group theory, in Low Dimensional Topology, London Math Soc. Lecture Note Series 48 (ed. R. Brown and T.L. Thickstun, Cambridge University Press, 1982, 215-238 [7] D. Cohen Introduction to Computer Theory, J. Wiley and Sons Inc. (1991) [8] V. Danos, L. Regnier, Reversible and Irreversible computations (GOI and λ-machines), Univ. Marseille Preprint [9] M. Erwig, Beyond homomorphisms, Preprint, FernUniversitat Hagen (1998) [10] J-Y. Girard, Linear Logic, Theor. Comp. Sci. 50, (1987) 1-102

20

[11] J-Y. Girard, Geometry of interaction 1, Proceedings Logic Colloquium ’88, (1989) 221-260, North Holland. [12] J-Y. Girard, Geometry of interaction 2, Proceedings of COLOG 88, Martin-Lof & Mints, 76-93 SLNCS 417 [13] J-Y. Girard, Geometry of interaction 3, Proceedings of the Workshop on Linear Logic 1994, MIT Press, To appear. [14] P.M. Hines, The Algebra of Self-similarity and its Applications, PhD thesis, University of Wales (1997) [15] J. Hopcroft, J. Ullman, Introduction to Automata Theory, Languages and Computation, Addison-Wesley (1979) [16] J. Howie, Automata and Languages, Oxford Science Publications, Oxford University Press, (1991) [17] J. Howie, Fundamentals of Semigroup Theory, Clarendon Press, Oxford, (1995) [18] A. Joyal, R. Street, The geometry of tensor calculus I, Advances in Math. 102 (1993) 20-78 [19] A. Joyal, R. Street, The Geometry of Tensor calculus II, to appear. [20] A. Joyal, R. Street, D. Verity, Traced Monoidal categories, Math. Proc. Camb. Phil. Soc., (1996) 425-446 [21] G. Kelly, M. Laplaza, Coherence for compact closed categories, Journal of Pure and Applied Algebra 19 (1980) 193-213 [22] M.V. Lawson, Inverse Semigroups: the theory of partial symmetries, World Scienti?c, Singapore (Due 1998) [23] S. MacLane, Categories for the working mathematician, Springer-Verlag, New York (1971) [24] Mei Chee Shum, Tortile tensor categories, Journal of Pure and Applied Algebra 93 (1994) 57-110 [25] J. C. Shepherdson, The reduction of two-way automata to one-way automata, IBM Journal of Research and Development (1959) 115-125

21


赞助商链接

更多相关文章:
更多相关标签:

All rights reserved Powered by 甜梦文库 9512.net

copyright ©right 2010-2021。
甜梦文库内容来自网络,如有侵犯请联系客服。zhit325@126.com|网站地图