1: \documentclass[amssymb,11pt]{article}

2: %\usepackage{hyperref}   % this package must appear in first line

3: %\usepackage{latexsym}   % for type $\Box$

4: %\usepackage{lgrind}     % for formated source code

5: %\usepackage{latexcad}   % latexcad.sty for drawings etc

6: \usepackage{graphicx}

7: %\usepackage{amsmath, amssymb, amsthm}

8: \setlength{\oddsidemargin}{10mm} \setlength{\marginparwidth}{0mm}

9: \setlength{\marginparsep}{0mm} \setlength{\topmargin}{0mm}

10: \setlength{\topskip}{0mm}

11: 

12: \setlength{\textwidth}{140mm} \setlength{\textheight}{210mm}

13: 

14: \setlength{\parskip}{2pt}

15: 

16: \begin{document}

17: \title{A Theory of Computation Based on Quantum Logic (I)}

18: \author{Mingsheng Ying\thanks{This work was partly

19: supported by the National Key Project for Fundamental Research of

20: China (Grant No: 1998030905) and the National

21: Foundation of Natural Sciences of China (Grant No: 60273003)}\\

22: \\

23: \small \em State Key Laboratory of Intelligent Technology and Systems,\\

24: \small \em Department of Computer Science and Technology,\\

25: \small \em Tsinghua University, Beijing 100084, China,\\

26: \small \em Email: yingmsh@tsinghua.edu.cn}

27: \date{}

28: \maketitle

29: 

30: \begin{abstract}

31: The (meta)logic underlying classical theory of computation is

32: Boolean (two-valued) logic. Quantum logic was proposed by Birkhoff

33: and von Neumann as a logic of quantum mechanics more than sixty

34: years ago. It is currently understood as a logic whose truth

35: values are taken from an orthomodular lattice. The major

36: difference between Boolean logic and quantum logic is that the

37: latter does not enjoy distributivity in general. The rapid

38: development of quantum computation in recent years stimulates us

39: to establish a theory of computation based on quantum logic. The

40: present paper is the first step toward such a new theory and it

41: focuses on the simplest models of computation, namely finite

42: automata. We introduce the notion of orthomodular lattice-valued

43: (quantum) automaton. Various properties of automata are carefully

44: reexamined in the framework of quantum logic by employing an

45: approach of semantic analysis. We define the class of regular

46: languages accepted by orthomodular lattice-valued automata. The

47: acceptance abilities of orthomodular lattice-valued

48: nondeterministic automata and their various modifications (such as

49: deterministic automata and automata with $\varepsilon-$moves) are

50: compared. The closure properties of orthomodular lattice-valued

51: regular languages are derived. The Kleene theorem about

52: equivalence of regular expressions and finite automata is

53: generalized into quantum logic. We also present a pumping lemma

54: for orthomodular lattice-valued regular languages. It is found

55: that the universal validity of many properties (for example, the

56: Kleene theorem, the equivalence of deterministic and

57: nondeterministic automata) of automata depend heavily upon the

58: distributivity of the underlying logic. This indicates that these

59: properties does not universally hold in the realm of quantum

60: logic. On the other hand, we show that a local validity of them

61: can be recovered by imposing a certain commutativity to the

62: (atomic) statements about the automata under consideration. This

63: reveals an essential difference between the classical theory of

64: computation and the computation theory based on quantum logic.

65: \end{abstract}\par

66: 

67: \smallskip\

68: 

69: \emph{Key Words:} Quantum logic, orthomodular lattice, algebraic

70: semantics,

71: 

72: finite automata, regular languages, quantum computation

73: 

74: \vspace{2em}

75: 

76: \textbf{Contents}

77: 

78: \smallskip\

79: 

80: 1. Introduction (page 2)

81: 

82: 2. Quantum logic (page 11)

83: 

84: \ \ \ \ 2.1. Orthomodular lattices (page 11)

85: 

86: \ \ \ \ 2.2. The language of quantum logic (page 20)

87: 

88: \ \ \ \ 2.3. The algebraic semantics of quantum logic (page 20)

89: 

90: \ \ \ \ 2.4. The operations of quantum sets (page 22)

91: 

92: 3. Orthomodular lattice-valued automata (page 25)

93: 

94: 4. Orthomodular lattice-valued deterministic automata (page 33)

95: 

96: 5. Orthomodular lattice-valued automata with $\epsilon-$moves

97: (page 40)

98: 

99: 6. Closure properties of orthomodular lattice-valued regularity

100: (page 44)

101: 

102: 7. Orthomodular lattice-valued regular expressions (page 57)

103: 

104: 8. Pumping lemma for orthomodular lattice-valued regular languages

105: (page 69)

106: 

107: 9. Conclusion (page 71)

108: 

109: \ \ \ \ References (page 73)

110: 

111: \bigskip\

112: 

113: \smallskip\

114: 

115: \textbf{1. Introduction}

116: 

117: \smallskip\

118: 

119: It is well-known that an axiomatization of a mathematical theory

120: consists of a system of fundamental notions as well as a set of

121: axioms about these notions. The mathematical theory is then the

122: set of theorems which can be derived from the axioms. Obviously,

123: one needs a certain logic to provide tools for reasoning in the

124: derivation of these theorems from the axioms. As pointed out by A.

125: Heyting [He63, page 5], in elementary axiomatics logic was used in

126: an unanalyzed form. Afterwards, in the studies for foundations of

127: mathematics beginning in the early of twentieth century, it had

128: been realized that a major part of mathematics has to exploit the

129: full power of classical (Boolean) logic [Ha82], the strongest one

130: in the family of existing logics. For example, group theory is

131: based on first-order logic, and point-set topology is built on a

132: fragment of second-order logic. However, a few mathematicians,

133: including the big names L. E. J. Brouwer, H. Poincare, L.

134: Kronecker and H. Weyl, took some kind of constructive position

135: which is in more or less explicit opposition to certain forms of

136: mathematical reasoning used by the majority of the mathematical

137: community. Some of them even endeavored to establish so-called

138: constructive mathematics, the part of mathematics that could be

139: rebuilt on constructivist principles. The logic employed in the

140: development of constructive mathematics is intuitionistic logic

141: [TD88] which is truly weaker than classical logic.

142: 

143: Since many logics different from classical logic and

144: intuitionistic logic have been invented in the last century, one

145: may naturally ask the question whether we are able to establish

146: some mathematical theories based on other nonclassical logics

147: besides intuitionistic logic. Indeed, as early as the first

148: nonclassical logics appeared, the possibility of building

149: mathematics upon them was conceived. As mentioned by A. Mostowski

150: [M65], J. Lukasiewicz hoped that there would be some nonclassical

151: logics which can be properly used in mathematics as non-Euclidean

152: geometry does. In 1952, J. B. Rosser and A. R. Turquette [RT52,

153: page 109] proposed a similar and even more explicit idea:

154: $$$$

155: \textit{"The fact that it is thus possible to generalize the

156: ordinary two-valued logic so as not only to cover the case of

157: many-valued statement calculi, but of many-valued quantification

158: theory as well, naturally suggests the possibility of further

159: extending our treatment of many-valued logic to cover the case of

160: many-valued sets, equality, numbers, etc. Since we now have a

161: general theory of many-valued predicate calculi, there is little

162: doubt about the possibility of successfully developing such

163: extended many-valued theories. ... we shall consider their careful

164: study one of the major unsolved problems of many-valued logic."}

165: $$$$

166: Unfortunately, the above idea has not attracted much attention in

167: logical community. For such a situation, A. Mostowski [M65]

168: pointed out that most of nonclassical logics invented so far have

169: not been really used in mathematics, and intuitionistic logic

170: seems the unique one of nonclassical logics which still has an

171: opportunity to carry out the Lukasiewicz's project. A similar

172: opinion was also expressed by J. Dieudonne [Di78], and he said

173: that mathematical logicians have been developing a variety of

174: nonclassical logics such as second-order logic, modal logic and

175: many-valued logic, but these logics are completely useless for

176: mathematicians working in other research areas.

177: 

178: One reason for this situation might be that there is no suitable

179: method to develop mathematics within the framework of nonclassical

180: logics. As was pointed out above, classical logic is applied as

181: the deduction tool in almost all mathematical theories. It should

182: be noted that what is used in these theories is the deductive

183: (proof-theoretical) aspect of classical logic. However, the proof

184: theory of nonclassical logics is much more complicated than that

185: of classical logic, and it is not an easy task to conduct

186: reasoning in the realm of the proof theory of nonclassical logics.

187: It is the case even for the simplest nonclassical logics,

188: three-valued logics. This is explicitly indicated by the following

189: excerpt from H. Hodes [Ho89]:

190: $$$$

191: \textit{"Of course three-valued logics will be somewhat more

192: complicated than classical two-valued logic. In fact,

193: proof-theoretically they are at least twice as complicated: ....

194: But model-theoretically they are only 50 percent more

195: complicated,....}

196: $$$$

197: And much worse, some nonclassical logics were introduced only in a

198: semantic way, and the axiomatizations of some among them are still

199: to be found, and some of them may be not (finitely) axiomatizable.

200: Thus, our experience in studying classical mathematics may be not

201: suited, or at least cannot directly apply, to develop mathematics

202: based on nonclassical logics. In the early 1990's an attempt had

203: been made by the author [Yi91-93; Yi93] to give a partial and

204: elementary answer in the case of point-set topology to the J. B.

205: Rosser and A. R. Turquette's question raised above. We employed a

206: semantical analysis approach to establish topology based on

207: residuated lattice-valued logic, especially the Lukasiewicz system

208: of continuous-valued logic. Roughly speaking, the semantical

209: analysis approach transforms our intended conclusions in

210: mathematics, which are usually expressed as implication formulas

211: in our logical language, into certain inequalities in the

212: truth-value lattice by truth valuation rules, and then we

213: demonstrate these inequalities in an algebraic way and conclude

214: that the original conclusions are semantically valid. We believe

215: that semantical analysis approach is an effective method to

216: develop mathematics based on nonclassical logics.

217: 

218: A much more essential reason for the situation that few

219: nonclassical logics have been applied in mathematics is absence of

220: appealing from other subjects or applications in the real world.

221: One major exception may be the case of quantum logic. Quantum

222: logic was introduced by G. Birkhoff and J. von Neumann [BN36] in

223: the thirties of the twentieth century as the logic of quantum

224: mechanics. They realized that quantum mechanical systems are not

225: governed by classical logical laws. Their proposed logic stems

226: from von Neumann's Hilbert space formalism of quantum mechanics.

227: The starting point was explained very well by the following

228: excerpt from G. Birkhoff and J. von Neumann [BN36]:

229: $$$$

230: \textit{"what logical structure one may hope to find in physical

231: theories which, like quantum mechanics, do not conform to

232: classical logic. Our main conclusion, based on admittedly

233: heuristic arguments, is that one can reasonably expect to find a

234: calculus of propositions which is formally indistinguishable from

235: the calculus of linear subspaces [of Hilbert space] with respect

236: to set products, linear sums, and orthogonal complements - and

237: resembles the usual calculus of propositions with respect to

238: 'and', 'or', and 'not'."}

239: $$$$

240: Thus linear (closed) subspaces of Hilbert space are identified

241: with propositions concerning a quantum mechanical system, and the

242: operations of set product, linear sum and orthogonal complement

243: are treated as connectives. By observing that the set of linear

244: subspaces of a finite-dimensional Hilbert space together with

245: these operations enjoys Dedekind's modular law, G. Birkhoff and J.

246: von Neumann [BN36] suggested to use modular lattices as the

247: algebraic version of the logic of quantum mechanics, just like

248: that Boolean algebras act as an algebraic counterpart of classical

249: logic. However, the modular law does not hold in an

250: infinite-dimensional Hilbert space. In 1937, K. Husimi [Hu37]

251: found a new law, called now the orthomodular law, which is valid

252: for the set of linear subspaces of any Hilbert space. Nowadays,

253: what is usually called quantum logic in the mathematical physics

254: literatures refers to the theory of orthomodular lattices.

255: Obviously, this kind of quantum logic is not very logical. Indeed,

256: there is also another much more 'logical' point of view on quantum

257: logic in which quantum logic is seen as a logic whose truth values

258: range over an orthomodular lattice (for an excellent exposition

259: for the latter approach of quantum logic, see M. L. Dalla Chiara

260: [DC86], or J. P. Rawling and S. A. Selesnick [RS00]). After the

261: invention of quantum logic, quite a few mathematicians have tried

262: to establish mathematics based on quantum logic. Indeed, J. von

263: Neumann [N62] himself proposed the idea of considering a quantum

264: set theory, corresponding to quantum logic, as does classical set

265: theory to classical logic. One important contribution in this

266: direction was made by G. Takeuti [T81]. His main idea was

267: explained, and the nature of mathematics based on quantum logic

268: was analyzed very well by the following citation from the

269: introduction of [T81]:

270: $$$$

271: \textit{"Since quantum logic is an intrinsic logic, i.e. the logic

272: of the quantum world, it is an important problem to develop

273: mathematics based on quantum logic, more specifically set theory

274: based on quantum logic. It is also a challenging problem for

275: logicians since quantum logic is drastically different from the

276: classical logic or the intuitionistic logic and consequently

277: mathematics based on quantum logic is extremely difficult. On the

278: other hand, mathematics based on quantum logic has a very rich

279: mathematical content. This is clearly shown by the fact that there

280: are many complete Boolean algebras inside quantum logic. For each

281: complete Boolean algebra $B$, mathematics based on $B$ has been

282: shown by our work on Boolean valued analysis to have rich

283: mathematical meaning. Since mathematics based on $B$ can be

284: considered as a sub-theory of mathematics based on quantum logic,

285: there is no doubt about the fact that mathematics based on quantum

286: logic is very rich. The situation seems to be the following.

287: Mathematics based on quantum logic is too gigantic to see through

288: clearly."}

289: $$$$

290: The main technical result of G. Takeuti [T81] is a construction of

291: orthomodular lattice-valued universe. He built up such an universe

292: in a way similar to Boolean-valued models of ZF + AC, and showed

293: that a reasonable set theory, including some axioms from ZF + AC

294: or their slight modifications, holds in this universe. Recently,

295: K. -G. Schlesinger [Sc99] developed a theory of quantum sets by

296: using a categorical approach in the spirit of topos theory. He

297: started with the category of complex (pre-)Hilbert spaces and

298: linear maps. This category was seen as the (basic) quantum set

299: universe. Then he was able to introduce the analog of number

300: systems and to deal with the analog of some algebraic structures

301: in quantum set theory. Indeed, K. -G. Schlesinger's terminal goal

302: is to build a quantum mathematics, i.e., a mathematical theory

303: where all the ingredients (like logic and set theory) adhere to

304: the rules of quantum mechanics. Quantum set theory is the

305: quantization of the mathematical theory of pure objects, and so it

306: is just the first step toward his goal. It is worth noting that

307: the role of quantum logic in such a quantum mathematics is

308: different from that in G. Takeuti's quantum set theory, and

309: quantum logic appears as an internal logic in the former.

310: 

311: After a careful examination on the development of mathematics

312: based on nonclassical logics, we now come to explore the

313: possibility of establishing a theory of computation based on

314: nonclassical logics. A formal formulation of the notion of

315: computation is one of the greatest scientific achievements in the

316: twentieth century. Since the middle of 1930's, various models of

317: computation have been introduced, such as Turing machines, Post

318: systems, $\lambda-$calculus and $\mu-$recursive functions. In

319: classical computing theory, these models of computations are

320: investigated in the framework of classical logic; more explicitly,

321: all properties of them are deduced by classical logic as a

322: (meta)logical tool. So, it is reasonable to say that classical

323: computing theory is a part of classical mathematics. Knowing the

324: basic idea of mathematics based on nonclassical logics, we may

325: naturally ask the question: is it possible to build a theory of

326: computation based on nonclassical logics, and what are the same of

327: and difference between the properties of the models of

328: computations in classical logic and the corresponding ones in

329: non-classical logics? There has been a very big population of

330: non-classical logics. Of course, it is unnecessary to construct

331: models of computations in each nonclassical logic and to compare

332: them with the ones in classical logic because some nonclassical

333: logics are completely irrelative to behaviors of computations.

334: Nevertheless, as will be explained shortly, it is absolutely worth

335: studying deeply and systematically models of computations based on

336: quantum logic.

337: 

338: It seems that both points of views on quantum logic mentioned

339: above have no obvious links to computations; but appearance of the

340: idea of quantum computers changed dramatically the long-standing

341: situation. The idea of quantum computation came from the studies

342: of connections between physics and computation. The first step

343: toward it was the understanding of the thermodynamics of classical

344: computation. In 1973, C. H. Bennet [Ben73] noted that a logically

345: reversible operation need not dissipate any energy and found that

346: a logically reversible Turing machine is a theoretical

347: possibility. In 1980, further progress was made by P. A. Benioff

348: [Be80] who constructed a quantum mechanical model of Turing

349: machine. His construction is the first quantum mechanical

350: description of computer, but it is not a real quantum computer. It

351: should be noted that in P. A. Benioff's model between computation

352: steps the machine may exist in an intrinsically quantum state, but

353: at the end of each computation step the tape of the machine always

354: goes back to one of its classical states. Quantum computers were

355: first envisaged by R. P. Feynman [Fe82; Fe86]. In 1982, he [Fe82]

356: conceived that no classical Turing machine could simulate certain

357: quantum phenomena without an exponential slowdown, and so he

358: realized that quantum mechanical effects should offer something

359: genuinely new to computation. Although R. P. Feynman proposed the

360: idea of universal quantum simulator, he did not give a concrete

361: design of such a simulator. His ideas were elaborated and

362: formalized by D. Deutsch in a seminal paper [De85]. In 1985, D.

363: Deutsch described the first true quantum Turing machine. In his

364: machine, the tape is able to exist in quantum states too. This is

365: different from P. A. Benioff's machine. In particular, D. Deutsch

366: introduced the technique of quantum parallelism by which quantum

367: Turing machine can encode many inputs on the same tape and perform

368: a calculation on all the inputs simultaneously. Furthermore, he

369: proposed that quantum computers might be able to perform certain

370: types of computations that classical computers can only perform

371: very inefficiently. One of the most striking advances was made by

372: P. W. Shor [S94] in 1994. By exploring the power of quantum

373: parallelism, he discovered a polynomial-time algorithm on quantum

374: computers for prime factorization of which the best known

375: algorithm on classical computers is exponential. In 1996, L. K.

376: Grover [Gr96] offered another apt killer of quantum computation,

377: and he found a quantum algorithm for searching a single item in an

378: unsorted database in square root of the time it would take on a

379: classical computer. Since both prime factorization and database

380: search are central problems in computer science and the quantum

381: algorithms for them are highly faster than the classical ones, P.

382: W. Shor and L. K. Grover's works stimulated an intensive

383: investigation on quantum computation. After that, quantum

384: computation has been an extremely exciting and rapidly growing

385: field of research.

386: 

387: The studies of quantum computation may be roughly divided into

388: four strata, arranged according increasing order of abstraction

389: degree: (1) physical implementations; (2) physical models; (3)

390: mathematical models; and (4) logical foundations. Almost all

391: pioneer works such as [Be80, F82, D85] in this field were devoted

392: to build physical models of quantum computing. In 1990's, a great

393: attention was paid to the physical implementation of quantum

394: computation. For example, S. Lloyd [L93] considered the practical

395: implementation by using electromagnetic pulses and J. I. Cirac and

396: P. Zoller [CZ95] used laser manipulations of cold trapped ions to

397: implement quantum computing. The current theoretical concerns in

398: the area of quantum computation have mainly been given to quantum

399: algorithms. But also there have been a few attempts to develop

400: mathematical models of quantum computation and to clarify the

401: relationship between different models. For example, except quantum

402: Turing machines, D. Deutsch [De89] also proposed the quantum

403: circuit model of computation, and A. C. Yao [Ya93] showed that the

404: quantum circuit model is equivalent to the quantum Turing machine

405: in the sense that they can simulate each other in polynomial time.

406: As is well known, in classical computing theory, there are still

407: two important classes of models of computation rather than Turing

408: machines; namely, finite automata and pushdown automata. They are

409: equipped with finite memory or finite memory with stack,

410: respectively, and so have weaker computing power than Turing

411: machines. Recently, J. P. Crutchfield and C. Moore [CM00], A.

412: Kondacs and J. Watrous [KW97], and S. Gudder [Gu00] tried to

413: introduce some quantum devices corresponding to these weaker

414: models of computation. Roughly speaking, quantum automata may be

415: seen as quantum counterparts of probabilistic automata. In a

416: probabilistic automaton, each transition is equipped with a number

417: in the unit interval to indicate the probability of the occurrence

418: of the transition; by contrast in a quantum automaton we associate

419: with each transition a vector in a Hilbert space which is

420: interpreted as the probability amplitude of the transition. In a

421: sense, these mathematical models of quantum computation can be

422: seen as abstractions of its physical models.

423: 

424: It should be noted that the theoretical models of quantum

425: computation mentioned above, including quantum Turing machines and

426: quantum automata, are still developed in classical (Boolean)

427: logic. Thus, their logical basis is the same as that of classical

428: computation, and we may argue that sometimes these models might be

429: not suitable for quantum computers that obey some logical laws

430: different from that in Boolean logic. Indeed, V. Vedral and M. B.

431: Plenio [VP98] already advocated that quantum computers require

432: quantum logic, something fundamentally different to classical

433: Boolean logic. As stated above, quantum logic has been existing

434: for a long time. So, the point is how to apply quantum logic in

435: the analysis and design of quantum computers. The background

436: exposed above highly motivates us to explore the possibility of

437: establishing a theory of computation based on quantum logic. The

438: purpose of the present paper and its continuations is exactly to

439: develop such a new theory. In a sense, our approach may be thought

440: of as a logical foundation of quantum computation and a further

441: abstraction of its mathematical models. The relation between

442: Crutchfield et al's studies [CM00, KW97, Gu00] on quantum automata

443: and our automata theory based on quantum logic is quite similar to

444: that between J. von Neumann's Hilbert space formalism of quantum

445: mechanics and quantum logic.

446: 

447: Since finite automata are the simplest models of computation (with

448: finite memory), in this paper we focus our attention on developing

449: a theory of finite automata based on quantum logic. The present

450: paper is organized as follows. In Section 2, we recall some basic

451: notions and results of quantum logic and its algebraic semantics

452: needed in the subsequent sections from the previous literature.

453: Some new lemmas on implication operators in quantum logic are

454: presented too. They are crucial in the proofs of several main

455: results in this paper. In Section 3, we introduce the notion of

456: orthomodular lattice-valued (quantum) automaton. Then two

457: different orthomodular lattice-valued predicates of regularity on

458: languages are proposed. These two predicates stands indeed for the

459: (orthomodular lattice-valued) class of languages accepted by

460: orthomodular lattice-valued automata. This provides us with a

461: framework in which various properties of automata can be

462: reexamined within quantum logic. The technique employed in this

463: paper is mainly the approach of semantic analysis developed in

464: [Yi91-93; Yi93]. The acceptance ability of orthomodular

465: lattice-valued nondeterministic automata are then compared with

466: that of their two kinds of modifications, namely deterministic

467: automata and automata with $\varepsilon-$moves, respectively in

468: Sections 4 and 5. The closure properties of orthomodular

469: lattice-valued regular languages are derived in Section 6. In

470: Section 7, we introduce the notion of orthomodular lattice-valued

471: regular expression, and the Kleene theorem about equivalence of

472: regular expressions and finite automata is generalized into

473: quantum logic. Section 8 is devoted to present a pumping lemma for

474: orthomodular lattice-valued regular languages. Some basic ideas of

475: this paper were announced in [Yi00], and Definitions 3.1 and 3.2,

476: Examples 3.1-4, and Propositions 6.1 and 6.3 were also presented

477: there. For completeness, however, they are included in the present

478: paper.

479: 

480: The most interesting thing is, in the author's opinion, the

481: discovery that the universal validity of many properties (for

482: example, the Kleene theorem, the equivalence of deterministic and

483: nondeterministic automata) of automata depend heavily upon the

484: distributivity of the underlying logic. It is shown that the

485: universal validity of these properties is equivalent to the

486: requirement that the set of truth values of the meta-logic

487: underlying our theory of automata is a Boolean algebra. This

488: indicates that these properties does not universally hold in the

489: realm of quantum logic, and it is in fact a negative conclusion in

490: our theory of automata based on quantum logic. Furthermore, it

491: implies the fact that an essential difference exists between the

492: classical theory of computation and the computation theory based

493: on quantum logic.

494: 

495: Observing that some important properties of automata cannot be

496: built within quantum logic, one may naturally ask the question

497: whether they may be partially recast without appealing to

498: distributivity of the underlying logic. Fortunately, we are able

499: to show that a local validity of these properties of automata can

500: be recovered by imposing a certain commutativity to the truth

501: values of the (atomic) statements about the automata under

502: consideration. Very surprisingly, almost all results in classical

503: automata theory that are not valid in a non-distributive logic can

504: be revived by a certain commutativity in quantum logic. This

505: further leads us to a new question: why commutativity plays such a

506: key role for quantum automata, and is there any physical

507: interpretation for it? To answer this question, let us first note

508: that all truth values in quantum logic are taken from an

509: orthomodular lattice. The prototype of orthomodular lattice is the

510: set of linear (closed) subspaces of a Hilbert space with the set

511: inclusion as its ordering relation. Suppose that $X$ and $Y$ are

512: two subspaces of a Hilbert space $H$. Moreover, we use $P_X$ and

513: $P_Y$ to denote the projections on $X$ and $Y$ respectively. Then

514: $P_X$ and $P_Y$ are Hermitian operators on $H$, and they may be

515: seen as two (physical) observables $A$ and $B$ in a quantum system

516: whose state space is $H$, according to the Hilbert space formalism

517: of quantum mechanics. If we write $\Delta (A)$ and $\Delta (B)$

518: for the respective standard deviations of measurement on $A$ and

519: $B$, then the Heisenberg uncertainty principle gives the following

520: inequality:

521: $$\Delta (A)\cdot \Delta (B)\geq \frac{1}{2} |<\psi

522: |[A,B]|\psi>|$$ for all quantum state $|\psi>$ in $H$, where

523: $[A,b]=AB-BA$ is the commutator between $A$ and $B$. We now turn

524: back to the orthomodular lattice of the linear subspaces of $H$.

525: The commutativity of $A$ and $B$ is defined by the condition

526: $X=(X\wedge Y)\vee (X\wedge Y^{\bot})$, where $\wedge$, $\vee$ and

527: $\bot$ are respectively the meet, union and orthocomplement. It

528: may be seen that the commutativity between $X$ and $Y$ is

529: equivalent to exactly the fact that $A$ and $B$ commutate, i.e.,

530: $AB=BA$. In this case, $|<\psi|[A,B]|\psi>|=0$, and $\Delta

531: (A)\cdot \Delta (B)$ may vanish; or in other words, $\Delta (A)$

532: and $\Delta (B)$ can simultaneously become arbitrarily small.

533: Remember that in our theory of automata based on quantum logic the

534: commutativity is attached to the basic statements describing the

535: considered automata. On the other hand, the basic statements are

536: indeed corresponding to some actions in these automata. Therefore,

537: a potential physical interpretation for the need of commutativity

538: is that some nice properties of automata require the standard

539: deviations of the observables concerning the basic actions in

540: these automata being able to reach simultaneously very small

541: values.

542: 

543: The results gained in our approach may offer some new insights on

544: the theory of computation. As an example, let us consider the

545: Church-Turing thesis. The realization that the intuitive notion of

546: "effective computation" can be identified with the mathematical

547: concept of "computation by the Turing machine" is based on the

548: fact that the Turing machine is computationally equivalent to some

549: vastly dissimilar formalisms for the same purpose, such as Post

550: systems, $\mu-$recursive functions, $\lambda-$calculus and

551: combinatory logic. As pointed out by J. E. Hopcroft and J. D.

552: Ullman [HU79], another reason for the acceptance of the Turing

553: machine as a general model of a computation is that the Turing

554: machine is equivalent to its many modified versions that would

555: seem off-hand to have increased computing power. We should note

556: that the equivalence between the Turing machine and its various

557: generalizations as well as other formalisms of computation has

558: been reached in classical Boolean logic. In addition, quantum

559: logic is known to be strictly weaker than Boolean logic. Thus, it

560: is reasonable to doubt that the same equivalence can be achieved

561: when our underlying meta-logic is replaced by quantum logic, and

562: the Church-Turing thesis needs to be reexamined in the realm of

563: quantum logic. Indeed, in a continuation of this paper we are

564: going to establish a theory of Turing machines based on quantum

565: logic. The details of such a theory is still to be exploited, but

566: the conclusion concerning the equivalence between deterministic

567: and nondeterministic automata obtained in this paper suggests us

568: to believe that the equivalence between deterministic and

569: nondeterministic Turing machines also depends upon the

570: distributivity of the underlying logic, and a certainty

571: commutativity for the basic actions in Turing machines will

572: guarantee such an equivalence. Keeping this belief in mind, we may

573: assert that a certain commutativity of the observables for some

574: basic actions in the Turing machine is a physical support of the

575: Church-Turing thesis in the framework of quantum logic.

576: Furthermore, with the above physical interpretation for

577: commutativity, this hints that there might be a deep connection

578: between the Heisenberg uncertainty principle and the Church-Turing

579: thesis, two of the greatest scientific discoveries in the

580: twentieth century. It is notable that such a connection could be

581: observed via an argument in a nonclassical logic (and it is

582: impossible to be found if we always work within the classical

583: logic). As early as in 1985, it was argued by D. Deutsch [De84]

584: that underlying the Church-Turing thesis there is an implicit

585: physical assertion. There is certainly no doubt about the

586: existence of such a physical assertion. The true problem here is:

587: what is it? The answer given by D. Deutsch himself is the

588: following physical principle: "every finitely realizable physical

589: system can be perfectly simulated by a universal model computing

590: machine operating by finite means". Our above analysis on the role

591: of commutativity in computation theory based on quantum logic

592: perhaps indicates that in order to be simulated by a universal

593: computing machine some observables of the physical system are

594: required to possess a certain commutativity. So, it is fair to say

595: that the observation on commutativity presented above provides a

596: complement to D. Deutsch's argument from a logical point of view.

597: 

598: \bigskip\

599: 

600: \textbf{2. Quantum Logic}

601: 

602: \smallskip\

603: 

604: The aim of this section is to recall some basic notions and

605: results about quantum logic needed in the subsequent sections and

606: to fix notations. In this paper, quantum logic is understood as a

607: complete orthomodular lattice-valued logic. This section is mainly

608: concerned with the semantic aspect of such a logic, and it will be

609: divided into four subsections. The first subsection will briefly

610: review some fundamental results on orthomodular lattices; for more

611: details, we refer to [Ka83] and [BH00]. In the second one we will

612: introduce the language of first-order quantum logic. The third

613: will discuss the algebraic semantics of first-order quantum logic.

614: Some useful properties of orthomodular lattice-valued sets are

615: given in the fourth subsection.

616: 

617: \smallskip\

618: 

619: \textbf{2.1. Orthomodular Lattices}

620: 

621: \smallskip\

622: 

623: The set of truth values of a quantum logic will be taken to be an

624: orthomodular lattice. So we first introduce the notion of

625: orthomodular lattice. An ortholattice is a 7-tuple

626: $$\ell =<L,\leq ,\wedge ,\vee ,\bot ,0,1>$$ where:

627: 

628: (1) $<L,\leq ,\wedge ,\vee ,0,1>$ is a bounded lattice, $0,1$ are

629: the least and greatest elements of $L,$ respectively, $\leq $ is

630: the partial ordering in $L,$ and for any $a,b\in L,$ $a\wedge b,$

631: and $a\vee b$ stand for the greatest lower bound and the least

632: upper bound of $a$ and $b$, respectively;

633: 

634: (2) $\bot $ is a unary operation on $L,$ called orthocomplement,

635: and required to satisfy the following conditions: for any $a,b\in

636: L$,

637: 

638: \ \ \ (i) $a\wedge a^{\bot }=0,\ a\vee a^{\bot }=1;$

639: 

640: \ \ \ (ii) $a^{\bot \bot }=a;$ and

641: 

642: \ \ \ (iii) $a\leq b$ implies $b^{\bot }\leq a^{\bot }.$

643: 

644: It is easy to see that the condition (iii) is equivalent to one of

645: the De Morgan laws: for any $a,b\in L$,

646: 

647: \ \ \ (iii') $(a\wedge b)^{\bot} = a^{\bot}\vee b^{\bot},\ (a\vee

648: b)^{\bot} = a^{\bot}\wedge b^{\bot}.$

649: 

650: Let $\ell =<L,\leq ,\wedge ,\vee ,\bot ,0,1>$ be an ortholattice,

651: and let $a,b\in L$. We say that $a$ commutes with $b$, in symbols

652: $aCb$, if $$a=(a\wedge b)\vee (a\wedge b^{\bot}).$$

653: 

654: An orthomodular lattice is an ortholattice $\ell =<L,\leq ,\wedge

655: ,\vee ,\bot ,0,1>$ satisfying the orthomodular law: for all

656: $a,b\in L$,

657: 

658: \ \ \ (iv) $a\leq b\ {\rm implies}\ a\vee (a^{\bot}\wedge b)=b.$

659: 

660: The orthomodular law can be replaced by the following equation:

661: 

662: \ \ \ (iv') $a\vee (a^{\bot }\wedge (a\vee b))=a\vee b\ {\rm for\

663: any}\ a,b\in L.$

664: 

665: A Boolean algebra is an ortholattice $\ell =<L,\leq ,\wedge ,\vee

666: ,\bot ,0,1>$ fulfilling the distributive law of join over meet:

667: for all $a,b,c\in L$,

668: 

669: \ \ \ (v) $a\vee (b\wedge c)=(a\vee b)\wedge (a\vee c).$

670: 

671: With the De Morgan law it is easy to know that the condition (v)

672: is equivalent to the distributive law of meet over join: for any

673: $a,b,c\in L$,

674: 

675: \ \ \ (v') $a\wedge (b\vee c)=(a\wedge b)\vee (a\wedge c).$

676: 

677: Obviously, the distributive law implies the orthomodular law, and

678: so a Boolean algebra is an orthomodular lattice.

679: 

680: The following lemma gives a characterization of orthomodular

681: lattices and it distinguishes orthomodular lattices from

682: ortholattices.

683: 

684: \smallskip\

685: 

686: \textbf{Lemma 2.1.} ([BH00], Propositions 2.1 and 2.2) Let $\ell

687: =<L,\leq ,\wedge ,\vee ,\bot ,0,1>$ be an ortholattice. Then the

688: following seven statements are equivalent:

689: 

690: (1) $\ell$ is an orthomodular lattice;

691: 

692: (2) For any $a,b\in L$, if $a\leq b$ and $a^{\bot}\wedge b=0$ then

693: $a=b$;

694: 

695: (3) For any $a,b\in L$, if $aCb$ then $bCa$;

696: 

697: (4) For any $a,b\in L$, if $aCb$ then $a^{\bot}Cb$;

698: 

699: (5) For any $a,b\in L$, if $aCb$ then $a\vee (a^{\bot}\wedge

700: b)=a\vee b$;

701: 

702: (6) The benzene ring $O_6$ (see Figure 1) is not a subalgebra of

703: $\ell$.

704: \begin{figure}\centering

705: \includegraphics{fig_1.eps}

706: \caption{Benzene ring} \label{fig 1 }

707: \end{figure}

708: 

709: (7) For any $a,b\in L$, if $a\leq b$ then the subalgebra $[a,b]$

710: of $\ell$ generated by $a$ and $b$ is a Boolean

711: algebra.$\heartsuit$

712: 

713: \smallskip\

714: 

715: The set of truth values of classical logic is a Boolean algebra;

716: whereas quantum logic is an orthomodular lattice-valued logic. It

717: is well-known that a Boolean algebra must be an orthomodular

718: lattice, but the inverse is not true. Thus, quantum logic is

719: weaker than classical logic. The major difference between a

720: Boolean algebra and an orthomodular lattice is that distributivity

721: is not valid in the latter. However, many cases still appeal an

722: application of the distributivity even when we manipulate elements

723: in an orthomodular lattice. This requires us to regain a certain

724: (weaker) version of distributivity in the realm of orthomodular

725: lattices. The key technique for this purpose is commutativity

726: which is able to provide a localization of distributivity. The

727: following lemma together with Lemma 2.1(4) indicates that

728: commutativity is preserved by all operations of orthomodular

729: lattice.

730: 

731: \smallskip\

732: 

733: \textbf{Lemma 2.2}. ([BH00], Proposition 2.4) Let $\ell =<L,\leq

734: ,\wedge ,\vee ,\bot ,0,1>$ be an orthomodular lattice, and let

735: $a\in L$ and $b_i\in L$ $(i\in I)$. If $aCb_i$ for any $i\in I$,

736: then $$aC\wedge_{i\in I}b_i\ {\rm and}\ aC\vee_{i\in I}b_i$$

737: provided $\wedge_{i\in I}b_i$ and $\vee_{i\in I}b_i$

738: exist.$\heartsuit$

739: 

740: \smallskip\

741: 

742: The local distributivity implied by commutativity is then given by

743: the following

744: 

745: \smallskip\

746: 

747: \textbf{Lemma 2.3}. ([BH00], Proposition 2.3) Let $\ell =<L,\leq

748: ,\wedge ,\vee ,\bot ,0,1>$ be an orthomodular lattice and let

749: $A\subseteq L$. For any $a\in A$ and $b_i\in A$ $(i\in I)$, if

750: $aCb_i$ for all $i\in I$, then

751: $$a\wedge \vee_{i\in I}b_i=\vee_{i\in I}(a\wedge b_i),$$

752: $$a\vee \wedge_{i\in I}b_i=\wedge_{i\in I}(a\vee b_i)$$

753: provided $\wedge_{i\in I} b_i$ and $\vee_{i\in I} b_i$

754: exist.$\heartsuit$

755: 

756: \smallskip\

757: 

758: The above lemma is very useful, and it often enables us to recover

759: distributivity in an orthomodular lattice. However, its condition

760: that all elements involved commute each other is quite strong, and

761: not easy to meet. This suggests us to find a way to weaken this

762: condition. One solution was found by G. Takeuti [T81], and he

763: introduced the notion of commutator which can be seen as an index

764: measuring the degree to which the commutativity is valid.

765: 

766: \smallskip\

767: 

768: \textbf{Definition 2.1}. ([T81], pages 305 and 307) Let $\ell

769: =<L,\leq ,\wedge ,\vee ,\bot ,0,1>$ be an orthomodular lattice and

770: let $A\subseteq L$.

771: 

772: (1) If $A$ is finite, then the commutator $\gamma (A)$ of $A$ is

773: defined by

774: $$\gamma (A)=\vee\{\wedge_{a\in A}a^{f(a)}:f\ {\rm is\ a\ mapping\ from}\ A\ {\rm into}\

775: \{1,-1\}\},$$ where $a^{1}$ denotes $a$ itself and $a^{-1}$

776: denotes $a^{\bot}$.

777: 

778: (2) The strong commutator $\Gamma (A)$ of $A$ is defined by

779: $$\Gamma (A)=\vee\{b: C(a,b)\ {\rm for\ all}\ a\in A\ {\rm and}\

780: C(a_1\wedge b, a_2\wedge b)\ {\rm for\ all}\ a_1, a_2\in A\}.$$

781: 

782: \smallskip\

783: 

784: The relation  between commutator and strong commutator is

785: clarified by the following lemma. In addition, the third item of

786: the following lemma shows that commutator is a relativization of

787: the notion of commutativity.

788: 

789: \smallskip\

790: 

791: \textbf{Lemma 2.4}. ([T81], Proposition 4 and its corollary) Let

792: $\ell =<L,\leq ,\wedge ,\vee ,\bot ,0,1>$ be an orthomodular

793: lattice and let $A\subseteq L$. Then

794: 

795: (1) $\Gamma(A)\leq \gamma(A)$.

796: 

797: (2) If $A$ is finite, then $\Gamma(A)= \gamma(A)$.

798: 

799: (3) $\gamma(A)=1$ if and only if all the members of $A$ are

800: mutually commutable.$\heartsuit$

801: 

802: \smallskip\

803: 

804: We now can present a generalization of Lemma 2.3 by using the tool

805: of commutator. It is easy to see from Lemmas 2.4(2) and (3) that

806: the following lemma degenerates to Lemma 2.3 when $aCb_i$ for all

807: $i\in I$.

808: 

809: \smallskip\

810: 

811: \textbf{Lemma 2.5}. ([T81], Propositions 5 and 6) Let $\ell

812: =<L,\leq ,\wedge ,\vee ,\bot ,0,1>$ be an orthomodular lattice and

813: let $A\subseteq L$. Then for any $a\in A$ and $b_i\in A$ $(i\in

814: I)$,

815: $$\Gamma(A)\wedge (a\wedge \vee_{i\in I}b_i)\leq \vee_{i\in I}(a\wedge b_i),$$

816: $$\Gamma(A)\wedge \wedge_{i\in I}(a\vee b_i)\leq a\vee \wedge_{i\in I}b_i.\heartsuit$$

817: 

818: \smallskip\

819: 

820: Suppose that we want to use the above lemma on a formula of the

821: form $a\wedge \vee_{i\in I}b_i$ or $a\vee \wedge_{i\in I}b_i$ in

822: order to get a local distributivity. In many situations, the

823: elements $a$ and $b_i$ $(i\in I)$ may be very complicated, and the

824: operations $\bot$, $\wedge$ and $\vee$ are involved in them. Then

825: the above lemma cannot be applied directly, and it needs the help

826: of the following

827: 

828: \smallskip\

829: 

830: \textbf{Lemma 2.6}. Let $\ell =<L,\leq ,\wedge ,\vee ,\bot ,0,1>$

831: be an orthomodular lattice and let $A\subseteq L$. Then for any

832: $B\subseteq [A]$ we have $$\Gamma (A)\leq \Gamma (B),$$ where

833: $[A]$ stands for the subalgebra of $\ell$ generated by $A$.

834: 

835: \smallskip\

836: 

837: \textbf{Proof}. For any $X\subseteq L$, we write

838: $$K(X)=\{b\in L:aCb\ {\rm and}\ (a_1\wedge b)C(a_2\wedge b)\

839: {\rm for\ all}\ a, a_1, a_2 \in X \}$$ Furthermore, we set $A_0=A$

840: and

841: $$A_{i+1} = A_i \cup \{a^{\bot}: a\in A_i\}\cup\{a_1\wedge a_2:

842: a_1, a_2\in A_i\}\ (i=0,1,2,...)$$

843: 

844: First, we prove that $K(A_i)=K(A)$ for all $i\geq 0$ by induction

845: on $i$. It is obvious that $K(A_{i+1})\subseteq K(A)$. Conversely,

846: suppose that $b\in K(A)$ and we want to show that $b\in

847: K(A_{i+1})$. It is easy to see that $aCb$ for any $a\in A_{i+1}$.

848: Thus, we only need to demonstrate the following

849: 

850: \textit{Claim:} $(a_1\wedge b)C(a_2\wedge b)$ for any $a_1, a_2\in

851: A_{i+1}$.

852: 

853: The essential part of the proof of the above claim is the

854: following two cases, and the other cases are clear, or can be

855: treated as iterations of them:

856: 

857: Case 1. $a_1\in A_i$, $a_2=c_1\wedge c_2$ and $c_1, c_2\in A_i$.

858: From the induction hypothesis we have $$(a_1\wedge b)C(c_1\wedge

859: b)\ {\rm and}\ (a_1\wedge b)C(c_2\wedge b).$$ This yields

860: $$(a_1\wedge b)C(c_1\wedge b)\wedge (c_2\wedge b)=(c_1\wedge

861: c_2)\wedge b=a_2\wedge b.$$

862: 

863: Case 2. $a_1\in A_i$, $a_2=c^{\bot}$ and $c\in A_i$. Then from the

864: induction hypothesis we obtain $(a_1\wedge b)C(c\wedge b)$, and

865: further $(a_1\wedge b)C(c\wedge b)^{\bot}$ by using Lemma 2.1(4).

866: In addition, $(a_1\wedge b)Cb$. This together with Lemma 2.2

867: yields $(a_1\wedge b)Cb\wedge(c\wedge b)^{\bot}$. Note that $cCb$

868: and so $b^{\bot}Cc^{\bot}$. Then by Lemma 2.3 we assert that

869: $$b^{\bot}\vee(c\wedge b)=b^{\bot}\vee c\ {\rm and}\ b\wedge (c\wedge

870: b)^{\bot}=b\wedge c^{\bot}$$. Hence, it follows that $(a_1\wedge

871: b)Cb\wedge c^{\bot}=a_2\wedge b.$

872: 

873: We now write $$A_\infty = \cup_{i=0}^{\infty}A_i.$$ Then

874: $$K(A_\infty)=\cap_{i=0}^{\infty}K(A_i)=K(A).$$ It is easy to see

875: that $A\subseteq A_\infty$ is a subalgebra of $\ell$. So,

876: $[A]\subseteq A_\infty$, $$K(A)=K(A_\infty)\subseteq

877: K([A])\subseteq K(B),$$ and $$\Gamma (A)=\vee K(A)\leq \vee

878: K(B)=\Gamma (B).\heartsuit$$

879: 

880: \smallskip\

881: 

882: As stated in the introduction, the aim of this paper is to develop

883: a theory of computation based on quantum logic. The logical

884: language for a theory of computation has to contain the universal

885: and existential quantifiers, and the two quantifiers are usually

886: interpreted as (infinite) meet and join, respectively. Hence, we

887: should assume that the lattice of the truth values of our quantum

888: logic is complete. A complete orthomodular lattice is an

889: orthomodular lattice $\ell =<L,\leq ,\wedge ,\vee ,\bot ,0,1>$ in

890: which for any $M\subseteq L,$ both the greatest lower bound

891: $\wedge M$ and the least upper bound $\vee M$ exist.

892: 

893: The function of a logic is provide us with a certain reasoning

894: ability, and the implication connective is an intrinsic

895: representative of inference within the logic. Thus each logic

896: should reasonably contain a connective of implication. To make a

897: complete orthomodular lattice available as the set of truth values

898: of quantum logic, we need to define a binary operation, called

899: implication operator, on it such that this operation may serve as

900: the interpretation of implication in this logic. Unfortunately, it

901: is a very vexed problem to define a reasonable implication

902: operator for quantum logic. All implication operators that one can

903: reasonably introduce in an orthomodular lattice are more or less

904: anomalous in the sense that they do not share most of the

905: fundamental properties of the implication in classical logic. This

906: is different from the cases of most weak logics. (For a thorough

907: discussion on the implication problem in quantum logic, see

908: [DC86], Section 3.)

909: 

910: A minimal condition for an implication operator $\rightarrow$ is

911: the requirement proposed by G. Birkhoff and J. von Neumann [BN36]:

912: $$a\rightarrow b=1\ {\rm if\ and\ only\ if}\ a\leq b$$ for any $a,b\in L$.

913: Usually in a logic, there are two ways in which implication is

914: introduced. The first one is to treat implication as a derived

915: connective; that is, implication is explicitly defined in terms of

916: other connectives such as negation, conjunction and disjunction.

917: All implications of this kind were found by G. Kalmbach [Ka74],

918: and they are presented by the following:

919: 

920: \smallskip\

921: 

922: \textbf{Lemma 2.7}. ([Ka74]; see also [Ka83], Theorem 15.3) The

923: orthomodular lattice freely generated by two elements is

924: isomorphic to $2^{4}\times MO2$, where $2$ stands for the Boolean

925: algebra of two elements. The elements of $2^{4}\times MO2$

926: satisfying the Birkhoff-von Neumann requirement are exactly the

927: following five polynomials of two variables:

928: $$a\rightarrow_1 b=(a^{\bot}\wedge b)\vee (a^{\bot}\wedge b^{\bot})\vee (a\wedge (a^{\bot}\vee b)),$$

929: $$a\rightarrow_2 b=(a^{\bot}\wedge b)\vee (a\wedge b)\vee ((a^{\bot}\vee b)\wedge b^{\bot}),$$

930: $$a\rightarrow_3 b=a^{\bot}\vee (a\wedge b),$$

931: $$a\rightarrow_4 b=b\vee (a^{\bot}\wedge b^{\bot}),$$

932: $$a\rightarrow_5 b=(a^{\bot}\wedge b)\vee (a\wedge b)\vee (a^{\bot}\wedge b^{\bot}).\heartsuit$$

933: 

934: \smallskip\

935: 

936: Obviously, this lemma implies that the above five polynomials are

937: all implication operators definable in orthomodular lattices. It

938: was shown by G. Kalmbach [Ka74, Ka83] that the orthomodular

939: lattice-valued (propositional) logic can be (finitely)

940: axiomatizable by using the modus ponens with

941: implication$\rightarrow_1$ as the only one rule of inference, but

942: the same conclusion does not hold for the other implications

943: $\rightarrow_i$ $(2\leq i\leq 5).$

944: 

945: We may also define the material conditional $\rightarrow_0$ in an

946: orthomodular $\ell=<L,\leq ,\wedge ,\vee ,\bot ,0,1>$ by

947: $$a\rightarrow _0 b=a^{\bot}\vee b$$

948: for all $a,b\in L.$ It is easy to see that $\rightarrow_0$ does

949: not fulfil the Birkhoff-von Neumann requirement. On the other

950: hand, the following lemma shows that the five implication

951: operators given in Lemma 2.7 degenerate to the material

952: conditional whenever the two operands are compatible.

953: 

954: \smallskip\

955: 

956: \textbf{Lemma 2.8}. ([DC86], Theorem 3.2) Let $\ell =<L,\leq

957: ,\wedge ,\vee ,\bot ,0,1>$ be an orthomodular lattice. Then for

958: any $a,b\in L$, $$a\rightarrow_i b=a\rightarrow_0 b$$ if and only

959: if $aCb$, where $1\leq i\leq 5.\heartsuit$

960: 

961: \smallskip\

962: 

963: The second way of defining an implication is to take its truth

964: function as the adjunctor (i.e., residuation) of the truth

965: function of conjunction. Note that in this case the implication is

966: usually not definable from negation, conjunction and disjunction,

967: and it has been treated as a primitive connective. Indeed, L.

968: Herman, E. Marsden and R. Piziak [HMP75] introduced an implication

969: in the style of residuation. Furthermore, the following lemma

970: shows that the five polynomial implication operators

971: $\rightarrow_i$ $(1\leq i\leq 5)$ cannot be defined as the

972: residuation of the conjunction unless $\ell$ is a Boolean algebra.

973: 

974: \smallskip\

975: 

976: \textbf{Lemma 2.9}. ([DC86], the revised version, page 25) Let

977: $\ell =<L,\leq ,\wedge ,\vee ,\bot ,0,1>$ be an orthomodular

978: lattice, and let $1\leq i\leq 5$. Then the following two

979: statements are equivalent:

980: 

981: (i) $\ell$ is a Boolean algebra.

982: 

983: (ii) the import-export law: for all $a,b\in L$,

984: $$a\wedge b\leq c\ {\rm if\ and\ only\ if}\ a\leq b\rightarrow_i c.\heartsuit$$

985: 

986: \smallskip\

987: 

988: Among the five orthomodular polynomial implications,

989: $\rightarrow_3$, named the Sasaki-hook, has often been preferred

990: since it enjoys some properties resembling those in intuitionistic

991: logic. The Sasaki-hook was originally introduced by P. D. Finch

992: [Fi70]. For a detailed discussion of the Sasaki-hook, see L.

993: Rom\'{a}n and B. Rumbos [RR91] and L. Rom\'{a}n and R. E. Zuazua

994: [RZ99]. Here we first point out that the Sasaki-hook possesses a

995: modification of residual characterization although it is defined

996: as a polynomial in orthomodular lattice. A weakening of the

997: import-export law is the resulting condition, called compatible

998: import-export law, by restricting the import-export law for any

999: $a,b\in L$ with $aCb$; that is, if $aCb$, then $a\wedge b\leq c$

1000: if and only if $a\leq b\rightarrow c$.

1001: 

1002: \smallskip\

1003: 

1004: \textbf{Lemma 2.10}. ([T81], Proposition 1 and its corollary;

1005: [DC86], the revised version, page 25) Let $\ell =<L,\leq ,\wedge

1006: ,\vee ,\bot ,0,1>$ be an orthomodular lattice, and let $a,$ $b$,

1007: $c\in L$. Then

1008: $$a\rightarrow b=\vee \{x:xCa\ {\rm and}\ x\wedge a\leq b\}.$$

1009: Moreover, among the five implications $\rightarrow_i$ $(1\leq

1010: i\leq 5)$, the Sasaki-hook $\rightarrow_3$ is the only one

1011: satisfying the compatible import-export law.$\heartsuit$

1012: 

1013: \smallskip\

1014: 

1015: Our mathematical reasoning frequently require that implication

1016: relation is preserved by conjunction and disjunction. Also, the

1017: negation is needed to be compatible with implication in the sense

1018: that the negation can reverse the direction of implication. And,

1019: to warrant the validity of a chain of inferences, the transitivity

1020: of implication is required. However, this is not the case in

1021: general if we are working in an orthomodular lattice. Fortunately,

1022: if we adopt the Sasaki-hook, then these properties of implication

1023: can be recovered by attaching a certain commutator.

1024: 

1025: \smallskip\

1026: 

1027: \textbf{Lemma 2.11.} Let $\ell =<L,\leq ,\wedge ,\vee ,\perp

1028: ,0,1>$ be an orthomodular lattice. Then

1029: 

1030: (1) for any $a_{i},b_{i}\in L$ $(i=1,...,n),$ let

1031: $X=\{a_{1},...,a_{n}\}\cup \{b_{1},...,b_{n}\},$

1032: $$\Gamma

1033: (X)\wedge \wedge _{i=1}^{n}(a_{i}\rightarrow _{3}b_{i})\leq \wedge

1034: _{i=1}^{n}a_{i}\rightarrow _{3}\wedge _{i=1}^{n}b_{i},$$

1035: $$\Gamma (X)\wedge \wedge _{i=1}^{n}(a_{i}\rightarrow

1036: _{3}b_{i})\leq \vee _{i=1}^{n}a_{i}\rightarrow _{3}\vee

1037: _{i=1}^{n}b_{i}.$$

1038: 

1039: (2) for any $a,b\in L$, $$\Gamma (a,b)\wedge (a\rightarrow

1040: _{3}b)\leq b^{\perp }\rightarrow _{3}a^{\perp }.$$

1041: 

1042: (3) for any $a,b,c\in L,$

1043: $$\Gamma (a,b,c)\wedge (a\rightarrow _{3}b)\wedge (b\rightarrow

1044: _{3}c)\leq a\rightarrow _{3}c.$$

1045: 

1046: \smallskip\

1047: 

1048: \textbf{Proof.} (1) We only prove the first inequality, and the

1049: proof of the second is similar. With Lemmas 2.5 and 2.6 we obtain

1050: $$\wedge

1051: _{i=1}^{n}a_{i}\rightarrow _{3}\wedge _{i=1}^{n}b_{i}=(\wedge

1052: _{i=1}^{n}a_{i})^{\perp }\vee (\wedge _{i=1}^{n}a_{i}\wedge \wedge

1053: _{i=1}^{n}b_{i})$$

1054: $$=\vee _{i=1}^{n}a_{i}{}^{\perp }\vee \wedge

1055: _{i=1}^{n}(a_{i}\wedge b_{i})$$

1056: $$\geq \Gamma (X)\wedge \wedge

1057: _{i=1}^{n}(\vee _{j=1}^{n}a_{j}{}^{\perp }\vee (a_{i}\wedge

1058: b_{i}))$$

1059: $$\geq \Gamma (X)\wedge \wedge _{i=1}^{n}(a_{i}{}^{\perp }\vee

1060: (a_{i}\wedge b_{i}))$$

1061: $$=\Gamma (X)\wedge \wedge

1062: _{i=1}^{n}(a_{i}\rightarrow b_{i}).$$

1063: 

1064: (2) First, we note that $a\wedge b,$ $a^{\perp }\wedge b,$ $

1065: a^{\perp }\wedge b^{\perp }\leq b\vee (a^{\perp }\wedge b^{\perp

1066: })=b^{\perp }\rightarrow _{3}a^{\perp }.$ Thus,

1067: $$\Gamma (a,b)=(a\wedge b)\vee (a\wedge b^{\perp })\vee (

1068: a^{\perp }\wedge b)\vee (a^{\perp }\wedge b^{\perp })$$

1069: $$\leq (b^{\perp }\rightarrow _{3}a^{\perp })\vee (a\wedge b^{\perp

1070: }),$$ and furthermore with Lemmas 2.5 and 2.6 we have

1071: $$\Gamma (a,b)\wedge (a\rightarrow _{3}b)=\Gamma (a,b)\wedge

1072: (a^{\perp }\vee (a\wedge b))$$

1073: $$\leq \Gamma (a,b)\wedge (a^{\perp }\vee b)$$

1074: $$=\Gamma (a,b)\wedge \Gamma (a,b)\wedge (a^{\perp }\vee b)$$

1075: $$\leq \Gamma (a,b)\wedge \lbrack (b^{\perp }\rightarrow

1076: _{3}a^{\perp })\vee (a\wedge b^{\perp })]\wedge (a^{\perp }\vee

1077: b)$$

1078: $$\leq \ [(b^{\perp }\rightarrow _{3}a^{\perp })\wedge (a^{\perp

1079: }\vee b)]\vee \lbrack (a\wedge b^{\perp })\wedge (a^{\perp }\vee

1080: b)]$$

1081: $$\leq (b^{\perp }\rightarrow _{3}a^{\perp })\vee \lbrack (a\wedge

1082: b^{\perp })\wedge (a^{\perp }\vee b)].$$ Note that $(a\wedge

1083: b^{\perp })^{\perp }=a^{\perp }\vee b$ and $(a\wedge b^{\perp

1084: })\wedge (a^{\perp }\vee b)=0.$ Then

1085: $$\Gamma (a,b)\wedge (a\rightarrow _{3}b)\leq b^{\perp }\rightarrow

1086: _{3}a^{\perp }.$$

1087: 

1088: (3) Again, we use Lemmas 2.5 and 2.6. This enables us to assert

1089: that

1090: $$\Gamma

1091: (a,b,c)\wedge (a\rightarrow _{3}b)\wedge (b\rightarrow

1092: _{3}c)=\Gamma (a,b,c)\wedge (a^{\perp }\vee (a\wedge b))\wedge

1093: (b^{\perp }\vee (b\wedge c)) $$

1094: $$\leq \Gamma (a,b,c)\wedge

1095: ([a^{\perp }\wedge (b^{\perp }\vee (b\wedge c))]\vee \lbrack

1096: (a\wedge b)\wedge (b^{\perp }\vee (b\wedge c))])$$

1097: $$\leq \Gamma

1098: (a,b,c)\wedge (a^{\perp }\vee \lbrack (a\wedge b)\wedge (b^{\perp

1099: }\vee (b\wedge c))]).$$

1100: 

1101: We note that $\Gamma (a,b,c)Ca^{\perp }$ and $$\Gamma

1102: (a,b,c)C[(a\wedge b)\wedge (b^{\perp }\vee (b\wedge c))]).$$ Then

1103: $$\Gamma (a,b,c)\wedge (a\rightarrow _{3}b)\wedge (b\rightarrow

1104: _{3}c)\leq (\Gamma (a,b,c)\wedge a^{\perp })\vee (\Gamma

1105: (a,b,c)\wedge \lbrack (a\wedge b)\wedge (b^{\perp }\vee (b\wedge

1106: c))])$$

1107: $$\leq a^{\perp }\vee (\Gamma (a,b,c)\wedge \lbrack (a\wedge

1108: b)\wedge (b^{\perp }\vee (b\wedge c))])$$

1109: $$\leq a^{\perp }\vee

1110: \lbrack (a\wedge b)\wedge b^{\perp }]\vee \lbrack (a\wedge

1111: b)\wedge (b\wedge c)]$$

1112: $$=a^{\perp }\vee \lbrack (a\wedge b)\wedge

1113: (b\wedge c)]$$

1114: $$\leq a^{\perp }\vee (a\wedge c)$$

1115: $$=a\rightarrow _{3}c.\heartsuit$$

1116: 

1117: \smallskip\

1118: 

1119: For simplicity of presentation, we finally introduce an

1120: abbreviation. For each implication operator $\rightarrow$, the

1121: bi-implication operator on $\ell $ is defined as follows:

1122: $$a\leftrightarrow b\stackrel{def}{=}(a\rightarrow b)\wedge

1123: (b\rightarrow a)$$ for any $a,b\in L.$

1124: 

1125: \smallskip\

1126: 

1127: \textbf{2.2. The Language of Quantum Logic}

1128: 

1129: \smallskip\

1130: 

1131: In this subsection we present the syntax of quantum logic. Given a

1132: complete orthomodular lattice $\ell =<L,\leq ,\wedge ,\vee ,\bot

1133: ,0,1>.$ We require that the language of an $\ell -$valued

1134: (quantum) logic possesses a nullary connective $ \mathbf{a}$ for

1135: each $a\in L$ as well as three other primitive connectives: an

1136: unary one $\lnot $ (negation) and two binary ones $\wedge $

1137: (conjunction), $\rightarrow$ (implication). The language also has

1138: a primitive quantifier $\forall $ (universal quantifier).

1139: 

1140: It deserves an explanation for our design decision of choosing

1141: implication as a primitive connective. In the sequel, many results

1142: only need to suppose that the implication operator satisfies the

1143: Birkhoff-von Neumann requirement. It is known that there are five

1144: polynomials fulfilling the Birkhoff-von Neumann requirement. If we

1145: treated implication as a derived connective defined in terms of

1146: negation, conjunction and disjunction, then it would be necessary

1147: to assume five different connectives of implication in our logical

1148: language. This would often complicate our presentation very much.

1149: On the other hand, in some cases, the Birkhoff-von Neumann

1150: condition is not enough and it requires the implication operator

1151: to be the Sasaki-hook. So, we decide to use implication as a

1152: primitive connective, and specify it when needed.

1153: 

1154: The syntax of $\ell-$valued logic is defined in a familiar way; we

1155: omit its details. To simplify the notations in what follows, it is

1156: necessary to introduce several derived formulas:

1157: 

1158: (i) $\varphi \vee \psi \stackrel{def}{=}\lnot (\lnot \varphi

1159: \wedge \lnot \psi );$

1160: 

1161: (ii) $\varphi \leftrightarrow \psi \stackrel{def}{=}(\varphi

1162: \rightarrow \psi )\wedge (\psi \rightarrow \varphi );$

1163: 

1164: (iii) $(\exists x)\varphi \stackrel{def}{=}\lnot (\forall x)\lnot

1165: \varphi ;$

1166: 

1167: (iv) $A\subseteq B\stackrel{def}{=}(\forall x)(x\in A\rightarrow

1168: x\in B);$ and

1169: 

1170: (v) $A\equiv B\stackrel{def}{=}(A\subseteq B)\wedge (B\subseteq

1171: A).$

1172: 

1173: Suppose that $\Delta$ is a finite set of formulas. The commutator

1174: of $\Delta$ is defined to be

1175: $$\gamma(\Delta)\stackrel{def}{=}\vee\{\wedge_{\varphi\in\Delta}

1176: \varphi^{f(\varphi)}:f\in \{1,-1\}^{\Delta}\},$$ where

1177: $\varphi^{1},\ \varphi^{-1}$ express $\varphi$ and $\lnot\varphi,$

1178: respectively. It is obvious that the above formula is the

1179: counterpart of Definition 2.1(1) in the language of our quantum

1180: logic.

1181: 

1182: \smallskip\

1183: 

1184: \textbf{2.3. The Algebraic Semantics of Quantum Logic}

1185: 

1186: \smallskip\

1187: 

1188: We now turn to give the semantics of quantum logic. There are

1189: several different versions of semantics for quantum logic; for

1190: example, quantum logic enjoys a semantics in the Kripke style

1191: [DC86; RS00]. What concerns us here is its algebraic semantics.

1192: Assume that $\ell =<L,\leq ,\wedge ,\vee ,\bot ,0,1>$ be an

1193: orthomodular lattice equipped with additionally a binary operation

1194: $\rightarrow$ over it. The operation $\rightarrow$ is required to

1195: be suited to serve as the truth function of implication

1196: connective. According to our explanation of the connective of

1197: implication in the last subsection, we leave the operation

1198: $\rightarrow$ unspecified but suppose that it satisfies the

1199: Birkhoff-von Neumann requirement. An $\ell -$valued interpretation

1200: is an interpretation in which every predicate symbol is associated

1201: with an $ \ell -$valued relation, i.e., a mapping from the product

1202: of some copies of the discourse universe into $L,$ where the

1203: number of copies is exactly the arity of the predicate symbol. The

1204: other items in $\ell-$valued logical language are interpreted as

1205: usual. For every (well-formed) formula $\varphi ,$ its truth value

1206: $\lceil \varphi \rceil$ is assumed in $L,$ and the truth valuation

1207: rules for logical and set-theoretical formulas are given as

1208: follows:

1209: 

1210: (i) $\lceil \mathbf{a}\rceil =a;$

1211: 

1212: (ii) $\lceil \lnot \varphi \rceil =\lceil \varphi \rceil ^{\bot

1213: };$

1214: 

1215: (iii) $\lceil \varphi \wedge \psi \rceil =\lceil \varphi \rceil

1216: \wedge \lceil \psi \rceil ;$

1217: 

1218: (iv) $\lceil \varphi \rightarrow \psi \rceil =\lceil \varphi

1219: \rceil \rightarrow \lceil \psi \rceil ;$

1220: 

1221: (v) if $U$ is the universe of discourse, then

1222: $$\lceil (\forall x)\varphi (x)\rceil =\wedge _{u\in U}\lceil

1223: \varphi (u)\rceil ;$$ and

1224: 

1225: (vi) $\lceil x\in A\rceil =A(x),$ where $A$ is a set constant

1226: (unary predicate symbol) and it is interpreted as a mapping, also

1227: denoted as $A,$ from the universe into $L,$ i.e., an $ \ell

1228: -$valued set (more exactly, an $\ell -$valued subset of the

1229: universe).

1230: 

1231: Note that in the above truth valuation rules $\wedge $ and $\vee $

1232: in the left-hand side are connectives in quantum logic whereas

1233: $\wedge $ and $\vee $ in the right-hand side stand for operations

1234: in the orthomodular lattice $ \ell $ of truth values. Also, the

1235: symbol $\rightarrow$ in the left-hand side of (iv) is a connective

1236: in the language of quantum logic, but the symbol $\rightarrow$ in

1237: the right-hand side of (iv) is the binary operation attached to

1238: $\ell$ that is explained at the beginning of this subsection.

1239: 

1240: As we claimed in the introduction, quantum logic will act as our

1241: meta-logic in the theory of computation developed in this paper.

1242: Then we still have to introduce several meta-logical notions for

1243: quantum logic. For every orthomodular lattice $\ell =<L,\leq

1244: ,\wedge ,\vee ,\bot ,0,1>,$ if $\Gamma $ is a set of formulas and

1245: $\varphi $ a formula, then $\varphi $ is a semantic consequence of

1246: $\Gamma $ in $\ell -$valued logic, written $\Gamma \stackrel{\ell

1247: }{\models }\varphi ,$ whenever $$\wedge _{\psi \in \Gamma }\lceil

1248: \psi \rceil \leq \lceil \varphi \rceil $$ for all $\ell -$valued

1249: interpretations. In particular, $\stackrel{\ell }{\models }\varphi

1250: $ means that $\phi \stackrel{\ell }{\models }\varphi ,$ i.e.,

1251: $\lceil \varphi \rceil =1$ always holds for every $\ell -$valued

1252: interpretation; in other words, $1$ is the unique designated truth

1253: value in $\ell .$ Furthermore, if $\Gamma \stackrel{ \ell

1254: }{\models }\varphi $ (resp. $\stackrel{\ell }{\models }\varphi $)

1255: for all orthomodular lattice $\ell $ then we say that $\varphi $

1256: is a semantic consequence of $\Gamma $ (resp. $\varphi $ is valid)

1257: in quantum logic and write $\Gamma \models \varphi $ (resp.

1258: $\models \varphi $).

1259: 

1260: We here are not going to give a detailed exposition on quantum

1261: logic, but would like to point out that quantum logic gives rise

1262: to many counterexamples to some meta-logical properties which hold

1263: for classical logic and for a large class of weaker logics; for

1264: example, M. L. Dalla Chiara [DC81] showed that a minimal version

1265: of quantum logic fails to enjoy the Lindenbaum property, and J.

1266: Malinowski [Ma90] found that the deduction theorem fails in

1267: quantum logic and some of its variants.

1268: 

1269: \smallskip\

1270: 

1271: \textbf{2.4. The Operations of Quantum Sets}

1272: 

1273: \smallskip\

1274: 

1275: Beside the language of quantum logic introduced in Section 2.2, we

1276: will also need some notations such as $\in $ (membership) from

1277: set-theoretical language in our study of computing theory based on

1278: quantum logic. As mentioned in the introduction, a theory of

1279: quantum sets has already been developed by G. Takeuti [T81]. A

1280: careful review of quantum set theory is out of the scope of the

1281: present paper. What mainly concerned G. Takeuti [T81] is how some

1282: axioms of classical set theory could be modified so that they will

1283: holds in the framework of quantum logic. In other words, he tried

1284: to clarify the relation of quantum set theory with the classical

1285: mathematics. Here, we instead propose some operations of

1286: $\ell-$valued sets and also introduce several notations for

1287: $\ell-$valued sets. These are needed in the subsequent sections.

1288: We write $L^{X}$ for the set of all $\ell-$valued subsets of $X$,

1289: i.e., all mappings from $X$ into $L$. For any non-empty set $X,$

1290: if $x\in X$ and $\lambda \in L-\{0\},$ then $x_\lambda $ is

1291: defined to be a mapping from $X$ into $L$ such that

1292: $$x_\lambda (x^{\prime })=\left\{

1293: \begin{array}{c}

1294: \lambda \ {\rm if }\ x^{\prime }=x, \\

1295: 0\ {\rm otherwise,}

1296: \end{array}

1297: \right.$$ and it is often called an $\ell-$valued point in $X.$ We

1298: write $p_\ell(X)$ for the set of all $\ell-$valued points in $X;$

1299: that is, $$p_\ell(X)=\{x_\lambda :x\in X\ {\rm and}\ \lambda \in

1300: L-\{0\}\}.$$ For each $e=x_\lambda \in p_\ell(X),$ $x$ is called

1301: the support of $e$ and denoted $s(e),$ and $\lambda $ is called

1302: the height of $e$ and written $h(e).$ In particular, an

1303: $\ell-$valued point of height $1$ is always identified with its

1304: support. The predicate $\in$ can be extended to a predicate

1305: between $\ell-$valued points and $\ell-$valued sets in a natural

1306: way: $$x_{\lambda}\in A\stackrel{def}{=}x_{\lambda}\subseteq A.$$

1307: Then it is easy to see that $$\lceil x_{\lambda}\in A\rceil =

1308: \lambda\rightarrow A(x)$$ for any $x\in X$, $\lambda\in L$ and

1309: $A\in L^{X}$, where $\rightarrow$ is the implication operator

1310: under consideration. For any $A\subseteq X$, its characteristic

1311: function is a mapping from $X$ into the Boolean algebra

1312: $\mathbf{2}=\{0,1\}$ of two elements, and so it can also be seen

1313: as a mapping from $X$ into $L$, namely, an $\ell-$valued subset of

1314: $X$. We will identify $A$ with its characteristic function. For

1315: any $a\in L$ and $A,B\in L^{X}$, we define all of the scalar

1316: product $aA,$ complement $A^{c}$, intersection $A\cap B$ and union

1317: $A\cup B$ to be $\ell-$valued subsets of $X$ and for all $x\in X$,

1318: 

1319: \smallskip\

1320: 

1321: (i) $x\in aA\stackrel{def}{=}\mathbf{a}\wedge (x\in A);$

1322: 

1323: (ii) $x\in A^{c}\stackrel{def}{=}\lnot (x \in A);$

1324: 

1325: (iii) $x\in A\cap B\stackrel{def}{=}(x\in A)\wedge (x\in B);$

1326: 

1327: (iv) $x\in A\cup B\stackrel{def}{=}(x\in A)\vee (x\in B).$

1328: 

1329: \smallskip\

1330: 

1331: From the truth valuation rules and the definition of derived

1332: formulas in the $\ell-$valued logical and set-theoretical

1333: language, we know that for all $x\in X$,

1334: 

1335: \smallskip\

1336: 

1337: (i') $(aA)(x)=a \wedge A(x);$

1338: 

1339: (ii') $(A^{c})(x)=A(x)^{\bot};$

1340: 

1341: (iii') $(A\cap B)(s)=A(s)\wedge B(s);$ and

1342: 

1343: (iv') $(A\cup B)(s)=A(s)\vee B(s).$

1344: 

1345: \smallskip\

1346: 

1347: It is easy to see that in the domain of $\ell-$valued sets the

1348: intersection and union operations are idempotent, commutative and

1349: associative, and they have $X$ and $\phi$, respectively as their

1350: unit elements. The intersection and union together with the

1351: complement satisfy the De Morgan law, but the distributivity of

1352: intersection over union or union over intersection is no longer

1353: valid. Clearly, the laws for operations of $\ell-$valued sets are

1354: essentially determined by the algebraic properties of the lattice

1355: $\ell$ of truth values.

1356: 

1357: Assume that $X$ and $Y$ are two non-empty sets, and

1358: $h:X\longrightarrow Y$ is a mapping. For any $A\in L^{X}$, its

1359: image $h(A)$ under $h$ is defined by

1360: $$y\in h(A)\stackrel{def}{=}(\exists x\in X)(y=f(x)\wedge x\in

1361: A,$$ and for any $B\in L^{Y}$, its pre-image $h^{-1}(B)$ under $h$

1362: is defined by $$x\in h^{-1}(B)\stackrel{def}{=}h(x)\in B.$$ The

1363: defining equations of $h(A)$ and $h^{-1}(B)$ may be rewritten,

1364: respectively, as follows: $$h(A)(y)=\vee \{A(X):x\in X\ {\rm and}\

1365: f(x)=y\},\ {\rm and}$$ $$h^{-1}(B)(x)=B(h(x)).$$

1366: 

1367: \smallskip\

1368: 

1369: \textbf{Lemma 2.12.} Let $\ell =<L,\leq ,\wedge ,\vee ,\perp

1370: ,0,1>$ be an orthomodular lattice, let $\rightarrow $ enjoy the

1371: Birkhoff-von Neumann requirement, and let $h:X\rightarrow Y$ be a

1372: mapping. Then for any $A,B\in L^{Y},$

1373: $$\stackrel{\ell }{\models} A\equiv B\rightarrow h^{-1}(A)\equiv h^{-1}(B).$$

1374: 

1375: \smallskip\

1376: 

1377: \textbf{Proof.} $$\lceil h^{-1}(A)\equiv h^{-1}(B)\rceil =\wedge

1378: _{x\in X}(h^{-1}(A)(x)\longleftrightarrow h^{-1}(B)(x))$$

1379: $$=\wedge _{x\in X}(A(h(x))\longleftrightarrow B(h(x)))$$

1380: $$\geq \wedge _{y\in Y}(A(y)\longleftrightarrow B(y))$$

1381: $$=\lceil A\equiv B\rceil .\heartsuit$$

1382: 

1383: \smallskip\

1384: 

1385: To conclude this section, we introduce the notion of $\ell-$valued

1386: language as well as some operations of $\ell-$valued languages.

1387: Suppose that $\Sigma$ is an alphabet; that is, a finite nonempty

1388: set (of input symbols). We write $\Sigma^{*}$ for the set of

1389: strings over $\Sigma$:

1390: $$\Sigma^{*}=\cup_{n=0}^{\infty} \Sigma^{n}.$$

1391: An $\ell-$valued language over $\Sigma$ is defined to be an

1392: $\ell-$valued subset of $\Sigma^{\ast}$. Thus, the set of

1393: $\ell-$valued languages over $\Sigma$ is exactly

1394: $L^{\Sigma^{\ast}}$. Let $A,B\in L^{\Sigma ^{\ast }}$ be two

1395: $\ell-$valued subsets of $\Sigma^{*}$. Then we define the

1396: concatenation $A\cdot B$ of $A$ and $B$ and the Kleene closure

1397: $A^{\ast }\in L^{\Sigma ^{\ast }}$ of $A$ as follows: for any

1398: $s\in \Sigma ^{\ast },$

1399: 

1400: \smallskip\

1401: 

1402: (v) $s\in A\cdot B\stackrel{def}{=}(\exists u,v\in

1403: \Sigma^{\ast})(s=uv\wedge u\in A\wedge v\in B);$

1404: 

1405: (vi) $s\in A^{\ast }\stackrel{def}{=}(\exists n\geq 0)(\exists

1406: s_{1},...,s_{n}\in \Sigma ^{\ast }(s=s_{1}...s_{n}\wedge \wedge

1407: _{i=1}^{n}(s_{i}\in A)).$

1408: 

1409: \smallskip\

1410: 

1411: The above defining equations can also be translated to the

1412: following two formulas in the lattice of truth values by employing

1413: the truth valuation rules: for every $s\in \Sigma^{*}$,

1414: 

1415: \smallskip\

1416: 

1417: (v') $(A\cdot B)(s)=\vee \{A(u)\wedge B(v):u,v\in \Sigma ^{\ast }\

1418: {\rm and}\ s=uv\};$

1419: 

1420: (vi') $A^{\ast }(s)=\vee \{\wedge _{i=1}^{n}A(s_{i}):n\geq

1421: 0,s_{1},...,s_{n}\in \Sigma ^{\ast }\ {\rm and}\

1422: s=s_{1}...s_{n}\}$.

1423: 

1424: \smallskip\

1425: 

1426: It is easy to demonstrate that if the meet $\wedge$ is

1427: distributive over the join $\vee$ in $\ell$ (in other words,

1428: $\ell$ is a Boolean algebra), then we have

1429: $$A^{*}=\cup_{n=0}^{\infty}A^{n}$$ where

1430: $$\left\{

1431: \begin{array}{c}

1432: A^{0}=\{\varepsilon \}, \\

1433: A^{n+1}=A^{n}\cdot A\ {\rm for\ all }\ n\geq 0.

1434: \end{array}

1435: \right. $$

1436: 

1437: \smallskip\

1438: 

1439: \textbf{3. Orthomodular Lattice-Valued Automata}

1440: 

1441: \smallskip\

1442: 

1443: For convenience we first recall some basic notions in classical

1444: automata theory. Let $\Sigma $ be a finite input alphabet whose

1445: elements are called input symbols or labels. Then a

1446: nondeterministic finite automaton (NFA for short) over $\Sigma $

1447: is a quadruple

1448: $$\Re =<Q,I,T,E>$$

1449: in which:

1450: 

1451: (i) $Q$ is a finite set whose elements are called states;

1452: 

1453: (ii) $I\subseteq Q$ and states in $I$ are said to be initial;

1454: 

1455: (iii) $T\subseteq Q$ and states in $T$ are said to be terminal;

1456: and

1457: 

1458: (iv) $E\subseteq Q\times \Sigma \times E,$ and each $(p,\sigma

1459: ,q)\in E$ is called a transition in (or an edge of) $\Re $ and it

1460: means that input $\sigma $ makes state $p$ evolves to $q.$

1461: 

1462: An NFA is said to be deterministic if $I$ is a singleton, and for

1463: any $p$ in $Q$ and $\sigma$ in $\Sigma$, there is exactly one $q$

1464: in  $Q$ such that $(p,\sigma,q)\in E$. Thus, the transition

1465: relation $E$ in a deterministic finite automaton (DFA, for short)

1466: may be seen as a mapping from $Q\times \Sigma $ into $Q,$ and it

1467: is called the transition function.

1468: 

1469: A path in $\Re $ is a finite sequence of the form

1470: $$c=q_0\sigma_1q_1...q_{k-1}\sigma _kq_k$$

1471: such that $(q_i,\sigma _{i+1},q_{i+1})\in E$ for each $i<k.$ In

1472: this case, the sequence $\sigma _1...\sigma _k$ is called the

1473: label of $c.$ A path $c=q_0\sigma _1q_1...q_{k-1}\sigma _kq_k$ is

1474: said to be successful if $q_0\in I$ and $q_k\in T.$ The language

1475: accepted by an automaton $\Re $ is the set of labels of all

1476: successful paths in $\Re .$ Let

1477: $$A\subseteq \Sigma ^{*}=\cup _{n=0}^\infty \Sigma ^n.$$

1478: Then $A$ is said to be regular if there is an automaton $\Re $

1479: over $\Sigma $ such that $A$ is the language accepted by $\Re .$

1480: 

1481: The notion of orthomodular lattice-valued automata is a natural

1482: generalization of NFAs. Let $\ell =<L,\leq ,\wedge ,\vee ,\bot

1483: ,0,1>$ be an orthomodular lattice, and let $\Sigma $ be a finite

1484: alphabet. Then an $\ell -$valued (quantum) automaton over $\Sigma

1485: $ is a quadruple $$\Re =<Q,I,T,\delta >$$ where:

1486: 

1487: (i) $Q$ is the same as in an NFA;

1488: 

1489: (ii) $I$ is an $\ell-$valued subset of $Q$; that is, a mapping

1490: from $Q$ into $L$. For each $q\in Q$, $I(q)$ indicates the truth

1491: value (in the underlying quantum logic) of the proposition that

1492: $q$ is an initial state;

1493: 

1494: (iii) $T$ is also an $\ell-$valued subset of $Q$, and for every

1495: $q\in Q$, $T(q)$ expresses the truth value (in our quantum logic)

1496: of the proposition that $q$ is terminal; and

1497: 

1498: (iv) $\delta $ is an $\ell -$valued subset of $Q\times \Sigma

1499: \times Q$; that is, a mapping from $Q\times \Sigma \times Q$ into

1500: $L,$ and it is called the $\ell -$valued (quantum) transition

1501: relation of $\Re .$ Intuitively, $\delta$ is an $\ell -$valued

1502: (ternary) predicate over $ Q,\Sigma $ and $Q$, and for any $p,q\in

1503: Q$ and $\sigma\in \Sigma$, $\delta (p,\sigma ,q)$ stands for the

1504: truth value (in quantum logic) of the proposition that input

1505: $\sigma $ causes state $p$ to become $q.$

1506: 

1507: The propositions of the form

1508: $$"q\ {\rm is\ an\ initial\ state}",\ {\rm written}\ "q\in I",$$

1509: $$"q\ {\rm is\ a\ terminal\ state}",\ {\rm written}\ "q\in T",$$

1510: and

1511: $$"{\rm input}\ \sigma\ {\rm causes\ state}\ p\ {\rm to\ become}\ q,\

1512: {\rm according\ to\ the\ specification}$$ $${\rm given\ by}\

1513: \delta,"\ {\rm written}\ "p\stackrel{\delta,\sigma

1514: }{\longrightarrow }q"$$ are assumed to be atomic propositions in

1515: our logical language designated for describing $\ell-$valued

1516: automata $\Re$. The truth values of the above three propositions

1517: are respectively $I(q)$, $T(q)$ and $\delta(p,\sigma,q)$. The set

1518: of these atomic propositions is denoted $atom(\Re)$. Formally, we

1519: have

1520: $$atom(\Re)=\{"q\in I":q\in Q\}\cup \{"q\in T":q\in Q\}\cup \{"p\stackrel{\delta,\sigma }

1521: {\longrightarrow }q":p,q\in Q\ {\rm and}\ \sigma\in \Sigma\}.$$

1522: 

1523: We write $\mathbf{A}(\Sigma ,\ell )$ for the (proper) class of all

1524: $\ell -$valued automata over $\Sigma.$

1525: 

1526: Before defining the concept of recognizability for $\ell -$valued

1527: automata, we need to introduce some auxiliary notions and

1528: notations. We set

1529: $$T(Q,\Sigma )=(Q\Sigma )^{*}Q=\cup _{n=0}^\infty [(Q\Sigma )^n\ Q];$$

1530: that is, the set of all alternative sequences of states and labels

1531: beginning at a state and also ending at a state. For any

1532: $c=q_0\sigma _1q_1...q_{k-1}\sigma _kq_k\in T(Q,\Sigma ),$ the

1533: length of $c$ is defined to be $k$ and denoted by $|c|,$ $q_0$ is

1534: the beginning of $c$ and denoted by $b(c),$ $q_k$ is the end of

1535: $c$ and denoted by $e(c),$ and sequence $s=\sigma _1...\sigma _k$

1536: is called the label of $c$ and denoted by $lb(c).$

1537: 

1538: Let $\Re \in \mathbf{A}(\Sigma ,\ell )$ be an $\ell-$valued

1539: automaton over $\Sigma$. Then the $\ell -$valued (unary) predicate

1540: $path_\Re $ on $T(Q,\Sigma )$ is defined as $path_\Re \in

1541: L^{T(Q,\Sigma )}$ (the set of all mappings from $ T(Q,\Sigma )$

1542: into $L$):

1543: $$path_\Re (c)\stackrel{def}{=}\wedge _{i=0}^{k-1}[(q_i,\sigma

1544: _{i+1},q_{i+1})\in \delta ]$$ for every $c=q_0\sigma

1545: _1q_1...q_{k-1}\sigma _kq_k\in T(Q,\Sigma ).$

1546: 

1547: In intuition, the truth value of the proposition that $c=q_0\sigma

1548: _1q_1...q_{k-1}\sigma _kq_k$ is a path in $\Re $ is

1549: $$\lceil path_\Re (c)\rceil =\wedge _{i=0}^{k-1}\delta (q_i,\sigma _{i+1},q_{i+1}).$$

1550: Note the difference between the symbols $\wedge$ in the above two

1551: equations: the former is a logical connective, whereas the latter

1552: is an operation on the lattice of truth values.

1553: 

1554: Now, we are ready to define one of the key notions in this paper,

1555: namely, recognizability for $\ell -$valued automata. It will be

1556: seen that the defining equation of $\ell-$valued recognizability

1557: is the same as that in the classical theory of automata. The

1558: essential difference between the quantum recognizability and the

1559: corresponding classical notion implicitly resides in their truth

1560: values.

1561: 

1562: \smallskip\

1563: 

1564: \textbf{Definition 3.1}. Let $\Re \in \mathbf{A}(\Sigma ,\ell )$.

1565: Then the $\ell -$valued (unary) recognizability predicate $rec_\Re

1566: $ on $\Sigma ^{*}$ is defined as $rec_\Re \in L^{\Sigma ^{*}}:$

1567: for every $s\in \Sigma ^{*},$

1568: $$rec_\Re (s)\stackrel{def}{=}(\exists c\in

1569: T(Q,\Sigma ))(b(c)\in I\wedge e(c)\in T\wedge lb(c)=s\wedge

1570: path_\Re (c)).$$ In other words, the truth value of the

1571: proposition that $s$ is recognizable by $ \Re $ is given by

1572: $$\lceil rec_\Re (s)\rceil

1573: =\vee \{I(b(c))\wedge T(e(c))\wedge\lceil path_\Re (c)\rceil :c\in

1574: T(Q,\Sigma )\ {\rm and}\ lb(c)=s\}.$$

1575: 

1576: \smallskip\

1577: 

1578: We note that $rec_\Re $ is defined above as an $\ell -$valued

1579: unary predicate on $\Sigma ^{*},$ so it may also be seen as an

1580: $\ell -$valued subset of $\Sigma ^{*};$ that is, a mapping

1581: $rec_\Re :\Sigma ^{*}\rightarrow L$ with $rec_\Re (s)=\lceil

1582: rec_\Re (s)\rceil $ for all $s\in \Sigma ^{*}.$

1583: 

1584: As a straightforward generalization of regular language, we can

1585: also define regularity for $\ell-$valued languages.

1586: 

1587: \smallskip\

1588: 

1589: \textbf{Definition 3.2}. The $\ell -$valued (unary) regularity

1590: predicate $Reg_\Sigma $ on $L^{\Sigma ^{*}}$ (the set of all $\ell

1591: -$valued subsets of $\Sigma ^{*}$ ) is defined as $Reg_\Sigma \in

1592: L^{(L^{\Sigma ^{*}})}:$ for each $A\in L^{\Sigma ^{*}},$

1593: $$Reg_\Sigma (A)\stackrel{def}{=}(\exists \Re \in \mathbf{A}(\Sigma

1594: ,\ell ))(A\equiv rec_\Re ).$$ Thus, the truth value of the

1595: proposition that $A$ is regular is

1596: $$\lceil Reg_\Sigma (A)\rceil =\vee \{\lceil A\equiv rec_\Re \rceil

1597: :\Re \in \mathbf{A}(\Sigma ,\ell )\}.$$

1598: 

1599: It should be noted that the (automaton) variable $\Re $ bounded by

1600: the existential quantifier in the right-hand side of the defining

1601: formula of $ Reg_\Sigma $ ranges over the proper class

1602: $\mathbf{A}(\Sigma ,\ell ).$ Some readers who are familiar with

1603: axiomatic set theory may worry about that this definition will

1604: cause a certain set-theoretical difficulty, but we stay well away

1605: from anything genuinely problematic. Indeed, for any $\ell

1606: -$valued automaton $\Re =<Q,I,T,\delta >,$ there is a bijection

1607: $\varsigma :Q\rightarrow |Q|$ (the cardinality of $Q$)

1608: $=\{0,1,...,|Q|-1\}$ and we can construct a new $\ell -$valued

1609: automaton $$\varsigma (\Re )=<|Q|,\varsigma (I),\varsigma

1610: (T),\varsigma (\delta )>$$ where $$\varsigma (\delta )(m,\sigma

1611: ,n)=\delta (\varsigma ^{-1}(m),\sigma ,\varsigma ^{-1}(n))$$ for

1612: any $m,n\in |Q|$ and $\sigma \in \Sigma .$ It is easy to see that

1613: $rec_\Re =rec_{\varsigma (\Re )}.$ Then in Definition 3.2 we may

1614: only require that the variable $\Re $ bounded by the existential

1615: quantifier ranges over all $ \ell -$valued automata whose state

1616: sets are subsets of $\omega $ (the set of all non-negative

1617: integers) and the class of all $\ell -$valued automata with

1618: subsets of $\omega $ as state sets is really a set, and in fact it

1619: is a subset of $(2^\omega )^3\times \cup _{Q\subseteq \omega

1620: }L^{Q\times \Sigma \times Q}.$ In most situations, however, the

1621: original version of Definition 3.2 is much more convenient and

1622: compatible with the corresponding definition in classical automata

1623: theory.

1624: 

1625: Before investigating carefully various properties of regular

1626: $\ell-$valued languages, we present some interesting examples. The

1627: first one indicates that every $\ell-$valued language is regular.

1628: It is well-known that a similar conclusion holds in classical

1629: automata theory.

1630: 

1631: \smallskip\

1632: 

1633: \textbf{Example 3.1.} For any $A\in L^{\Sigma ^{*}},$ if $A$ is

1634: finite, i..e., $suppA=\{s\in \Sigma^{\ast}:A(s)>0\}$ is finite,

1635: then

1636: $$\stackrel{\ell }{\models }Reg_\Sigma (A).$$

1637: Indeed, suppose that $suppA=\{\sigma _{i1}...\sigma

1638: _{im_i}:i=1,...,k\}.$ Then we construct an $\ell -$valued

1639: automaton $\Re _A=(Q_A,I_A,T_A,\delta _A)$ in the following way:

1640: 

1641: (i) $Q_A=\cup _{i=1}^k\{q_{i0},q_{i1},...,q_{im_i}\};$

1642: 

1643: (ii) $I_A=\{q_{10},q_{20},...,q_{k0}\};$

1644: 

1645: (iii) $T_A=\{q_{1m_1},q_{2m_2},...,q_{km_k}\};$ and

1646: 

1647: (iv) We define $$\delta _A(q_{ij},\sigma

1648: _{i(j+1)},q_{i(j+1)})=A(\sigma _{i1}...\sigma _{im_i})$$ for any

1649: $1\leq i\leq k$ and $0\leq j<m_i,$ and we define $\delta

1650: _A(p,\sigma ,q)=0$ for other $(p,\sigma ,q)\in Q_A\times \Sigma

1651: \times Q_A.$ Then it is easy to see that $rec_{\Re _A}=A$ and

1652: $$\lceil Reg_\Sigma (A)\rceil \geq \lceil A\equiv rec_{\Re

1653: _A}\rceil =1.\heartsuit $$

1654: 

1655: \smallskip\

1656: 

1657: The following example may be seen as an extension of Example 3.1,

1658: and it shows that the recognizability of a quantum language is not

1659: less than the volume of its finite part.

1660: 

1661: \smallskip\

1662: 

1663: \textbf{Example 3.2.} For any $A\in L^{\Sigma ^{*}},$ we define

1664: $$A\downarrow \lambda =\{s\in \Sigma ^{*}:A(s)\not\leq \lambda

1665: \},$$ and

1666: $$A\uparrow \lambda =\{s\in \Sigma ^{*}:A(s)\not\geq

1667: \lambda \}.$$

1668: 

1669: Let $A\in L^{\Sigma ^{*}}.$ Then

1670: 

1671: (1) $\stackrel{\ell }{\models }\mathbf{\mu }\rightarrow Reg_\Sigma

1672: (A),$ where $\mu =\vee \{\lambda ^{\bot }:A\downarrow \lambda $ is

1673: finite$\};$ and

1674: 

1675: (2) $\stackrel{\ell }{\models }\mathbf{\theta }\rightarrow

1676: Reg_\Sigma (A),$ where $\theta =\vee \{\lambda :A\uparrow \lambda

1677: $ is finite$\}.$

1678: 

1679: Here, $\rightarrow$ may be interpreted as any implication operator

1680: satisfying the Birkhoff-von Neumann requirement. We only prove (1)

1681: and (2) may be proven likewise. For any $\lambda \in L,$ if

1682: $A\downarrow \lambda $ is finite, then we define $A\Downarrow

1683: \lambda \in L^{\Sigma ^{*}}$ as follows: for any $s\in \Sigma

1684: ^{*},$

1685: $$(A\Downarrow \lambda )(s)=\left\{

1686: \begin{array}{c}

1687: A(s)\ {\rm if}\ A(s)\not\leq \lambda , \\

1688: 0\ {\rm if}\ A(s)\leq \lambda .

1689: \end{array}

1690: \right. $$ Clearly, $A\Downarrow \lambda $ is finite. Then from

1691: Example 3.1 we know that there is an $\ell -$valued automata $\Re

1692: [\lambda ]$ such that $rec_{\Re [\lambda ]}=A\Downarrow \lambda ,$

1693: i.e., $ rec_{\Re [\lambda ]}=A(s)$ if $A(s)\not\leq \lambda $ and

1694: $rec_{\Re [\lambda ]}=0$ if $A(s)\leq \lambda ,$ and

1695: $$\lceil Rec_\Sigma (A)\rceil \geq \lceil A\equiv rec_{\Re [\lambda

1696: ]}\rceil =\wedge \{A(s)\leftrightarrow rec_{\Re [\lambda

1697: ]}:A(s)\not\leq \lambda \}\wedge \wedge \{A(s)\leftrightarrow

1698: 0:A(s)\leq \lambda \}$$

1699: $$=\wedge \{A(s)\leftrightarrow 0:A(s)\leq

1700: \lambda \}\geq \lambda ^{\bot }.\heartsuit $$

1701: 

1702: \smallskip\

1703: 

1704: The third example gives a simple connection between

1705: recognizability in classical automata theory and the $\ell

1706: -$valued predicate $Reg_\Sigma $ introduced above.

1707: 

1708: \smallskip\

1709: 

1710: \textbf{Example 3.3.} Let $A\subseteq \Sigma ^{*}$ be a regular

1711: language (in classical automata theory), $B\in L^{\Sigma ^{*}}$

1712: and

1713: $$suppB=\{s\in \Sigma ^{*}:B(s)>0\}\subseteq A,$$ and let

1714: $$\lambda =\vee \{\wedge _{s\in A}(a\leftrightarrow B(s)):a\in

1715: L\}.$$ Then $$\stackrel{\ell }{\models }\mathbf{\lambda

1716: }\rightarrow Reg_\Sigma (B).$$ In particular, if $A\subseteq

1717: \Sigma ^{*}$ is regular then for every $a \in L,$

1718: $$\stackrel{\ell }{\models }Reg_\Sigma (A[a]),$$ where $

1719: A[a]\in L^{\Sigma ^{*}}$ is given as

1720: $$A[a](s)=\left\{

1721: \begin{array}{c}

1722: a \ {\rm if}\ s\in A, \\

1723: 0\ {\rm otherwise.}

1724: \end{array}

1725: \right. $$

1726: 

1727: This conclusion is not difficult to prove. In fact, since $A$ is

1728: regular, there must be an automaton $\Re =<Q,I,T,E>$ that accepts

1729: the language $A.$ Now, for each $a\in L,$ we construct an $ \ell

1730: -$valued automaton $\Re _a=<Q,I,T,\delta _a)$ such that

1731: $$\delta _a(p,\sigma ,q)=\left\{

1732: \begin{array}{c}

1733: a\ {\rm if}\ (p,\sigma ,q)\in E, \\

1734: 0\ {\rm otherwise.}

1735: \end{array}

1736: \right.$$ Then it is easy to know that for all $s\in \Sigma ^{*},$

1737: $$\lceil rec_{\Re _a}(s)\rceil =\left\{

1738: \begin{array}{c}

1739: a\ {\rm if}\ s\in A, \\

1740: 0\ {\rm otherwise,}

1741: \end{array}

1742: \right.$$ and

1743: $$\lceil B\equiv rec_{\Re _a}\rceil =\wedge _{s\in

1744: A}(a\leftrightarrow B(s)]).$$ Therefore, we have

1745: $$\lceil Reg_\Sigma

1746: (B)\rceil \geq \vee \{\lceil B\equiv rec_{\Re _a}\rceil :a\in

1747: L\}=\lambda .\heartsuit $$

1748: 

1749: \smallskip\

1750: 

1751: The fourth example demonstrates that the $\ell -$valued predicate

1752: $ Reg_\Sigma $ defined above is not trivial; that is, it does not

1753: in general degenerate into a two-valued (Boolean) predicate.

1754: 

1755: \smallskip\

1756: 

1757: \textbf{Example 3.4}. We consider a canonical orthomodular

1758: lattice. This lattice has a clear interpretation in quantum

1759: physics. One pasts together observables of the spin one-half

1760: system. Then he will obtain an orthomodular lattice $L(x)\oplus

1761: L(\overline{x}),$ where

1762: $$L(x)=\{0,p_{-},p_{+},1\}$$ corresponds to the outcomes of a

1763: measurement of the spin states along the $x-$axis and

1764: $$L(\overline{x})=\{

1765: \overline{0}=1,\overline{p_{-}},\overline{p_{+}},\overline{1}=0\}$$

1766: is obtained by measuring the spin states along a different spatial

1767: direction; and $L(x)\oplus L(\overline{x})$ may be visualized as

1768: the following ''Chinese lantern'' (see [Sv98] for a more detailed

1769: description of $ L(x)\oplus L(\overline{x})$) (see Figure 2).

1770: 

1771: \begin{figure}\centering

1772: \includegraphics{fig_2.eps}\caption{"Chinese lantern"} \label{fig 2}

1773: \end{figure}

1774: 

1775: In this example, we set $\rightarrow =\rightarrow_3$ (the

1776: Sasaki-hook). By a routine calculation we have

1777: $$p_{-}\leftrightarrow p_{+}=p_{-}\leftrightarrow

1778: \overline{p_{-}}=p_{-}\leftrightarrow \overline{ p_{+}}=0$$ and

1779: $p_{-}\leftrightarrow 1=p_{-}.$ Thus, for each $\lambda \in

1780: L(x)\oplus L(\overline{x}),$ $\lambda \not\leq p_{-}$ implies $

1781: p_{-}\leftrightarrow \lambda \leq p_{-}.$

1782: 

1783: Furthermore, let $\Sigma =\{\sigma ,\tau \}$ and $A=\{\sigma

1784: ^n\tau ^n:n\in \omega \},$ and for any $t\in L(x)\oplus

1785: L(\overline{x}),$ let $A_t\in L^{\Sigma ^{*}}$ be given as

1786: follows:

1787: $$A_t(s)=\left\{

1788: \begin{array}{c}

1789: 1\ {\rm if}\ s\in A, \\

1790: t\ {\rm otherwise.}

1791: \end{array}

1792: \right. $$ Then it holds that $$\stackrel{\ell }{\models

1793: }\mathbf{p}_{-}\leftrightarrow Reg_\Sigma (A_{p_{-}});$$ that is,

1794: $\lceil Reg_\Sigma (A_{p_{-}})\rceil =p_{-}.$ In fact, we know

1795: that $\Sigma ^{*}$ is regular (see [E74], Example II.2.3), and

1796: with Example 3.3 it is easy to see that $\lceil Reg_\Sigma

1797: (A_{p_{-}})\rceil \geq p_{-}.$ Conversely, for any $\ell -$valued

1798: automaton $ \Re =<Q,I,T,\delta >,$ if $|Q|=n$ then

1799: $$\lceil A_{p_{-}}\equiv rec_\Re \rceil \leq [A_{p_{-}}(\sigma

1800: ^n\tau ^n)\leftrightarrow rec_\Re (\sigma ^n\tau ^n)]\wedge \wedge

1801: _{k,l\in \omega \ {\rm s.t. }\ k\neq l}[A_{p_{-}}(\sigma ^k\tau

1802: ^l)\leftrightarrow rec_\Re (\sigma ^k\tau ^l)]$$

1803: $$=rec_\Re (\sigma

1804: ^n\tau ^n)\wedge \wedge _{k,l\in \omega \ {\rm s.t. }\ k\neq

1805: l}[p_{-}\leftrightarrow rec_\Re (\sigma ^k\tau ^l)].$$ If $rec_\Re

1806: (\sigma ^n\tau ^n)\leq p_{-},$ then $\lceil A_{p_{-}}\equiv

1807: rec_\Re \rceil \leq p_{-}.$ Now, we consider the case of $rec_\Re

1808: (\sigma ^n\tau ^n)\not\leq p_{-}.$ For any $c\in T(Q,\Sigma ),$ if

1809: $b(c)\in I,$ $ e(c)\in T$ and $lb(c)=\sigma ^n\tau ^n,$ then $c$

1810: must be of the form $$ c=p_0\sigma p_1...p_{n-1}\sigma p_n\tau

1811: q_1...q_{n-1}\tau q_n.$$ Since $|Q|=n, $ there are $i,j$ such that

1812: $i<j\leq n$ and $p_i=p_j.$ We put

1813: $$c^{+}=p_0\sigma p_1...p_{j-1}\sigma p_j(=p_i)\sigma

1814: p_{i+1}...p_{j-1}\sigma p_j\sigma p_{j+1}...p_{n-1}\sigma p_n\tau

1815: q_1...q_{n-1}\tau q_n.$$ Then $b(c^{+})\in I,$ $e(c^{+})\in T,$

1816: $lb(c^{+})=\sigma ^{n+(j-i)}\tau ^n$ and $\lceil path_\Re

1817: (c^{+})\rceil =\lceil path_\Re (c)\rceil .$ Therefore, it holds

1818: that

1819: $$rec_\Re (\sigma ^{n+(j-i)}\tau ^n)\geq \vee \{\lceil

1820: path_\Re (c^{+})\rceil :b(c)\in I, e(c)\in T\ {\rm and}\

1821:  lb(c)=\sigma ^n\tau ^n\}$$

1822: $$=\vee \{\lceil path_\Re (c)\rceil :b(c)\in I, e(c)\in T\ {\rm

1823: and}\ lb(c)=\sigma ^n\tau ^n\}$$

1824: $$=rec_\Re (\sigma ^n\tau ^n),$$

1825: and $$rec_\Re (\sigma ^{n+(j-i)}\tau ^n)\not\leq p_{-}.$$

1826: Furthermore, we have $$\lceil A_{p_{-}}\equiv rec_\Re \rceil \leq

1827: p_{-}\leftrightarrow rec_\Re (\sigma ^{n+(j-i)}\tau ^n)\leq

1828: p_{-}.$$

1829: 

1830: So, for all $\ell -$valued automata $\Re $ we have $\lceil

1831: A_{p_{-}}\equiv rec_\Re \rceil \leq p_{-},$ and it follows that

1832: $$\lceil Rec_\Sigma (A_{p_{-}})\rceil =\vee \{\lceil A\equiv

1833: rec_\Re \rceil :\Re \in \mathbf{A} (\Sigma ,\ell )\}\leq p_{-}.$$

1834: This together with $\lceil Reg_\Sigma (A_{p_{-}})\rceil \geq

1835: p_{-}$ obtained before leads to $\lceil Reg_\Sigma

1836: (A_{p_{-}})\rceil =p_{-}.$

1837: 

1838: Similarly, we have $\lceil Reg_\Sigma (A_t)\rceil =t$ for

1839: $t=p_{+},\overline{ p_{-}}$ and $\overline{p_{+}}.\heartsuit$

1840: 

1841: \smallskip\

1842: 

1843: Motivated by the above example, we propose the open problem: how

1844: to describe orthomodular lattices $\ell =<L,\leq ,\wedge ,\vee

1845: ,\bot ,0,1>$ which satisfy that

1846: $$\{\lceil Reg_\Sigma (A)\rceil :A\in L^{\Sigma ^{*}}\}=L,$$ i.e., the truth

1847: values of recognizability traverse all over $L,$ or more

1848: explicitly, for every $\lambda \in L,$ there is $A\in L^{\Sigma

1849: ^{*}}$ such that $\lceil Reg_\Sigma (A)\rceil =\lambda .\ $ It

1850: seems that this is a difficult problem.

1851: 

1852: The $\ell-$valued regularity predicate $Reg_\Sigma$ in Definition

1853: 3.2 is a direct generalization of the notion of regular language

1854: in classical automata theory. In what follows, we will see that

1855: the predicate $Reg_\Sigma$ does not work well in many cases. Why

1856: this happens? Note that $Reg_\Sigma$ is merely a simple mimic of

1857: the classical concept of regular language, and an essential

1858: feature of quantum logic is missing here. In the defining equation

1859: of $Reg_\Sigma$, the language $A$ to be recognized and the

1860: automaton $\Re$ for recognizing $A$ are left completely

1861: irrelevant. In the case of classical logic, this does not causes

1862: any difficulty in manipulating regular languages. Nevertheless,

1863: the thing changes when we work in quantum logic. After an analysis

1864: it was found that a suitable link between $A$ and $\Re$ is a

1865: commutativity of them. This motivates the following:

1866: 

1867: \smallskip\

1868: 

1869: \textbf{Definition 3.3.} The $\ell -$valued (unary and partial)

1870: predicate $CReg_{\Sigma }$ on $L^{\Sigma ^{\ast }}$ is called

1871: commutative regularity and it is defined as $CReg_{\Sigma }\in

1872: L^{(L^{\Sigma ^{\ast }})}:$ for any $A\in L^{\Sigma ^{\ast }}$

1873: with finite $ Range(A)=\{A(s):s\in \Sigma ^{\ast }\},$

1874: $$CReg_{\Sigma }(A)\stackrel{def}{=}(\exists \Re

1875: \in \mathbf{A}(\Sigma ,\ell ))(\gamma (atom(\Re )\cup r(A))\wedge

1876: (A\equiv rec_{\Re })),$$ where $r(A)=\{\mathbf{a}:a\in

1877: Range(A)\}.$

1878: 

1879: \smallskip\

1880: 

1881: The exposition concerning the automata variable $\Re$ in the

1882: defining equation of $Reg_{\Sigma}$ in Definition 3.2 also applies

1883: to $CReg_{\Sigma}$ in the above definition.

1884: 

1885: It is obvious that the notion of commutative regularity is

1886: stronger than regularity. In other words, we have for any $A\in

1887: L^{\Sigma^{\ast}}$,

1888: $$\stackrel{\ell }{\models } CReg_{\Sigma}(A)\rightarrow

1889: Reg_{\Sigma}(A).$$ On the other hand, if $\ell$ is a Boolean

1890: algebra; that is, the underlying logic is the classical Boolean

1891: logic, then these two notions are equivalent; or formally, for all

1892: $A\in L^{\Sigma^{\ast}}$, it holds that

1893: $$\stackrel{\ell }{\models } CReg_{\Sigma}(A)\leftrightarrow

1894: Reg_{\Sigma}(A).$$ This is just why the predicate $Reg_\Sigma$

1895: works very well in classical automata theory but not in the theory

1896: of automata based on quantum logic.

1897: 

1898: \bigskip\

1899: 

1900: \textbf{4. Orthomodular Lattice-Valued Deterministic Automata}

1901: 

1902: \smallskip\

1903: 

1904: The notion of nondeterminism plays a central role in the theory of

1905: computation. The nondeterministic mechanism enables a device to

1906: change its states in a way that is only partially determined by

1907: the current state and input symbol. Obviously, the concept of

1908: $\ell-$valued automaton introduced in the last section is a

1909: generalization of nondeterministic finite automaton. In classical

1910: theory of automata, each nondeterministic finite automaton is

1911: equivalent to a deterministic one; more exactly, there exists a

1912: deterministic finite automaton which accepts the same language as

1913: the originally given nondeterministic one does. The aim of this

1914: section is just to see whether this result is still valid in the

1915: framework of quantum logic. To this end, we first introduce the

1916: concept of deterministic $\ell-$valued automaton.

1917: 

1918: Let $\Re=<Q,I,T,\delta>\in \mathbf{A}(\Sigma,\ell)$ be an

1919: $\ell-$valued automata over $\Sigma$. If

1920: 

1921: (i) there is a unique $q_0$ in $Q$ with $I(q_0)>0$; and

1922: 

1923: (ii) for all $q$ in $Q$ and $\sigma$ in $\Sigma ,$ there is a

1924: unique state $p$ in $Q$ such that $$ \delta (q,\sigma,p)>0,$$ then

1925: $M$ is called an $\ell-$valued (quantum) deterministic finite

1926: automaton ($\ell-$valued DFA for short). The $\ell-$valued

1927: transition relation $\delta $ in an $\ell-$valued DFA may be

1928: equivalently represented by a mapping from $Q\times \Sigma $ into

1929: $Q\times(L-\{0\}).$ For any $q$ in $Q$ and $\sigma$ in $\Sigma,$

1930: if $p$ is the unique element in $Q$ with $\delta (q,\sigma,p)>0,$

1931: then $\delta (q,\sigma)=(p,\delta (q,\sigma,p))\in

1932: Q\times(L-\{0\}).$

1933: 

1934: The class of $\ell-$valued DFAs over $\Sigma$ is denoted

1935: $\mathbf{DA}(\Sigma,\ell)$.

1936: 

1937: Suppose that $\Re$ is an $\ell-$valued DFA, $\delta

1938: (q_0,\sigma_1)=(q_1,\lambda _1)$ and $\delta

1939: (q_i,\sigma_{i+1})=(q_{i+1},\lambda _{i+1})$ for all

1940: $i=1,2,...,n-1.$ Then it is easy to see that $$\lceil rec_\Re

1941: (\sigma_1 ...\sigma_n)\rceil =I(q_0)\wedge T(q_n)\wedge \wedge

1942: _{i=1}^n\lambda _i.$$

1943: 

1944: Throughout this section, we always suppose that the lattice $\ell$

1945: of truth values is finite.

1946: 

1947: The proof of the equivalence between classical deterministic

1948: finite and nondeterministic finite automata is carried out by

1949: building the power set construction of a nondeterministic finite

1950: automaton that is deterministic and can simulate the given

1951: nondeterministic one. The power set construction can be naturally

1952: extended into the case of $\ell-$valued automata.

1953: 

1954: Let $\Re =<Q,I,T,\delta

1955: >\in \mathbf{A}(\Sigma ,\ell )$ be an $\ell -$valued automaton

1956: over $\Sigma .$ We define the $\ell -$valued power set

1957: construction of $\Re $ to be $\ell -$valued automaton

1958: $$\ell ^{\Re }=<L^{Q},I_{1},\overline{T},\overline{

1959: \delta }>$$ over $\Sigma ,$ where:

1960: 

1961: (i) $L^{Q}$ is the set of all $\ell -$valued subsets of $Q;$ that

1962: is, mappings from $Q$ into $L;$

1963: 

1964: (ii) $I_{1}$ is an $\ell -$valued point with height $1;$ that is,

1965: $I_{1}\in L^{(L^{Q})}$ and

1966: $$I_{1}(X)=\left\{

1967: \begin{array}{c}

1968: 1\ {\rm if }X=I, \\

1969: 0\ {\rm otherwise}

1970: \end{array}

1971: \right.$$ for all $X\in L^{Q};$

1972: 

1973: (iii) $\overline{T}\in L^{(L^{Q})};$ that is, $\overline{T}$ is an

1974: $\ell -$valued subset of $L^{Q},$ and

1975: $$\overline{T}(X)=\vee _{q\in Q}[X(q)\wedge T(q)]$$

1976: for any $X\in L^{Q};$ and

1977: 

1978: (iv) $\overline{\delta }$ is a mapping from $L^{Q}\times \Sigma $

1979: into $ L^{Q},$ and for each $X\in L^{Q},$ $\overline{\delta

1980: }(X,\sigma )\in L^{Q}$ and

1981: $$\overline{\delta }(X,\sigma )(q)=\vee _{p\in Q}[X(p)\wedge \delta (p,\sigma

1982: ,q)]$$ for every $q\in Q.$

1983: 

1984: Since $L$ is assumed to be finite, $L^{Q}$ is finite too. Thus, it

1985: is easy to see that $\ell ^{\Re }$ is an $\ell -$valued DFA.

1986: Moreover, both the set of the initial states and the transition

1987: relation are two-valued, namely, their truth values are either $0$

1988: or $1,$ and only the set of terminal states carries $\ell -$valued

1989: information.

1990: 

1991: The following theorem compares the abilities of an $\ell-$valued

1992: automaton and its power set construction according to the

1993: $\ell-$valued languages recognized by them.

1994: 

1995: \smallskip\

1996: 

1997: \textbf{Theorem 4.1.} Let $\ell =<L,\leq ,\wedge ,\vee ,\bot

1998: ,0,1>$ be a finite orthomodular lattice, and let $\longrightarrow$

1999: be an implication operator satisfying the Birkhoff-von Neumann

2000: requirement.

2001: 

2002: (1) For any $\Re \in \mathbf{A}(\Sigma ,\ell )$ and $s\in \Sigma

2003: ^{\ast },$

2004: $$\stackrel{\ell }{ \models } rec_{\Re }(s)\longrightarrow rec_{(\ell

2005: ^{\Re })}(s).$$

2006: 

2007: (2) For any $\Re \in \mathbf{A}(\Sigma ,\ell )$ and $s\in \Sigma

2008: ^{\ast },$

2009: $$\stackrel{\ell }{ \models } \gamma(atom(\Re))\wedge rec_{(\ell

2010: ^{\Re })}(s) \longrightarrow rec_{\Re }(s),$$ and in particular if

2011: $\rightarrow =\rightarrow_3$, then

2012: $$\stackrel{\ell }{ \models } \gamma(atom(\Re))\longrightarrow (rec_{(\ell

2013: ^{\Re })}(s) \longleftrightarrow rec_{\Re }(s)).$$

2014: 

2015: (3) The following two statements are equivalent to each other:

2016: 

2017: \ \ \ \ \ \ (i) $\ell$ is a Boolean algebra.

2018: 

2019: \ \ \ \ \ \ (ii) For any $\Re \in \mathbf{A}(\Sigma ,\ell )$ and

2020: $s\in \Sigma ^{\ast },$

2021: $$\stackrel{\ell }{ \models } rec_{\Re }(s)\longleftrightarrow rec_{(\ell

2022: ^{\Re })}(s).$$

2023: 

2024: \smallskip\

2025: 

2026: \textbf{Proof.} The proof of (1) is easy, and we omit it here.

2027: 

2028: (2) Suppose that $\Re =<Q,I,T,\delta

2029: >\in \mathbf{A}(\Sigma ,\ell )$ and $\ell ^{\Re

2030: }=<L^{Q},I_{1},\overline{T}, \overline{\delta }>$ is the $\ell

2031: -$valued power set construction of $\Re .$ Our aim is to

2032: demonstrate that

2033: $$\lceil \gamma(atom(\Re))\rceil \wedge \lceil rec_{(\ell ^{\Re })}(s)\rceil\leq \lceil rec_{\Re }(s)\rceil

2034: $$ for all $s\in \Sigma ^{\ast }.$ To this end, we first prove the

2035: following

2036: $$claim:\ \ \lceil \gamma(atom(\Re))\rceil \wedge \overline{\delta }(I,\sigma _{1}...\sigma

2037: _{n})(q_{n}) \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

2038: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $$

2039: $$\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \leq\vee \{I(q_{0})\wedge \wedge

2040: _{i=0}^{n-1}\delta (q_{i},\sigma

2041: _{i+1},q_{i+1}):q_{0},q_{1},...,q_{n-1}\in Q\}$$ for any $\sigma

2042: _{1},...,\sigma _{n}\in \Sigma $ and $q\in Q.$ We proceed by

2043: induction on $n.$ For $n=0,$ it is clear. The definition of

2044: $\overline{\delta}$ yields

2045: $$\overline{\delta }(I,\sigma _{1}...\sigma

2046: _{n})(q_{n})=\overline{\delta }( \overline{\delta }(I,\sigma

2047: _{1}...\sigma _{n-1}),\sigma _{n})(q_{n})\ \ \ \ \ \ \ \ \ \ \ \ \

2048: \ \ \ \ \ \ \ \ \ $$

2049: $$=\vee _{q_{n-1}\in Q}[\overline{\delta }(I,\sigma _{1}...\sigma

2050: _{n-1})(q_{n-1})\wedge \delta (q_{n-1},\sigma _{n},q_{n})].$$ We

2051: write $$\lceil atom(\Re)\rceil =\{\lceil \varphi\rceil: \varphi\in

2052: atom(\Re)\}.$$ Then it holds that

2053: $$\lceil \gamma(atom(\Re))\rceil=\gamma(\lceil atom(\Re)\rceil).$$ Note

2054: that the symbol $\gamma$ in the left-hand side applies to a set of

2055: logical formulas, whereas the one in the right-hand side applies

2056: to a subset of $L$. Furthermore, it is easy to see that

2057: $\delta(q_{n-1},\sigma_n,q_n),\ \overline{\delta}(I,\sigma_1

2058: ...\sigma_{n-1})(q_{n-1})$ and $\lceil \gamma(atom(\Re))\rceil$

2059: are all in $[\lceil atom(\Re)\rceil]$ (the subalgebra of $\ell$

2060: generated by $\lceil atom(\Re)\rceil$). Thus, with Lemmas 2.5 and

2061: 2.6 and the induction hypothesis we obtain

2062: $$\lceil \gamma(atom(\Re))\rceil\wedge \overline{\delta }(I,\sigma _{1}...\sigma

2063: _{n})(q_{n}) =\lceil \gamma(atom(\Re))\rceil\wedge \lceil

2064: \gamma(atom(\Re))\rceil $$ $$\ \ \ \ \ \ \ \ \ \ \wedge \vee

2065: _{q_{n-1}\in Q}[\overline{\delta }(I,\sigma _{1}...\sigma

2066: _{n-1})(q_{n-1})\wedge \delta (q_{n-1},\sigma _{n},q_{n})]$$

2067: $$\leq \vee _{q_{n-1}\in Q}[\lceil \gamma(atom(\Re))\rceil\wedge

2068: (\vee \{I(q_0)\wedge\wedge_{i=0}^{n-2}\delta(q_i,\sigma

2069: _{i+1},q_{i+1}):$$ $$\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

2070: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

2071: q_0,q_1,...,q_{n-2}\in Q\})\wedge \delta (q_{n-1},\sigma

2072: _{n},q_{n})].$$ Using Lemmas 2.5 and 2.6 again, we complete the

2073: proof of the above claim.

2074: 

2075: Now with this claim, we can use Lemmas 2.5 and 2.6 twice and

2076: derive that

2077: $$\lceil \gamma(atom(\Re))\rceil\wedge \lceil

2078: rec_{(\ell^{Re})}(\sigma_1 ...\sigma_n)\rceil =\lceil

2079: \gamma(atom(\Re))\rceil\wedge \overline{T}( \overline{\delta

2080: }(I,\sigma _{1}...\sigma _{n}))$$

2081: $$=\lceil \gamma(atom(\Re))\rceil\wedge \vee _{q_{n}\in Q}[\overline{\delta }(I,\sigma _{1}...\sigma

2082: _{n})(q_{n})\wedge T(q_{n})]$$

2083: $$\leq \vee _{q_{n}\in Q}[\lceil \gamma(atom(\Re))\rceil\wedge \overline{\delta }(I,\sigma _{1}...\sigma

2084: _{n})(q_{n})\wedge T(q_{n})]$$

2085: $$\leq \vee _{q_{n}\in Q}[\lceil \gamma(atom(\Re))\rceil\wedge (\vee \{I(q_{0})\wedge \wedge

2086: _{i=0}^{n-1}\delta (q_{i},\sigma

2087: _{i+1},q_{i+1}):q_{0},q_{1},...,q_{n-1}\in Q\})\wedge T(q_{n})]$$

2088: $$\leq \vee \{I(q_{0})\wedge \wedge _{i=0}^{n-1}\delta (q_{i},\sigma

2089: _{i+1},q_{i+1})\wedge T(q_{n}):q_{0},q_{1},...,q_{n-1}\in Q\}$$

2090: $$=\lceil rec_{\Re }(\sigma _{1}...\sigma _{n})\rceil .$$

2091: 

2092: For the case of $\rightarrow =\rightarrow_3$, what we want to

2093: prove is

2094: $$\lceil \gamma(atom(\Re))\rceil \leq \lceil rec_{(\ell ^{\Re })}(s)\rceil\longrightarrow_3 \lceil rec_{\Re }(s)\rceil

2095: .$$ With the above conclusion and Lemma 2.10, it suffices to show

2096: that $\lceil \gamma(atom(\Re))\rceil C \lceil rec_{\Re

2097: }(s)\rceil$. We observe that $$\lceil \gamma(atom(\Re))\rceil

2098: =\vee \{\wedge_{\varphi\in \lceil

2099: atom(\Re)\rceil}\varphi^{f(\varphi)}:f\in \{0,1\}^{\lceil

2100: atom(\Re)\rceil}\}.$$ Then Lemma 2.2 tells us that we only need to

2101: prove $\wedge_{\varphi\in \lceil

2102: atom(\Re)\rceil}\varphi^{f(\varphi)}C \lceil rec_{\Re }(s)\rceil$

2103: for all $f\in \{0,1\}^{\lceil atom(\Re)\rceil}$. For every

2104: $\psi\in \lceil atom(\Re)\rceil$, note that

2105: $$\wedge_{\varphi\in \lceil

2106: atom(\Re)\rceil}\varphi^{f(\varphi)}\leq \psi^{f(\psi)}.$$ Then

2107: $\wedge_{\varphi\in \lceil atom(\Re)\rceil}\varphi^{f(\varphi)} C

2108: \psi^{f(\psi)},$ and furthermore it follows that

2109: $\wedge_{\varphi\in \lceil atom(\Re)\rceil}\varphi^{f(\varphi)} C

2110: \psi$ from Lemmas 2.1(3) and (4). Since $\lceil rec_\Re (s)\rceil$

2111: is calculated from some elements in $\lceil atom(\Re)\rceil$ by

2112: applying a finite number of meets or unions, we complete the proof

2113: with Lemma 2.2.

2114: 

2115: (3) Note that $\lceil \gamma(atom(\Re))\rceil=1$ is always valid

2116: when $\ell$ is a Boolean algebra. Thus, it is proved that (i)

2117: implies (ii). We now turn to show that (ii) implies (i). It

2118: suffices to show that the meet $\wedge$ is distributive over the

2119: union $\vee$; that is, $$a\wedge (b\vee c)=(a\wedge b)\vee

2120: (a\wedge c)$$ for all $a,b,c\in L$. Let $a,b,c\in L.$ We construct

2121: an $\ell -$valued automaton

2122: $$\Re =<\{u,v,w\},\{u,v\},\{w\},\delta >$$ over $ \Sigma $ which

2123: has at least one element $\sigma ,$ where $\delta (u,\sigma

2124: ,u)=a,$ $\delta (u,\sigma ,w)=c,$ $\delta (v,\sigma ,u)=b,$ and

2125: $\delta $ takes the value $0$ for other cases. It may be

2126: visualized by Figure 3.

2127: 

2128: \begin{figure}\centering

2129: \includegraphics[width=0.5\textwidth]{fig_3.eps}\caption{Automaton a} \label{fig 3}

2130: \end{figure}

2131: 

2132: In the automaton $\Re $ we have

2133: $$\lceil rec_{\Re }(\sigma \sigma )\rceil =\vee \{I(q_{0})\wedge

2134: T(q_{2})\wedge \delta (q_{0},\sigma ,q_{1})\wedge \delta

2135: (q_{1},\sigma ,q_{2}):q_{0},q_{1},q_{2}\in Q\}$$

2136: $$=\vee \{\delta (u,\sigma ,q_{1})\wedge \delta (q_{1},\sigma

2137: ,w):q_{1}\in Q\}\vee \vee \{\delta (v,\sigma ,q_{1})\wedge \delta

2138: (q_{1},\sigma ,v):q_{1}\in Q\}$$

2139: $$=[\delta (u,\sigma ,u)\wedge \delta (u,\sigma ,w)]\vee \lbrack

2140: \delta (v,\sigma ,u)\wedge \delta (u,\sigma ,w)]$$

2141: $$=(a\wedge c)\vee (b\wedge c).$$

2142: 

2143: Consider the $\ell -$valued power set construction $\ell ^{\Re }$

2144: of $\Re .$ Then

2145: $$\overline{\delta }(I,\sigma )(u)=\vee _{q\in Q}[I(q)\wedge \delta

2146: (q,\sigma ,u)]$$

2147: $$=\delta (u,\sigma ,u)\vee \delta (v,\sigma ,u)]$$

2148: $$=a\vee b.$$

2149: Similarly, we obtain $\overline{\delta }(I,\sigma )(v)=0$ and

2150: $\overline{ \delta }(I,\sigma )(w)=c.$ It follows that for any

2151: $q\in Q,$

2152: $$\overline{\delta }(I,\sigma \sigma )(q)=\overline{\delta

2153: }(\overline{\delta }(I,\sigma ),\sigma )(q)$$

2154: $$=\vee _{q^{\prime }\in Q}[\overline{\delta }(I,\sigma )(q^{\prime

2155: })\wedge \delta (q^{\prime },\sigma ,q)]$$

2156: $$=[\overline{\delta }(I,\sigma )(u)\wedge \delta (u,\sigma

2157: ,q)]\vee \lbrack \overline{\delta }(I,\sigma )(w)\wedge \delta

2158: (w,\sigma ,q)]$$

2159: $$=(a\vee b)\wedge \delta (u,\sigma ,q).$$

2160: Thus, $$\overline{\delta }(I,\sigma \sigma )(u)=(a\vee b)\wedge

2161: a=a,$$ $$ \overline{\delta }(I,\sigma \sigma )(v)=0$$ and

2162: $$\overline{\delta }(I,\sigma \sigma )(w)=(a\vee b)\wedge c.$$

2163: Therefore,

2164: $$\lceil rec_{(\ell ^{\Re })}(\sigma \sigma )\rceil

2165: =\overline{T}(\overline{ \delta }(I,\sigma \sigma ))$$

2166: $$=\vee _{q\in Q}[\overline{\delta }(I,\sigma \sigma )(q)\wedge

2167: T(q)]$$

2168: $$=\overline{\delta }(I,\sigma \sigma )(w)$$

2169: $$=(a\vee b)\wedge c.$$

2170: 

2171: Finally, from the assumption (ii) we assert that

2172: $$(a\wedge c)\vee (b\wedge c)=\lceil rec_{\Re }(\sigma \sigma

2173: )\rceil =\lceil rec_{(\ell ^{\Re })}(\sigma \sigma )\rceil =(a\vee

2174: b)\wedge c.\heartsuit$$

2175: 

2176: \smallskip\

2177: 

2178: Many results in this paper appear in the same scheme as the above

2179: theorem. So, we here give a detailed explanation of this theorem.

2180: The above theorem points out that the ability of an $\ell-$valued

2181: automaton for recognizing language is always weaker than that of

2182: its power set construction. On the other hand, in order to warrant

2183: that an $\ell-$valued automaton $\Re$ and its power set

2184: construction have the same ability of accepting language, the

2185: condition $\gamma(atom(\Re))$ has to be imposed. The intuitive

2186: meaning of this condition is that (the truth values of) any two

2187: atomic propositions describing $\Re$ should commute. (See also the

2188: physical interpretation of commutativity presented in the

2189: introductory section.) The third part of Theorem 4.1 indicates

2190: that the equivalence between a nondeterministic finite automaton

2191: and its power set construction is universally valid if and only if

2192: the underlying logic degenerates to the classical Boolean logic.

2193: In other words, if the meta-logic that we use in our reasoning

2194: does not enjoy distributivity, then such a meta-logic is not

2195: strong enough to guarantee the universal validity of any

2196: nondeterministic finite automaton and its power set construction,

2197: and we can always find a nondeterministic finite automaton such

2198: that the equivalence between it and its power set construction is

2199: not derivable with the mere inference power provided by such a

2200: meta-logic.

2201: 

2202: In Section 3, we introduced the regularity and commutative

2203: regularity predicates $Reg_{\Sigma}$ and $CReg_{\Sigma}$. They are

2204: all given with respect to nondeterministic $\ell-$valued automata.

2205: Now we propose a restricted version of them based on the smaller

2206: class of deterministic $\ell-$valued automata.

2207: 

2208: \smallskip\

2209: 

2210: \textbf{Definition 4.1.} Let $\ell=<L,\leq ,\wedge ,\vee ,\bot

2211: ,0,1>$ be an orthomodular lattice. Then the $\ell -$valued (unary)

2212: predicates $DReg_{\Sigma}$ and (unary and partial) predicate

2213: $CDReg_{\Sigma }$ on $L^{\Sigma ^{\ast }}$ are called

2214: deterministic regularity and commutative deterministic regularity,

2215: respectively, and they are defined as $DReg_{\Sigma}$,

2216: $CDReg_{\Sigma }\in L^{(L^{\Sigma ^{\ast }})}:$ for any $A\in

2217: L^{\Sigma ^{\ast }}$,

2218: $$DReg_{\Sigma }(A)\stackrel{def}{=}(\exists \Re

2219: \in \mathbf{DA}(\Sigma ,\ell ))(A\equiv rec_{\Re }),$$ and for any

2220: $A\in L^{\Sigma ^{\ast }}$ with finite $Range(A)=\{A(s):s\in

2221: \Sigma^{\ast}\},$

2222: $$CDReg_{\Sigma }(A)\stackrel{def}{=}(\exists \Re

2223: \in \mathbf{DA}(\Sigma ,\ell ))(\gamma (atom(\Re )\cup r(A))\wedge

2224: (A\equiv rec_{\Re })),$$ where $r(A)=\{\mathbf{a}:a\in

2225: Range(A)\}.$

2226: 

2227: \smallskip\

2228: 

2229: It is similar to the relation between $Reg_\Sigma$ and

2230: $CReg_\Sigma$ that $CDReg_\Sigma$ is stronger than $DReg_\Sigma$.

2231: In other words, it holds that for any $A\in L^{\Sigma^{\ast}}$,

2232: $$\stackrel{\ell }{\models } CDReg_{\Sigma}(A)\rightarrow

2233: DReg_{\Sigma}(A).$$ The following corollary shows that a certain

2234: commutativity condition guarantees that they are equivalent.

2235: Furthermore, if $\ell$ is a Boolean algebra, then the four notions

2236: $Reg_{\Sigma}$, $CReg_{\Sigma}$, $DReg_{\Sigma}$ and

2237: $CDReg_{\Sigma}$ all coincide.

2238: 

2239: \smallskip\

2240: 

2241: \textbf{Corollary 4.2.} Let $\ell=<L,\leq ,\wedge ,\vee ,\bot

2242: ,0,1>$ be a finite orthomodular lattice, and let $\longrightarrow

2243: = \longrightarrow_3$. Then for any $A\in L^{\Sigma^{\ast}}$,

2244: $$\stackrel{\ell }{ \models }CReg_{\Sigma}(A)\longleftrightarrow CDReg_{\Sigma}(A).$$

2245: In particular, if $\ell$ is a Boolean algebra, then for any $A\in

2246: L^{\Sigma ^{\ast }},$

2247: $$\stackrel{\ell }{ \models } Reg_{\Sigma}(A)\longleftrightarrow DReg_{\Sigma}(A) .$$

2248: 

2249: \smallskip\

2250: 

2251: \textbf{Proof}. It is clear that $$\stackrel{\ell }{ \models

2252: }CDReg_{\Sigma}(A)\rightarrow CDReg_{\Sigma }(A).$$ Then we only

2253: need to prove that $$\stackrel{\ell }{ \models }CReg_{\Sigma

2254: }(A)\rightarrow CDReg_{\Sigma }(A);$$ that is, for any $\Re \in

2255: \mathbf{A}(\Sigma ,\ell ),$

2256: $$\lceil \gamma (atom(\Re )\cup r(A))\rceil \wedge \lceil A\equiv

2257: rec_{\Re }\rceil \leq \vee \{\lceil \gamma (atom(\wp )\cup

2258: r(A))\rceil \wedge \lceil A\equiv rec_{\wp }\rceil :\wp \in

2259: \mathbf{DA}(\Sigma ,\ell )\}.$$

2260: 

2261: First, by using Lemmas 2.5, 2.6 and 2.11(2) we have $$\lceil

2262: \gamma (atom(\Re )\cup r(A))\rceil \wedge \lceil A\equiv rec_{\Re

2263: }\rceil \wedge \lceil rec_{\Re }\equiv rec_{(\ell ^{\Re })}\rceil

2264: =\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

2265: \ \ \ $$

2266: $$\lceil \gamma (atom(\Re )\cup r(A))\rceil \wedge \wedge _{s\in

2267: \Sigma ^{\ast }}(A(s)\leftrightarrow rec_{\Re }(s))\wedge \wedge

2268: _{s\in \Sigma ^{\ast }}(rec_{\Re }(s)\leftrightarrow rec_{(\ell

2269: ^{\Re })}(s))$$

2270: $$=\wedge _{s\in \Sigma ^{\ast }}(\lceil \gamma (atom(\Re )\cup

2271: r(A))\rceil \wedge (A(s)\rightarrow rec_{\Re }(s))\wedge (rec_{\Re

2272: }(s)\rightarrow rec_{(\ell ^{\Re })}(s))\wedge$$

2273: $$\wedge _{s\in \Sigma ^{\ast }}(\lceil \gamma (atom(\Re

2274: )\cup r(A))\rceil \wedge (rec_{(\ell ^{\Re })}(s)\rightarrow

2275: rec_{\Re }(s))\wedge (rec_{\Re }(s)\rightarrow A(s))$$

2276: $$\leq \wedge _{s\in \Sigma ^{\ast }}(A(s)\rightarrow rec_{(\ell

2277: ^{\Re })}(s))\wedge \wedge _{s\in \Sigma ^{\ast }}(rec_{(\ell

2278: ^{\Re })}(s)\rightarrow A(s))$$

2279: $$=\wedge _{s\in \Sigma ^{\ast }}(A(s)\leftrightarrow rec_{(\ell

2280: ^{\Re })}(s)) $$

2281: $$=\lceil A\equiv rec_{(\ell ^{\Re })}\rceil .$$

2282: 

2283: Second, from Theorem 4.1(2) we obtain

2284: $$\lceil \gamma (atom(\Re )\cup r(A))\rceil \leq \lceil \gamma

2285: (atom(\Re ))\rceil \leq \lceil rec_{\Re }\equiv rec_{(\ell ^{\Re

2286: })}\rceil ,$$ and

2287: $$\lceil \gamma (atom(\Re )\cup r(A))\rceil \wedge \lceil A\equiv

2288: rec_{\Re }\rceil \leq \lceil \gamma (atom(\Re )\cup r(A))\rceil

2289: \wedge \lceil A\equiv rec_{\Re }\rceil \wedge \lceil rec_{\Re

2290: }\equiv rec_{(\ell ^{\Re })}\rceil $$

2291: $$\leq \lceil A\equiv rec_{(\ell ^{\Re })}\rceil .$$

2292: 

2293: In addition, it is easy to see that

2294: $$\lceil \gamma (atom(\Re )\cup r(A))\rceil \leq \lceil \gamma

2295: (atom(\ell ^{\Re })\cup r(A))\rceil $$ from Lemma 2.6. Therefore,

2296: it follows that

2297: $$\lceil \gamma (atom(\Re )\cup r(A))\rceil \wedge \lceil A\equiv

2298: rec_{\Re }\rceil \leq \lceil \gamma (atom(\ell ^{\Re })\cup

2299: r(A))\rceil \wedge \lceil A\equiv rec_{(\ell ^{\Re })}\rceil $$

2300: $$\leq \vee \{\lceil \gamma (atom(\wp )\cup r(A))\rceil \wedge

2301: \lceil A\equiv rec_{\wp }\rceil :\wp \in \mathbf{DA}(\Sigma ,\ell

2302: )\},$$ and we complete the proof. $\heartsuit $

2303: 

2304: \smallskip\

2305: 

2306: It should be note that in the above corollary the second

2307: conclusion is obtained from the first one by removing simply the

2308: commutativity. The second conclusion is in general not correct.

2309: The reason is that an essential application is needed in the

2310: derivation of the implication $CReg_\Sigma\longrightarrow

2311: CDReg_\Sigma.$

2312: 

2313: \bigskip\

2314: 

2315: \textbf{5. Orthomodular Lattice-Valued Automata with

2316: $\varepsilon-$Moves}

2317: 

2318: \smallskip\

2319: 

2320: Automata with $\varepsilon-$moves are nondeterministic automata in

2321: which transitions on the empty input $\varepsilon$ are included,

2322: and they have the same power for accepting languages. In the

2323: classical theory of automata, automata with $\varepsilon-$moves

2324: are very convenient tools in building complex automata from simple

2325: ones and in proving the closure properties of regular languages.

2326: The aim of this section is to introduce an orthomodular

2327: lattice-valued extension of automaton with $\varepsilon-$moves.

2328: Let $\ell =<L,\leq ,\wedge ,\vee ,\perp ,0,1>$ be an orthomodular

2329: lattice. Then an $\ell -$valued automaton with $\varepsilon

2330: -$moves over $\Sigma$ is a quadruple $ \Re =<Q,I,T,\delta >$ in

2331: which all components are the same as in an $\ell -$valued

2332: automaton (without $\varepsilon -$moves), but the domain of the

2333: quantum transition relation $\delta $ is changed to $Q\times

2334: (\Sigma \cup \{\varepsilon \})\times Q;$ that is, $\delta $ is a

2335: mapping from $Q\times (\Sigma \cup \{\varepsilon \})\times Q$ into

2336: $L,$ where $\varepsilon $ stands for the empty string of input

2337: symbols. Thus, in an $\ell -$valued automaton with $\varepsilon

2338: -$moves, transitions of the form "$p\stackrel{\delta ,\varepsilon

2339: }{\longrightarrow }q$" are allowed. So, $atom(\Re )$ contains the

2340: atomic propositions "$p\stackrel{\delta ,\varepsilon

2341: }{\longrightarrow }q$", and their truth values are given as

2342: $\delta (p,\varepsilon ,q)$ for all $p,q\in Q.$

2343: 

2344: Now let $\Re =<Q,I,T,\delta >$ be an $\ell -$valued automaton with

2345: $ \varepsilon -$moves. We put $$T_{\varepsilon }(Q,\Sigma

2346: )=(Q(\Sigma \cup \{\varepsilon \}))^{\ast }Q=\cup _{n=0}^{\infty

2347: \lbrack }(Q(\Sigma \cup \{\varepsilon \}))^{n}Q].$$ The difference

2348: between $T(Q,\Sigma )$ and $T_{\varepsilon }(Q,\Sigma )$ is that

2349: in the latter the empty string may be used as labels. For any $

2350: c=q_{0}\sigma_{1} q_{1}...q_{k-1}\sigma _{k}q_{k}\in

2351: T_{\varepsilon }(Q,\Sigma ), $ $lb_{\varepsilon }(c)$ is defined

2352: to be the sequence $\sigma _{1}...\sigma _{k} $ with all

2353: occurrences of $\varepsilon $ deleted. Note that it is possible

2354: that the length of $lb_{\varepsilon }(c)$ is strictly smaller than

2355: $k.$ Then the recognizability $ rec_{\Re }$ is also defined as an

2356: $\ell -$valued unary predicate over $ \Sigma ^{\ast },$ and it is

2357: given by

2358: $$rec_{\Re }(s)\stackrel{def}{=}(\exists c\in T_{\varepsilon

2359: }(Q,\Sigma ))(b(c)\in I\wedge e(c)\in T\wedge lb_{\varepsilon

2360: }(c)=s\wedge path_{\Re }(c))$$ for all $s\in \Sigma ^{\ast },$

2361: where $path_{\Re }$ is defined in the same way as in an $\ell

2362: -$valued automaton without $\varepsilon -$moves. The defining

2363: equation of $rec_\Re$ may be rewritten in terms of truth valued as

2364: follows: $$\lceil rec_\Re (s)\rceil = \vee \{I(b(c))\wedge

2365: T(e(c))\lceil path_\Re (c)\rceil : c\in T_\varepsilon (Q,\Sigma)\

2366: {\rm and}\ lb_\varepsilon (c)=s\},$$ where $$\lceil path_\Re

2367: (c)\rceil = \wedge_{i=0}^{k-1}\delta(q_i,\sigma_{i+1},q_{i+1})$$

2368: if $c=q_0 \sigma_1 q_1 ... q_{k-1} \sigma_k q_k.$

2369: 

2370: For any $\ell -$valued automaton $\Re =<Q,I,T,\delta >$ with

2371: $\varepsilon -$ moves, its $\varepsilon-$reduction is defined to

2372: be the $\ell -$valued automaton $\Re ^{-\varepsilon

2373: }=<Q,I,T^{\prime },\delta ^{\prime }>$ (without $\varepsilon -

2374: $moves) in which

2375: 

2376: (i) for any $q\in Q,$

2377: $$q\in T^{\prime }\stackrel{def}{=}(\exists q\in Q,m\geq 0)(q\in

2378: T\wedge \delta (q_{0},\varepsilon ^{m},q));$$ that is,

2379: $$T^{\prime }(q)=\vee _{q\in Q,m\geq 0}(T(q)\wedge \delta

2380: (q_{0},\varepsilon ^{m},q));$$

2381: 

2382: (ii) for any $p,q\in Q$ and $\sigma \in \Sigma ,$ $$\delta

2383: ^{\prime }(p,\sigma ,q)\stackrel{def}{=}(\exists m,n\geq 0)\delta

2384: (p,\varepsilon ^{m}\sigma \varepsilon ^{n},q);$$ that is,

2385: $$\delta ^{\prime }(p,\sigma ,q)=\vee _{m,n\geq 0}\delta

2386: (p,\varepsilon ^{m}\sigma \varepsilon ^{n},q),$$ where

2387: $$\delta (q_{0},\sigma _{1}...\sigma

2388: _{k},q_{k})\stackrel{def}{=}(\exists q_{1},...,q_{k-1}\in

2389: Q)(\delta (q_{0},\sigma _{1},q_{1})\wedge \delta (q_{1},\sigma

2390: _{2},q_{2})\wedge \delta (q_{k-1},\sigma _{k},q_{k})).$$ In other

2391: words,

2392: $$\delta (q_{0},\sigma _{1}...\sigma _{k},q_{k})=\vee \{(\delta

2393: (q_{0},\sigma _{1},q_{1})\wedge \delta (q_{1},\sigma

2394: _{2},q_{2})\wedge \delta (q_{k-1},\sigma

2395: _{k},q_{k}):q_{1},...,q_{k-1}\in Q\}$$ for all $k\geq 1,$

2396: $q_{0},q_{k}\in Q$ and $\sigma _{1},...,\sigma _{k}\in \Sigma .$

2397: 

2398: The following theorem gives a clear relation between the language

2399: accepted by an orthomodular lattice-valued automaton with

2400: $\varepsilon-$moves and that accepted by its

2401: $\varepsilon-$reduction. In general, the $\varepsilon-$reduction

2402: of an automaton with $\varepsilon-$moves has a stronger power of

2403: acceptance than itself. A certain commutativity between basic

2404: actions of the automaton implies the equivalence between an

2405: automaton with $\varepsilon-$moves and its

2406: $\varepsilon-$reduction. However, an universal validity of such an

2407: equivalence requires that the underlying logic degenerates to the

2408: classical Boolean logic.

2409: 

2410: \smallskip\

2411: 

2412: \textbf{Theorem 5.1.} Let $\ell =<L,\leq ,\wedge ,\vee ,\bot

2413: ,0,1>$ be an orthomodular lattice, and let $\longrightarrow$ be an

2414: implication operator satisfying the Birkhoff-von Neumann

2415: requirement.

2416: 

2417: (1) For any $\ell -$valued automaton $\Re $ with $\varepsilon

2418: -$moves over $ \Sigma ,$ and for any $s\in \Sigma ^{\ast },$

2419: $$\stackrel{\ell }{\models }rec_{\Re }(s)\rightarrow rec_{\Re

2420: ^{-\varepsilon }}(s).$$

2421: 

2422: (2) For any $\ell -$valued automaton $\Re $ with $\varepsilon

2423: -$moves over $ \Sigma ,$ and for any $s\in \Sigma ^{\ast },$

2424: $$\stackrel{\ell }{\models }\gamma (atom(\Re ))\wedge rec_{\Re

2425: ^{-\varepsilon }}(s)\rightarrow rec_{\Re }(s),$$ and in particular

2426: if $\rightarrow =\rightarrow _{3}$ then

2427: $$\stackrel{\ell }{\models }\gamma (atom(\Re ))\rightarrow (rec_{\Re

2428: }(s)\leftrightarrow rec_{\Re ^{-\varepsilon }}(s)).$$

2429: 

2430: (3) The following two statements are equivalent:

2431: 

2432: \ \ \ \ \ \ (i) $\ell $ is a Boolean algebra;

2433: 

2434: \ \ \ \ \ \ (ii) For all $\ell -$valued automaton $\Re $ with

2435: $\varepsilon -$moves over $ \Sigma ,$ and for all $s\in \Sigma

2436: ^{\ast },$

2437: $$\stackrel{\ell }{\models }rec_{\Re }(s)\leftrightarrow rec_{\Re

2438: ^{-\varepsilon }}(s).$$

2439: 

2440: \smallskip\

2441: 

2442: \textbf{Proof.} The proof of (1) is similar to that of (2), so we

2443: omit it. We now prove (2). First, we use induction on the length

2444: $|c|$ of $c$ to show that for any $c\in T(Q,\Sigma ),$

2445: $$claim:\ \ \lceil \gamma (atom(\Re )\rceil \wedge \lceil path_{\Re

2446: ^{-\varepsilon }}(c)\rceil \leq \vee \{\lceil path_{\Re

2447: }(c^{\prime })\rceil :c^{\prime }\in T_{\varepsilon }(Q,\Sigma

2448: ),b(c^{\prime })=b(c),\ \ \ \ \ \ \ \ \ \ $$

2449: $$\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ e(c^{\prime })=e(c)\ {\rm and}\ lb_{\varepsilon }(c^{\prime

2450: })=lb(c)\}.$$ For the case of $|c|=1,$ it is immediate from the

2451: definition of transition relation $\delta ^{\prime }$ in $\Re

2452: ^{-\varepsilon }.$ If $c=c^{\prime }\sigma q,$ then with the

2453: induction hypothesis and Lemmas 2.5 and 2.6, we have

2454: $$\lceil \gamma (atom(\Re ))\rceil \wedge \lceil path_{\Re

2455: ^{-\varepsilon }}(c)\rceil =\lceil \gamma (atom(\Re ))\rceil

2456: \wedge \lceil path_{\Re ^{-\varepsilon }}(c^{\prime })\rceil

2457: \wedge \delta ^{\prime }(e(c^{\prime }),\sigma ,q)$$

2458: $$=\lceil \gamma (atom(\Re ))\rceil \wedge \lceil \gamma (atom(\Re

2459: ))\rceil \wedge \lceil path_{\Re ^{-\varepsilon }}(c^{\prime

2460: })\rceil \wedge \vee _{m,n\geq 0}\delta (e(c^{\prime

2461: }),\varepsilon ^{m}\sigma \varepsilon ^{n},q) $$

2462: $$\leq \vee _{m,n\geq 0}(\lceil \gamma (atom(\Re ))\rceil \wedge

2463: \lceil path_{\Re ^{-\varepsilon }}(c^{\prime })\rceil \wedge

2464: \delta (e(c^{\prime }),\varepsilon ^{m}\sigma \varepsilon

2465: ^{n},q))$$

2466: $$\leq \vee _{m,n\geq 0}[\lceil \gamma (atom(\Re ))\rceil \wedge

2467: \vee \{\lceil path_{\Re }(d^{\prime })\rceil :d^{\prime }\in

2468: T_{\varepsilon }(Q,\Sigma ),b(d^{\prime })=b(c^{\prime

2469: }),e(d^{\prime })=e(c^{\prime })$$ $${\rm and}\ lb_{\varepsilon

2470: }(d^{\prime })=lb(c^{\prime })\}\wedge \delta (e(c^{\prime

2471: }),\varepsilon ^{m}\sigma \varepsilon ^{n},q)]$$

2472: $$\leq \vee \{\lceil \gamma (atom(\Re ))\rceil \wedge \lceil

2473: path_{\Re }(d^{\prime })\rceil \wedge \delta (e(c^{\prime

2474: }),\varepsilon ^{m}\sigma \varepsilon ^{n},q):m,n\geq 0,d^{\prime

2475: }\in T_{\varepsilon }(Q,\Sigma ),$$

2476: $$b(d^{\prime })=b(c^{\prime }),e(d^{\prime })=e(c^{\prime

2477: }),lb_{\varepsilon }(d^{\prime })=lb(c^{\prime })\}.$$

2478: Furthermore, we know that

2479: $$\delta (e(c^{\prime }),\varepsilon ^{m}\sigma \varepsilon

2480: ^{n},q)=\vee \{\delta (e(c^{\prime }),\varepsilon ,p_{1})\wedge

2481: \delta (p_{1},\varepsilon ,p_{2})\wedge ...\wedge \delta

2482: (p_{m-1},\varepsilon ,p_{m})\wedge \delta (p_{m},\sigma ,q_{n})$$

2483: $$\wedge \delta (q_{n},\varepsilon ,q_{n-1})\wedge ...\wedge \delta

2484: (q_{2},\varepsilon ,q_{1})\wedge \delta (q_{1},\varepsilon

2485: ,q):p_{1},...,p_{m},q_{1},...,q_{n}\in Q\}.$$ Again, we use Lemmas

2486: 2.5 and 2.6 and obtain

2487: $$\lceil \gamma (atom(\Re ))\rceil \wedge \lceil path_{\Re

2488: ^{-\varepsilon }}(c)\rceil \leq \vee \{\lceil path_{\Re

2489: }(d^{\prime })\rceil \wedge \delta (e(c^{\prime }),\varepsilon

2490: ,p_{1})\wedge \delta (p_{1},\varepsilon ,p_{2})\wedge ...$$

2491: $$\wedge \delta (p_{m-1},\varepsilon ,p_{m})\wedge \delta

2492: (p_{m},\sigma ,q_{n})\wedge \delta (q_{n},\varepsilon

2493: ,q_{n-1})\wedge ...\wedge \delta (q_{2},\varepsilon ,q_{1})\wedge

2494: \delta (q_{1},\varepsilon ,q):$$ $$m,n\geq 0,d^{\prime }\in

2495: T_{\varepsilon }(Q,\Sigma )\ {\rm with}\ b(d^{\prime

2496: })=b(c^{\prime }),e(d^{\prime })=e(c^{\prime })$$ $${\rm and}\

2497: lb_{\varepsilon }(d^{\prime })=lb(c^{\prime

2498: }),p_{1},...,p_{m},q_{1},...,q_{n}\in Q\}.$$ We put $d=d^{\prime

2499: }\varepsilon p_{1}\varepsilon p_{2}...p_{m-1}\varepsilon

2500: p_{m}\sigma q_{n}\varepsilon q_{n-1}...q_{2}\varepsilon

2501: q_{1}\varepsilon q.$ Then $b(d)=b(d^{\prime })=b(c^{\prime }),$

2502: $e(d)=q=e(c),$ $lb_{\varepsilon }(d)=lb_{\varepsilon }(d^{\prime

2503: })\sigma =lb(c^{\prime })\sigma =lb(c),$ and

2504: $$\lceil path_{\Re }(d)\rceil =\lceil path_{\Re }(d^{\prime

2505: })\rceil \wedge \delta (e(c^{\prime }),\varepsilon ,p_{1})\wedge

2506: \delta (p_{1},\varepsilon ,p_{2})\wedge ...$$

2507: $$\wedge \delta (p_{m-1},\varepsilon ,p_{m})\wedge \delta

2508: (p_{m},\sigma ,q_{n})\wedge \delta (q_{n},\varepsilon

2509: ,q_{n-1})\wedge ...\wedge \delta (q_{2},\varepsilon ,q_{1})\wedge

2510: \delta (q_{1},\varepsilon ,q).$$ Therefore,

2511: $$\lceil \gamma (atom(\Re ))\rceil \wedge \lceil path_{\Re

2512: ^{-\varepsilon }}(c)\rceil \leq \vee \{\lceil path_{\Re }(d)\rceil

2513: :d\in T_{\varepsilon }(Q,\Sigma ),b(d)=b(c),$$ $$e(d)=e(c)\ {\rm

2514: and}\ lb_{\varepsilon }(d)=lb(c)\}$$ and the claim holds for the

2515: case of $|c|=|c^{\prime }|+1.$

2516: 

2517: Now it follows from the above claim and Lemmas 2.5 and 2.6 that

2518: $$\lceil \gamma (atom(\Re ))\rceil \wedge \lceil rec_{\Re

2519: ^{-\varepsilon }}(s)\rceil =\lceil \gamma (atom(\Re ))\rceil

2520: \wedge \lceil \gamma (atom(\Re ))\rceil \wedge \vee

2521: \{I(b(c))\wedge T^{\prime }(e(c))$$

2522: $$\wedge \lceil path_{\Re ^{-\varepsilon }}(c)\rceil :c\in

2523: T(Q,\Sigma ),lb(c)=s\}$$

2524: $$\leq \vee \{\lceil \gamma (atom(\Re ))\rceil \wedge I(b(c))\wedge

2525: T^{\prime }(e(c))\wedge \lceil path_{\Re ^{-\varepsilon

2526: }}(c)\rceil :c\in T(Q,\Sigma ),lb(c)=s\}$$

2527: $$\leq \vee \{\lceil \gamma (atom(\Re ))\rceil \wedge I(b(c))\wedge

2528: T^{\prime }(e(c))\wedge \vee \{\lceil path_{\Re }(c^{\prime

2529: })\rceil :c^{\prime }\in T_{\varepsilon }(Q,\Sigma ),b(c^{\prime

2530: })=b(c),$$

2531: $$e(c^{\prime })=e(c)\ {\rm and}\ lb_{\varepsilon }(c^{\prime

2532: })=lb(c)\}:c\in T(Q,\Sigma ),lb(c)=s\}$$

2533: $$\leq \vee \{\lceil \gamma (atom(\Re ))\rceil \wedge I(b(c))\wedge

2534: T^{\prime }(e(c))\wedge \lceil path_{\Re }(c^{\prime })\rceil

2535: :c\in T(Q,\Sigma ),$$

2536: $$c^{\prime }\in T_{\varepsilon }(Q,\Sigma ),b(c^{\prime

2537: })=b(c),e(c^{\prime })=e(c)\ {\rm and}\ lb_{\varepsilon

2538: }(c^{\prime })=lb(c)=s\}$$

2539: $$=\vee \{\lceil \gamma (atom(\Re ))\rceil \wedge I(b(c))\wedge

2540: \vee _{m\geq 0}(T(q)\wedge \delta (e(c),\varepsilon ^{m},q))\wedge

2541: \lceil path_{\Re }(c^{\prime })\rceil :c\in T(Q,\Sigma ),$$

2542: $$c^{\prime }\in T_{\varepsilon }(Q,\Sigma ),b(c^{\prime

2543: })=b(c),e(c^{\prime })=e(c)\ {\rm and}\ lb_{\varepsilon

2544: }(c^{\prime })=lb(c)=s\}$$ $$\leq \vee \{\lceil \gamma (atom(\Re

2545: ))\rceil \wedge I(b(c))\wedge T(q)\wedge \lceil path_{\Re

2546: }(c^{\prime })\rceil \wedge \delta (e(c),\varepsilon ^{m},q):m\geq

2547: 0,c\in T(Q,\Sigma ),$$

2548: $$c^{\prime }\in T_{\varepsilon }(Q,\Sigma ),b(c^{\prime

2549: })=b(c),e(c^{\prime })=e(c)\ {\rm and}\ lb_{\varepsilon

2550: }(c^{\prime })=lb(c)=s\}$$

2551: $$\leq \vee \{\lceil \gamma (atom(\Re ))\rceil \wedge I(b(c))\wedge

2552: T(q)\wedge \lceil path_{\Re }(c^{\prime })\rceil \wedge \delta

2553: (e(c),\varepsilon ,q_{1})\wedge \delta (q_{1},\varepsilon

2554: ,q_{2})\wedge ...$$

2555: $$\wedge \delta (q_{m-2},\varepsilon ,q_{m-1})\wedge \delta

2556: (q_{m-1},\varepsilon q):m\geq 0,c\in T(Q,\Sigma ),c^{\prime }\in

2557: T_{\varepsilon }(Q,\Sigma ),b(c^{\prime })=b(c),$$

2558: $$e(c^{\prime })=e(c),lb_{\varepsilon }(c^{\prime

2559: })=lb(c)=s,q_{1},...,q_{m-1}\in Q\}.$$ If we write $d=c^{\prime

2560: }\varepsilon q_{1}\varepsilon q_{2}...q_{m-2}\varepsilon

2561: q_{m-1}\varepsilon q,$ then $b(d)=b(c^{\prime })=b(c),$ $e(d)=q,$

2562: $lb_{\varepsilon }(d)=lb(c^{\prime })=s$ and

2563: $$\lceil path_{\Re }(d)\rceil =\lceil path_{\Re }(c^{\prime

2564: })\rceil \wedge \delta (e(c),\varepsilon ,q_{1})\wedge \delta

2565: (q_{1},\varepsilon ,q_{2})\wedge ...\wedge \delta

2566: (q_{m-2},\varepsilon ,q_{m-1})\wedge \delta (q_{m-1},\varepsilon

2567: ,q).$$ Thus,

2568: $$\lceil \gamma (atom(\Re ))\rceil \wedge \lceil rec_{\Re

2569: ^{-\varepsilon }}(s)\rceil \leq \vee \{I(b(d))\wedge T(e(d))\wedge

2570: \lceil path_{\Re }(d)\rceil :d\in T_{\varepsilon }(Q,\Sigma

2571: ),lb_{\varepsilon }(d)=s\}$$

2572: $$=\lceil rec_{\Re }(s)\rceil .$$

2573: 

2574: For (3), the part from (i) to (ii) is immediate from (2) by noting

2575: that $ \lceil \gamma (atom(\Re ))\rceil =1$ always holds in a

2576: Boolean algebra $\ell .$ Conversely, we demonstrate that (ii)

2577: implies (i). For any $a,b,c\in L,$ consider $\ell -$valued

2578: automaton $\Re

2579: =<\{q_{0},q_{1},...,q_{5}\},\{q_{0}\},\{q_{5}\},\delta >$ with

2580: $\varepsilon - $moves in which $\sigma \in \Sigma ,$ $\delta

2581: (q_{0},\sigma ,q_{1})=a,$ $ \delta (q_{1},\varepsilon

2582: ,q_{2})=\delta (q_{1},\varepsilon ,q_{3})=\delta (q_{4},\sigma

2583: ,q_{5})=1,$ $\delta (q_{2},\varepsilon ,q_{4})=b,$ $\delta

2584: (q_{3},\varepsilon ,q_{4})=c,$ and $\delta $ takes values $0$ for

2585: other arguments (see Figure 4).

2586: 

2587: \begin{figure}\centering

2588: \includegraphics{fig_4.eps}\caption{Automaton b} \label{fig 4}

2589: \end{figure}

2590: 

2591: By a routine calculation we know that its $\varepsilon -$reduction

2592: is $\Re ^{-\varepsilon

2593: }=<\{q_{0},q_{1},...,q_{5}\},\{q_{0}\},\{q_{5}\},\delta ^{\prime

2594: }>$ where $\delta ^{\prime }(q_{0},\sigma ,q_{1})=\delta ^{\prime

2595: }(q_{0},\sigma ,q_{2})=\delta ^{\prime }(q_{0},\sigma ,q_{3})=a,$

2596: $\delta ^{\prime }(q_{0},\sigma ,q_{4})=(a\wedge b)\vee (a\wedge

2597: c),$ $\delta ^{\prime }(q_{1},\sigma ,q_{5})=b\vee c,$ $\delta

2598: ^{\prime }(q_{2},\sigma ,q_{5})=b,$ $\delta ^{\prime

2599: }(q_{3},\sigma ,q_{5})=c,$ $\delta ^{\prime }(q_{4},\sigma

2600: ,q_{5})=1,$ and $\delta $ takes value $0$ for other arguments (see

2601: Figure 5). Then it follows from (ii) that

2602: $$a\wedge (b\vee c)=[a\wedge (b\vee c)]\vee (a\wedge b)\vee

2603: (a\wedge c)\vee \lbrack (a\wedge b)\vee (a\wedge c)]$$

2604: $$=\lceil rec_{\Re ^{-\varepsilon }}(\sigma \sigma )\rceil $$

2605: $$=\lceil rec_{\Re }(\sigma \sigma )\rceil $$

2606: $$=(a\wedge b)\vee (a\wedge c).$$

2607: This shows that $\ell $ enjoys the distributivity of meet over

2608: union, and it is a Boolean algebra.$\heartsuit$

2609: 

2610: \begin{figure}\centering

2611: \includegraphics[width=1\textwidth]{fig_5.eps}\caption{Automaton c} \label{fig 5}

2612: \end{figure}

2613: 

2614: \bigskip\

2615: 

2616: \textbf{6. Closure Properties of Orthomodular Lattice-Valued

2617: Regularity}

2618: 

2619: \smallskip\

2620: 

2621: It was shown in the classical automata theory that the class of

2622: regular languages is closed under various operations such as

2623: union, intersection, complement, concatenation, the Kleene

2624: closure, substitution and homomorphism. In this section, we are

2625: going to examine the closure properties of orthomodular

2626: lattice-valued languages under these operations. We first consider

2627: the inverse of an $\ell-$valued language. Let $A\in L^{\Sigma

2628: ^{*}}.$ Then the inverse $A^{-1}\in L^{\Sigma ^{*}}$ of $ A$ is

2629: defined as follows:

2630: $$A^{-1}(\sigma _1...\sigma _m)=A(\sigma _m...\sigma _1)$$ for any

2631: $m\in \omega $ and for any $\sigma _1,...,\sigma _m\in \Sigma .$

2632: 

2633: The following proposition shows that both regularity and

2634: commutative regularity are preserved by the inverse operation.

2635: 

2636: \smallskip\

2637: 

2638: \textbf{Proposition 6.1.} Let $\ell=<L,\leq ,\wedge ,\vee ,\bot

2639: ,0,1>$ be a complete orthomodular lattice, and let

2640: $\longrightarrow $ fulfil the property that $a\leftrightarrow a=1$

2641: for any $a\in L$. Then for any $A\in L^{\Sigma ^{*}},$

2642: $$\stackrel{\ell }{ \models }Reg_\Sigma (A)\leftrightarrow

2643: Reg_\Sigma (A^{-1}),$$ and

2644: $$\stackrel{\ell }{ \models }CReg_\Sigma (A)\leftrightarrow

2645: CReg_\Sigma (A^{-1}).$$

2646: 

2647: \smallskip\

2648: 

2649: \textbf{Proof}. Noting that $A=(A^{-1})^{-1},$ it suffices to show

2650: that $$ \lceil Reg_\Sigma (A)\rceil \leq \lceil Reg_\Sigma

2651: (A^{-1})\rceil .$$ For any $\ell -$valued automaton $\Re

2652: =(Q,I,T,\delta ),$ we define the inverse of $ \Re $ to be the

2653: $\ell -$valued automaton $\Re ^{-1}=(Q,T,I,\delta ^{-1}),$ where

2654: $\delta ^{-1}(p,\sigma ,q)=\delta (q,\sigma ,p)$ for any $p,q\in

2655: Q$ and $\sigma \in \Sigma .$ Then it is easy to see that $rec_{\Re

2656: ^{-1}}=(rec_\Re )^{-1},$ and furthermore we have

2657: $$\lceil

2658: Reg_\Sigma (A)\rceil =\vee \{\lceil A\equiv rec_\Re \rceil :\Re

2659: \in \mathbf{A}(\Sigma ,\ell )\}$$

2660: $$=\vee \{\lceil A^{-1}\equiv

2661: (rec_\Re )^{-1}\rceil :\Re \in \mathbf{A} (\Sigma ,\ell )\}$$

2662: $$=\vee \{\lceil A^{-1}\equiv rec_{\Re ^{-1}}\rceil :\Re \in

2663: \mathbf{A} (\Sigma ,\ell )\}$$

2664: $$\leq \vee \{\lceil A^{-1}\equiv

2665: rec_\wp \rceil :\wp \in \mathbf{A}(\Sigma ,\ell )\}=\lceil

2666: Rec_\Sigma (A^{-1})\rceil .$$. The proof for commutative

2667: regularity is similar. $\heartsuit$

2668: 

2669: \smallskip\

2670: 

2671: The commutative regularity is preserved by the complement

2672: operation, but it is not the case for the regularity predicate.

2673: 

2674: \smallskip\

2675: 

2676: \textbf{Proposition 6.2.} If $\ell =<L,\leq ,\wedge ,\vee ,\perp

2677: ,0,1>$ is a finite orthomodular lattice, and $\rightarrow

2678: =\rightarrow _{3},$ then for any $A\in L^{\Sigma ^{\ast }},$

2679: $$\stackrel{\ell }{\models }CReg_{\Sigma }(A)\rightarrow

2680: CReg_{\Sigma }(A^{c}).$$

2681: 

2682: \smallskip\

2683: 

2684: \textbf{Proof.} For any $\Re =<Q,I,T,\delta >\in \mathbf{A}(\Sigma

2685: ,\ell ),$ we observe that $\ell ^{\Re

2686: }=<L^{Q},I_{1},\overline{T},\overline{\delta }>$ is an $\ell

2687: -$valued deterministic automaton and only $\overline{T}$ carries

2688: $\ell -$valued information. Then we set $(\ell ^{\Re

2689: })^{c}=<L^{Q},I_{1}, \overline{T}^{c},\overline{\delta }>,$ where

2690: for any $X\in L^{Q},$ $

2691: \overline{T}^{c}(X)=(\overline{T}(X))^{c}.$ It is easy to see that

2692: for all $ s\in \Sigma ^{\ast },$ $rec_{(\ell ^{\Re

2693: })^{c}}(s)=(rec_{(\ell ^{\Re })}(s))^{\perp }.$

2694: 

2695: Now by using Theorem 4.1 and Lemmas 2.5 and 2.6 we obtain

2696: $$\lceil \gamma (atom(\Re )\cup r(A)\rceil \wedge \lceil A\equiv

2697: rec_{\Re }\rceil \leq \lceil \gamma (atom(\Re )\cup r(A)\rceil

2698: \wedge \lceil A\equiv rec_{\Re }\rceil \wedge \lceil rec_{\Re

2699: }\equiv rec_{(\ell ^{\Re })}\rceil $$

2700: $$=\wedge _{s\in \Sigma ^{\ast }}(\lceil \gamma (atom(\Re )\cup

2701: r(A)\rceil \wedge (A(s)\rightarrow rec_{\Re }(s))\wedge (rec_{\Re

2702: }(s)\rightarrow rec_{(\ell ^{\Re })}(s)))\wedge $$

2703: $$\wedge _{s\in \Sigma ^{\ast }}(\lceil \gamma (atom(\Re )\cup

2704: r(A)\rceil \wedge (rec_{(\ell ^{\Re })}(s)\rightarrow rec_{\Re

2705: }(s))\wedge (rec_{\Re }(s)\rightarrow A(s)))$$

2706: $$\leq \wedge _{s\in \Sigma ^{\ast }}(\lceil \gamma (atom(\Re )\cup

2707: r(A)\rceil \wedge (A(s)\rightarrow rec_{(\ell ^{\Re })}(s)))\wedge

2708: $$

2709: $$\wedge _{s\in \Sigma ^{\ast }}(\lceil \gamma (atom(\Re )\cup

2710: r(A)\rceil \wedge (rec_{(\ell ^{\Re })}(s)\rightarrow A(s))).$$

2711: Then Lemma 2.11(2) yields

2712: $$\lceil \gamma (atom(\Re )\cup r(A)\rceil \wedge \lceil A\equiv

2713: rec_{\Re }\rceil \leq \wedge _{s\in \Sigma ^{\ast }}(rec_{(\ell

2714: ^{\Re })}^{\perp }(s)\rightarrow A^{\perp }(s))\wedge \wedge

2715: _{s\in \Sigma ^{\ast }}(A^{\perp }(s)\rightarrow rec_{(\ell ^{\Re

2716: })}^{\perp }(s))$$

2717: $$=\wedge _{s\in \Sigma ^{\ast }}(A^{\perp }(s)\leftrightarrow

2718: rec_{(\ell ^{\Re })}^{\perp }(s))$$

2719: $$=\wedge _{s\in \Sigma ^{\ast }}(A^{\perp }(s)\leftrightarrow

2720: rec_{(\ell ^{\Re })^{c}}(s))$$

2721: $$=\lceil A^{c}\equiv rec_{(\ell ^{\Re })^{c}}\rceil .$$

2722: 

2723: In addition, we have $$\lceil \gamma (atom(\Re )\cup r(A)\rceil

2724: \leq \lceil \gamma (atom(\Re )\cup r(A^{c})\rceil $$ from Lemma

2725: 2.5. Therefore,

2726: $$\lceil \gamma (atom(\Re )\cup r(A)\rceil \wedge \lceil A\equiv

2727: rec_{\Re }\rceil \leq \lceil \gamma (atom(\Re )\cup r(A^{c})\rceil

2728: \wedge \lceil A^{c}\equiv rec_{(\ell ^{\Re })^{c}}\rceil $$

2729: $$\leq \lceil CReg_{\Sigma }(A^{c})\rceil .$$

2730: 

2731: Finally, since $\Re $ is allowed to be arbitrary, it follows that

2732: $$\lceil CReg_{\Sigma }(A)\rceil =\vee _{\Re \in

2733: \mathbf{A}(\Sigma ,\ell )}\lceil \gamma (atom(\Re )\cup r(A)\rceil

2734: \wedge \lceil A\equiv rec_{\Re }\rceil $$

2735: $$\leq \lceil CReg_{\Sigma }(A^{c})\rceil .\heartsuit$$

2736: 

2737: \smallskip\

2738: 

2739: We now turn to deal with the union of two $\ell-$valued language.

2740: Let $\Re =<Q_{A},I_{A},T_{A},\delta _{A})$ and $\wp

2741: =<Q_{B},I_{B},T_{B},\delta _{B}>\in \mathbf{A}(\Sigma ,\ell )$ be

2742: two $\ell - $valued automata over $\Sigma .$ We assume that

2743: $Q_{A}\cap Q_{B}=\phi .$ Then the (disjoint) union $\Re \cup \wp $

2744: of $\Re $ and $\wp $ is defined to be $\Im

2745: =(Q_{C},I_{C},T_{C},\delta _{C}),$ where:

2746: 

2747: (i) $Q_{C}=Q_{A}\cup Q_{B};$

2748: 

2749: (ii) $I_{C}=I_{A}\cup I_{B};$

2750: 

2751: (iii) $T_{C}=T_{A}\cup T_{B};$ and

2752: 

2753: (iv) $\delta _{C}:Q_{C}\times \Sigma \times Q_{C}\longrightarrow

2754: L$ is given as follows: for any $p,q\in Q_{C}$ and $\sigma \in

2755: \Sigma ,$

2756: $$\delta _{C}(p,\sigma ,q)=\left\{

2757: \begin{array}{c}

2758: \delta _{A}(p,\sigma ,q)\ {\rm if }\ p,q\in Q_{A}, \\

2759: \delta _{B}(p,\sigma ,q)\ {\rm if }\ p,q\in Q_{B}, \\

2760: 0\ {\rm otherwise.}

2761: \end{array}

2762: \right. $$

2763: 

2764: The following proposition describes the recognizability of the

2765: union of two $\ell-$valued automata. As in the classical theory, a

2766: word $s$ in $\Sigma^{\ast}$ is recognized by the union of two

2767: $\ell-$valued automata if and only if $s$ is recognized by one of

2768: them.

2769: 

2770: \smallskip\

2771: 

2772: \textbf{Proposition 6.3.} Let $\ell=<L,\leq ,\wedge ,\vee ,\bot

2773: ,0,1>$ be a complete orthomodular lattice. If the implication

2774: operator $\longrightarrow $ satisfies that $a\leftrightarrow a=1$

2775: for any $a\in L,$ then for any $\Re ,\wp \in \mathbf{A(\Sigma

2776: ,\ell )}$ and for any $s\in \Sigma ^{\ast },$

2777: $$\stackrel{\ell }{ \models } rec_{\Re \cup \wp

2778: }(s)\longleftrightarrow rec_{\Re }(s)\vee rec_{\wp }(s).$$

2779: 

2780: \smallskip\

2781: 

2782: \textbf{Proof}. Let $s=\sigma _{1}...\sigma _{k}.$ Then

2783: $$\lceil rec_{\Re \cup \wp }(s)\rceil =\vee \{(I_{A}\cup

2784: I_{B})(q_{0})\wedge (T_{A}\cup T_{B})(q_{k})\wedge \wedge

2785: _{i=0}^{k-1}\delta _{A\cup B}(q_{i},\sigma

2786: _{i+1},q_{i+1}):q_{0},q_{1},...,q_{k}\in Q_{A}\cup Q_{B}\}$$

2787: $$=[\vee \{(I_{A}\cup I_{B})(q_{0})\wedge (T_{A}\cup

2788: T_{B})(q_{k})\wedge \wedge _{i=0}^{k-1}\delta _{A\cup

2789: B}(q_{i},\sigma _{i+1},q_{i+1}):q_{0},q_{1},...,q_{k}\in

2790: Q_{A}\}]$$

2791: $$\ \ \ \ \vee \lbrack \vee \{(I_{A}\cup I_{B})(q_{0})\wedge (T_{A}\cup

2792: T_{B})(q_{k})\wedge \wedge _{i=0}^{k-1}\delta _{A\cup

2793: B}(q_{i},\sigma _{i+1},q_{i+1}):q_{0},q_{1},...,q_{k}\in

2794: Q_{B}\}]$$

2795: $$\ \ \ \ \ \ \vee \lbrack \vee \{(I_{A}\cup I_{B})(q_{0})\wedge (T_{A}\cup

2796: T_{B})(q_{k})\wedge \wedge _{i=0}^{k-1}\delta _{A\cup

2797: B}(q_{i},\sigma _{i+1},q_{i+1}):q_{0},q_{1},...,q_{k}\in Q_{A}\cup

2798: Q_{B},$$ $${\rm and\ there\ are}\ i,j\ {\rm such\ that}\ 0\leq

2799: i,j\leq k\ {\rm and}\ q_{i}\in Q_{A}\ {\rm and}\ q_{j}\in

2800: Q_{B}\}].$$ From the definition of $\Re \cup \wp ,$ we know that

2801: for any $ q_{0},q_{1},...,q_{k}\in Q_{A},$ $$(I_{A}\cup

2802: I_{B})(q_{0})=I_{A}(q_{0}),$$ $$(T_{A}\cup

2803: T_{B})(q_{k})=T_{A}(q_{k}),$$

2804: $$\wedge _{i=0}^{k-1}\delta _{A\cup B}(q_{i},\sigma

2805: _{i+1},q_{i+1})=\wedge _{i=0}^{k-1}\delta _{A}(q_{i},\sigma

2806: _{i+1},q_{i+1}),$$ and for any $q_{0},q_{1},...,q_{k}\in Q_{B},$

2807: $$(I_{A}\cup I_{B})(q_{0})=I_{B}(q_{0}),$$

2808: $$(T_{A}\cup T_{B})(q_{k})=T_{B}(q_{k}),$$

2809: $$\wedge _{i=0}^{k-1}\delta _{A\cup B}(q_{i},\sigma

2810: _{i+1},q_{i+1})=\wedge _{i=0}^{k-1}\delta _{B}(q_{i},\sigma

2811: _{i+1},q_{i+1}).$$ If $q_{0},q_{1},...,q_{k}\in Q_{A}\cup Q_{B},$

2812: and there are $i,j$ such that $0\leq i,j\leq k$ and $q_{i}\in

2813: Q_{A}$ and $q_{j}\in Q_{B},$ then we can find some $m\in

2814: \{0,1,...,k-1\}$ such that $q_{m}\in Q_{A}$ and $q_{m+1}\in

2815: Q_{B},$ or $q_{m}\in Q_{B}$ and $q_{m+1}\in Q_{A}.$ Then $\delta

2816: _{A\cup B}(q_{m},\sigma _{m+1},q_{m+1})=0,$ and $$\wedge

2817: _{i=0}^{k-1}\delta _{A\cup B}(q_{i},\sigma _{i+1},q_{i+1})=0.$$

2818: Therefore, it follows that

2819: $$\lceil rec_{\Re \cup \wp }(s)\rceil =[\vee \{I_{A}(q_{0})\wedge

2820: T_{A}(q_{k})\wedge \wedge _{i=0}^{k-1}\delta _{A}(q_{i},\sigma

2821: _{i+1},q_{i+1}):q_{0},q_{1},...,q_{k}\in Q_{A}\}]$$

2822: $$\vee \lbrack \vee \{I_{B}(q_{0})\wedge T_{B}(q_{k})\wedge \wedge

2823: _{i=0}^{k-1}\delta _{B}(q_{i},\sigma

2824: _{i+1},q_{i+1}):q_{0},q_{1},...,q_{k}\in Q_{B}\}]$$

2825: $$=\lceil rec_{\Re }(s)\vee rec_{\wp }(s)\rceil .\heartsuit $$

2826: 

2827: \smallskip\

2828: 

2829: The following corollary slightly generalizes Example 3.1.

2830: 

2831: \smallskip\

2832: 

2833: \textbf{Corollary 6.4}. If $Range(A)=\{A(s):s\in \Sigma^{\ast}\}$

2834: is finite, and $A_\lambda =\{s\in\Sigma^{\ast}:A(s)\geq \lambda\}$

2835: is a regular language (in classical automata theory) for every

2836: $\lambda\in Range(A)$, then

2837: $$\stackrel{\ell }{ \models }Reg_\Sigma (A).$$

2838: 

2839: \smallskip\

2840: 

2841: \textbf{Proof.} Suppose that

2842: $Range(A)=\{\lambda_1,...,\lambda_n\}.$ Then it is easy to see

2843: that

2844: $$A=\cup_{i=1}^{n} \lambda_i A_{\lambda_i}.$$ From Example 3.3 we

2845: know that there exists an $\ell-$valued automaton $\Re_i$ such

2846: that $rec_{\Re_i}=\lambda_i A_{\lambda_i}$ for each $i\leq n$.

2847: Thus, by proposition 6.3 we obtain $$rec_{\cup_{i=1}^{n} \Re_i}

2848: =\cup_{i=1}^{n} \lambda_i A_{\lambda_i}=A$$ and complete the

2849: proof. $\heartsuit$

2850: 

2851: \smallskip\

2852: 

2853: We now consider the product of two $\ell-$valued automata. Let

2854: $\Re =<Q_{A},I_{A},T_{A},\delta _{A})$ and $\wp

2855: =<Q_{B},I_{B},T_{B},\delta _{B}>\in \mathbf{A}(\Sigma ,\ell )$ be

2856: two $\ell -$valued automata over $ \Sigma .$ Then their product

2857: $\Re \times \wp $ is defined to be $\Im =(Q_{C},I_{C},T_{C},\delta

2858: _{C}),$ where:

2859: 

2860: \smallskip\

2861: 

2862: (i) $Q_{C}=Q_{A}\times Q_{B};$

2863: 

2864: (ii) $I_{C}=I_{A}\times I_{B};$

2865: 

2866: (iii) $T_{C}=T_{A}\times T_{B};$ and

2867: 

2868: (iv) $\delta _{C}:Q_{C}\times \Sigma \times Q_{C}\longrightarrow

2869: L$ and for any $p_{a},q_{a}\in Q_{A},$ $p_{b},q_{b}\in Q_{B}$ and

2870: $\sigma \in \Sigma ,$

2871: $$\delta _{C}((p_{a},p_{b}),\sigma ,(q_{a},q_{b}))=\delta

2872: _{A}(p_{a},\sigma ,q_{a})\wedge \delta _{B}(p_{b},\sigma

2873: ,q_{b}).$$

2874: 

2875: \smallskip\

2876: 

2877: It is well-known in the classical automata theory that the

2878: language accepted by the union of two automata is the union of the

2879: languages accepted by these two automata, and the language

2880: accepted by the product of two automata is the intersection of the

2881: languages accepted by the factor automata. Proposition 6.3 shows

2882: that the conclusion about the union of two automata can be

2883: generalized into the theory of automata based on quantum logic

2884: without appealing any additional condition. One may naturally

2885: expect that the conclusion for product of automata can also be

2886: easily generalized into the framework of quantum logic. However,

2887: the case for the product of two automata is much more complicated,

2888: and the following proposition tells us that in order to make the

2889: above conclusion about product of automata still valid in the

2890: automata theory based on quantum logic, a certain commutativity is

2891: necessary to be added on the basic actions of the factor automata.

2892: 

2893: \smallskip\

2894: 

2895: \textbf{Proposition 6.5.} Let $\ell =<L,\leq ,\wedge ,\vee ,\perp

2896: ,0,1>$ be a complete orthomodular lattice.

2897: 

2898: (1) For any $\Re ,\wp \in \mathbf{A}(\Sigma ,\ell ),$ and for any

2899: $s\in \Sigma ^{\ast },$

2900: $$\stackrel{\ell }{\models }rec_{\Re \times \wp }(s)\longrightarrow

2901: rec_{\Re }(s)\wedge rec_{\wp }(s).$$

2902: 

2903: (2) For any $\Re ,\wp \in \mathbf{A}(\Sigma ,\ell ),$ and for any

2904: $s\in \Sigma ^{\ast },$

2905: $$\stackrel{\ell }{\models }\gamma (atom(\Re )\cup atom(\wp ))\wedge

2906: rec_{\Re }(s)\wedge rec_{\wp }(s)\longrightarrow rec_{\Re \times

2907: \wp }(s),$$ and in particular if $\longrightarrow =\longrightarrow

2908: _{3},$ then

2909: $$\stackrel{\ell }{\models}\gamma (atom(\Re )\cup atom(\wp

2910: ))\longrightarrow (rec_{\Re }(s)\wedge rec_{\wp

2911: }(s)\longleftrightarrow rec_{\Re \times \wp }(s)).$$

2912: 

2913: (3) The following two statements are equivalent:

2914: 

2915: \ \ \ \ \ \ (i) $\ell $ is a Boolean algebra.

2916: 

2917: \ \ \ \ \ \ (ii) for all $\Re ,\wp \in \mathbf{A}(\Sigma ,\ell ),$

2918: and for all $s\in \Sigma ^{\ast },$

2919: $$\stackrel{\ell }{\models }rec_{\Re }(s)\wedge rec_{\wp

2920: }(s)\longleftrightarrow rec_{\Re \times \wp }(s).$$

2921: 

2922: \smallskip\

2923: 

2924: \textbf{Proof}. We have directly

2925: $$\lceil rec_{\Re \times \wp }(s)\rceil =\vee \{(I_{A}\times

2926: I_{B})(q_{a0},q_{b0})\wedge (T_{A}\times

2927: T_{B})(q_{ak},q_{bk})\wedge \wedge _{i=0}^{k-1}\delta _{A\times

2928: B}((q_{ai},q_{bi}),$$ $$\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

2929: \ \sigma _{i+1},(q_{a(i+1)},q_{b(i+1)})):

2930: q_{a0},q_{a1},...,q_{ak}\in Q_{A}\ {\rm and}\

2931: q_{b0},q_{b1},...,q_{bk}\in Q_{B}\}$$

2932: $$=\vee \{I_{A}(q_{a0})\wedge I_{B}(q_{b0})\wedge

2933: T_{A}(q_{ak})\wedge T_{B}(q_{bk})\wedge \wedge _{i=0}^{k-1}\delta

2934: _{A}(q_{ai},\sigma _{i+1},q_{a(i+1)})\wedge$$

2935: $$\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \wedge

2936: _{i=0}^{k-1}\delta _{B}(q_{bi},\sigma _{i+1},q_{b(i+1)}):

2937: q_{a0},q_{a1},...,q_{ak}\in Q_{A}\ {\rm and}\

2938: q_{b0},q_{b1},...,q_{bk}\in Q_{B}\}, $$ and

2939: $$\lceil rec_{\Re }(s)\wedge rec_{\wp }(s)\rceil =[\vee

2940: \{I_{A}(q_{0})\wedge T_{A}(q_{k})\wedge \wedge _{i=0}^{k-1}\delta

2941: _{A}(q_{i},\sigma _{i+1},q_{i+1}):q_{0},q_{1},...,q_{k}\in

2942: Q_{A}\}]$$

2943: $$\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \wedge \lbrack \vee \{I_{B}(q_{0})\wedge

2944: T_{B}(q_{k})\wedge \wedge _{i=0}^{k-1}\delta _{B}(q_{i},\sigma

2945: _{i+1},q_{i+1}):q_{0},q_{1},...,q_{k}\in Q_{B}\}]$$ from the

2946: definitions of product and recognizability of $\ell -$valued

2947: automata. It is clear that $$\lceil rec_{\Re \times \wp }(s)\rceil

2948: \leq \lceil rec_{\Re }(s)\wedge rec_{\wp }(s)\rceil .$$ This

2949: indicates that (1) is true. By using Lemmas 2.4(2), 2.5 and 2.6

2950: twice, we can deduce that $$\lceil \gamma (atom(\Re )\cup atom(\wp

2951: ))\wedge rec_{\Re }(s)\wedge rec_{\wp }(s)\rceil \leq \lceil

2952: rec_{\Re \times \wp }(s)\rceil .$$ Thus, (2) is proved. The first

2953: part of (3) that (i) implies (ii) is immediately derivable from

2954: (2) because we have $\lceil \gamma (atom(\Re )\cup atom(\wp

2955: ))\rceil =1$ provided $\ell $ is a Boolean algebra. Conversely, we

2956: show that (ii) implies (i) by constructing two $\ell -$valued

2957: automata and examining the behavior of their product. For any

2958: $a,b,c\in L,$ we choose some $\sigma _{0}\in \Sigma $ and set

2959: $$\Re =(\{p\},\{p\},\{p\},\delta _{A}),$$ where $\delta

2960: _{A}(p,\sigma ,p)=a$ if $\sigma =\sigma _{0}$ and $0$ otherwise,

2961: and $$\wp =(\{q,r,s\},\{q\},\{r,s\},\delta _{B}),$$ where $\delta

2962: _{B}(x,\sigma ,y)=b$ if $x=q,$ $y=r,$ and $\sigma =\sigma _{0};$

2963: $c$ if $x=q,$ $y=s,$ and $\sigma =\sigma _{0},$ $0$ otherwise.

2964: Then $\Re ,\wp \in \mathbf{A}(\Sigma ,\ell ),$ and it is easy to

2965: see that

2966: $$\Re \times \wp

2967: =(\{(p,q),(p,r),(p,s)\},\{(p,q)\},\{(p,r),(p,s)\},\delta _{A\times

2968: B}),$$ where $\delta _{A\times B}((p,x),\sigma ,(p,y))=a\wedge b$

2969: if $x=q,$ $y=r$ and $\sigma =\sigma _{0};$ $a\wedge c$ if $x=q,$

2970: $y=s$ and $\sigma =\sigma _{0};$ and $0$ otherwise (see Figure 6).

2971: Furthermore, by a routine calculation we have

2972: $$\lceil rec_{\Re }(\sigma _{0})\rceil =a,$$

2973: $$\lceil rec_{\wp }(\sigma _{0})\rceil =b\vee c,\ {\rm and}$$

2974: $$\lceil rec_{\Re \times \wp }(\sigma _{0})\rceil =(a\wedge b)\vee

2975: (a\wedge c).$$ Therefore, with (ii) we finally obtain

2976: $$a\wedge b\vee c=\lceil rec_{\Re }(\sigma _{0})\rceil \wedge

2977: \lceil rec_{\wp }(\sigma _{0})\rceil $$ $$=\lceil rec_{\Re \times

2978: \wp }(\sigma _{0})\rceil =(a\wedge b)\vee (a\wedge c).\heartsuit$$

2979: 

2980: \begin{figure}\centering

2981: \includegraphics[width=0.5\textwidth]{fig_6.eps}\caption{Automaton d} \label{fig 6}

2982: \end{figure}

2983: 

2984: \smallskip\

2985: 

2986: To prove the closure property of orthomodular lattice-valued

2987: regularity under the concatenation operation of languages, we

2988: propose the concept of concatenation of two orthomodular

2989: lattice-valued automata. Suppose that $\Re

2990: _{1}=<Q_{1},I_{1},T_{1},\delta _{1}>,$ $\Re

2991: _{2}=<Q_{2},I_{2},T_{2},\delta _{2}>\in \mathbf{A}(\Sigma ,\ell )$

2992: be two $ \ell -$valued automata, and $Q_{1}\cap Q_{2}=\phi .$ We

2993: define the concatenation of $\Re _{1}$ and $\Re _{2}$ to be $\ell

2994: -$valued automaton $ \Re _{1}\Re _{2}=<Q_{1}\cup

2995: Q_{2},I_{1},T_{2},\delta _{2}>$ with $ \varepsilon -$moves, where

2996: $\delta :Q\times (\Sigma \cup \{\varepsilon \})\times Q\rightarrow

2997: L$ is given by

2998: $$\delta (p,\sigma ,q)=\left\{

2999: \begin{array}{c}

3000: \delta _{1}(p,\sigma ,q)\ {\rm if }\ p,q\in Q_{1}\ {\rm and }\

3001: \sigma \neq

3002: \varepsilon  \\

3003: \delta _{2}(p,\sigma ,q)\ {\rm if }\ p,q\in Q_{2}\ {\rm and }\

3004: \sigma \neq

3005: \varepsilon  \\

3006: T_{1}(p)\wedge I_{2}(q)\ {\rm if }\ p\in Q_{1},q\in Q_{2}\ {\rm

3007: and }\ \sigma

3008: =\varepsilon  \\

3009: 0\ {\rm otherwise.}

3010: \end{array}

3011: \right. $$

3012: 

3013: The following proposition clarifies the relation between the

3014: language recognized by the concatenation of two orthomodular

3015: lattice-valued automata and the concatenation of the languages

3016: recognized by the two automata.

3017: 

3018: \smallskip\

3019: 

3020: \textbf{Proposition 6.6}. Let $\ell =<L,\leq ,\wedge ,\vee ,\perp

3021: ,0,1>$ be an orthomodular lattice and $\rightarrow $ fulfil the

3022: Birkhoff-von Neumann requirement.

3023: 

3024: (1) For all $\Re _{1},\Re _{2}\in \mathbf{A}(\Sigma ,\ell ),$ and

3025: for each $ s\in \Sigma ^{\ast },$

3026: $$\stackrel{\ell }{\models }rec_{\Re _{1}\Re _{2}}(s)\rightarrow

3027: (\exists s_{1},s_{2}\in \Sigma ^{\ast })(s_1 s_2=s\wedge rec_{\Re

3028: _{1}}(s_{1})\wedge rec_{\Re _{2}}(s_{2})).$$

3029: 

3030: (2) For all $\Re _{1},\Re _{2}\in \mathbf{A}(\Sigma ,\ell ),$ and

3031: for each $ s\in \Sigma ^{\ast },$

3032: $$\stackrel{\ell }{\models }\gamma (atom(\Re _{1})\cup atom(\Re

3033: _{2}))\wedge (\exists s_{1},s_{2}\in \Sigma ^{\ast })(s_1

3034: s_2=s\wedge $$ $$rec_{\Re _{1}}(s_{1})\wedge rec_{\Re

3035: _{2}}(s_{2}))\rightarrow rec_{\Re _{1}\Re _{2}}(s),$$ and if

3036: $\rightarrow =\rightarrow _{3}$ then

3037: $$\stackrel{\ell }{\models }\gamma (atom(\Re _{1})\cup atom(\Re

3038: _{2}))\rightarrow (rec_{\Re _{1}\Re _{2}}(s)\leftrightarrow

3039: (\exists s_{1},s_{2}\in \Sigma ^{\ast })$$ $$(s_1 s_2=s\wedge

3040: rec_{\Re _{1}}(s_{1})\wedge rec_{\Re _{2}}(s_{2}))).$$

3041: 

3042: (3) The following two statements are equivalent:

3043: 

3044: \ \ \ \ \ \ (i) $\ell $ is a Boolean algebra;

3045: 

3046: \ \ \ \ \ \ (ii) for all $\Re _{1},\Re _{2}\in \mathbf{A}(\Sigma

3047: ,\ell ),$ and for each $ s\in \Sigma ^{\ast },$

3048: $$\stackrel{\ell }{\models }rec_{\Re _{1}\Re _{2}}(s)\leftrightarrow

3049: (\exists s_{1},s_{2}\in \Sigma ^{\ast })(s_1 s_2=s\wedge rec_{\Re

3050: _{1}}(s_{1})\wedge rec_{\Re _{2}}(s_{2})).$$

3051: 

3052: \smallskip\

3053: 

3054: \textbf{Proof}. (1) For any $q_{0},q_{1},...,q_{m}\in Q_{1}\cup

3055: Q_{2},$ $ \sigma _{1},...,\sigma _{m}\in \Sigma \cup \{\varepsilon

3056: \}$ with $\sigma _{1}...\sigma _{m}=s$ (note that it is possible

3057: that $|s|<m$ since $\sigma _{1},...,\sigma _{m}$ may contain

3058: $\varepsilon$'s), if

3059: $$I_{1}(q_{0})\wedge T_{2}(q_{m})\wedge \wedge _{i=1}^{m}\delta

3060: (q_{i-1},\sigma _{i},q_{i})>0,$$ then there exists $j\leq m$ such

3061: that $\sigma _{j}=\varepsilon ,$ $\sigma _{i}\neq \varepsilon $

3062: $(i\neq j),$ $q_{0},...,q_{j-1}\in Q_{1},$ $ q_{j},...,q_{m}\in

3063: Q_{2}.$ Thus, $s=\sigma _{1}...\sigma _{j-1}\sigma _{j+1}...\sigma

3064: _{n},$ and

3065: $$I_{1}(q_{0})\wedge T_{2}(q_{m})\wedge \wedge _{i=1}^{m}\delta

3066: (q_{i-1},\sigma _{i},q_{i})=I_{1}(q_{0})\wedge T_{2}(q_{m})\wedge

3067: \wedge _{i=1}^{j-1}\delta _{1}(q_{i-1},\sigma _{i},q_{i})$$

3068: $$\wedge T_{1}(q_{j-1})\wedge I_{2}(q_{j})\wedge \wedge

3069: _{i=j+1}^{m}\delta _{2}(q_{i-1},\sigma _{i},q_{i})$$

3070: $$=[I_{1}(q_{0})\wedge T_{1}(q_{j-1})\wedge \wedge

3071: _{i=1}^{j-1}\delta _{1}(q_{i-1},\sigma _{i},q_{i})]\wedge \lbrack

3072: I_{2}(q_{j})\wedge T_{2}(q_{m})\wedge \wedge _{i=j+1}^{m}\delta

3073: _{2}(q_{i-1},\sigma _{i},q_{i})] $$

3074: $$\leq rec_{\Re _{1}}(\sigma _{1}...\sigma _{j-1})\wedge rec_{\Re

3075: _{2}}(\sigma _{j+1}...\sigma _{m})$$

3076: $$\leq \vee \{rec_{\Re _{1}}(s_{1})\wedge rec_{\Re

3077: _{2}}(s_{2}):s_{1}s_{2}=s\}.$$

3078: 

3079: (2) First, we can use Lemmas 2.5 and 2.6 to derive that

3080: $$\lceil \gamma (atom(\Re _{1})\cup atom(\Re _{2}))\wedge (\exists

3081: s_{1},s_{2}\in \Sigma ^{\ast })(s_{1}s_{2}=s\wedge rec_{\Re

3082: _{1}}(s_{1})\wedge rec_{\Re _{2}}(s_{2}))\rceil $$

3083: $$=\lceil \gamma (atom(\Re _{1})\cup atom(\Re _{2}))\rceil \wedge

3084: \vee _{s_{1}s_{2}=s}(rec_{\Re _{1}}(s_{1})\wedge rec_{\Re

3085: _{2}}(s_{2}))$$

3086: $$\leq \vee _{s_{1}s_{2}=s}(\lceil \gamma (atom(\Re _{1})\cup

3087: atom(\Re _{2}))\rceil \wedge rec_{\Re _{1}}(s_{1})\wedge rec_{\Re

3088: _{2}}(s_{2})).$$

3089: 

3090: For any $s_{1},s_{2}\in \Sigma ^{\ast }$ with $s_{1}s_{2}=s,$ we

3091: use Lemmas 2.5 and 2.6 again, and this yields

3092: $$\lceil \gamma (atom(\Re _{1})\cup atom(\Re _{2}))\rceil \wedge

3093: rec_{\Re _{1}}(s_{1})\wedge rec_{\Re _{2}}(s_{2})=\lceil \gamma

3094: (atom(\Re _{1})\cup atom(\Re _{2}))\rceil \wedge $$

3095: $$\vee _{lb(c_{1})=s_{1}}(I_{1}(b(c_{1}))\wedge

3096: T_{1}(e(c_{1}))\wedge \lceil path_{\Re _{1}}(s_{1})\rceil )\wedge

3097: \vee _{lb(c_{2})=s_{2}}(I_{2}(b(c_{2}))\wedge

3098: T_{2}(e(c_{2}))\wedge \lceil path_{\Re _{2}}(s_{2})\rceil )$$

3099: $$\leq \vee

3100: _{lb(c_{1})=s_{1},lb(c_{2})=s_{2}}(I_{1}(b(c_{1}))\wedge

3101: T_{1}(e(c_{1}))\wedge \lceil path_{\Re _{1}}(s_{1})\rceil \wedge

3102: I_{2}(b(c_{2}))\wedge T_{2}(e(c_{2}))\wedge \lceil path_{\Re

3103: _{2}}(s_{2})\rceil ).$$

3104: 

3105: Furthermore, for any $c_{1}=p_{0}\sigma _{1}p_{1}...p_{m-1}\sigma

3106: _{m}p_{m}$ and $c_{2}=q_{0}\tau _{1}q_{1}...q_{n-1}\tau _{n}q_{n}$

3107: with $s_{1}=\sigma _{1}...\sigma _{m}$ and $s_{2}=\tau _{1}...\tau

3108: _{n},$

3109: $$I_{1}(b(c_{1}))\wedge T_{1}(e(c_{1}))\wedge \lceil path_{\Re

3110: _{1}}(s_{1})\rceil \wedge I_{2}(b(c_{2}))\wedge

3111: T_{2}(e(c_{2}))\wedge \lceil path_{\Re _{2}}(s_{2})\rceil =$$

3112: $$I_{1}(p_{0})\wedge T_{2}(q_{m})\wedge \wedge _{i=1}^{m}\delta

3113: _{1}(p_{i-1},\sigma _{i},p_{i})\wedge T_{1}(p_{m})\wedge

3114: I_{2}(q_{0})\wedge \wedge _{j=1}^{n}\delta _{2}(q_{j-1},\tau

3115: _{j},q_{j})$$

3116: $$=I_{1}(p_{0})\wedge T_{2}(q_{m})\wedge \lceil path_{\Re _{1}\Re

3117: _{2}}(p_{0}\sigma _{1}p_{1}...p_{m-1}\sigma _{m}p_{m}\varepsilon

3118: q_{0}\tau _{1}q_{1}...q_{n-1}\tau _{n}q_{n})\rceil $$

3119: $$\leq rec_{\Re _{1}\Re _{2}}(s).$$

3120: 

3121: (3) The part that (i) implies (ii) is a simple corollary of (2).

3122: Conversely, it suffices to show that $\ell $ enjoys

3123: distributivity; that is, for any $ a,b,c\in L,$ $a\wedge (b\vee

3124: c)=(a\wedge b)\vee (a\wedge c).$ Let $\Re

3125: _{1}=<\{p_{0},p_{1}\},\{p_{0}\},\{p_{1}\},\delta _{1}>$ and $\Re

3126: _{2}=<\{q_{0},q_{1},q_{2}\},\{q_{0}\},\{q_{1},q_{2}\},\delta

3127: _{2}>,$ where $ \delta _{1}(p_{0},\sigma ,p_{1})=a,$ $\delta

3128: _{2}(q_{0},\sigma ,q_{1})=b,$ $ \delta _{2}(q_{0},\sigma

3129: ,q_{2})=c,$ and $\delta _{1},$ $\delta _{2}$ take value $0$ for

3130: other arguments (see Figure 7). Then it follows that

3131: $$a\wedge (b\vee c)=\lceil (\exists s_{1},s_{2}\in \Sigma ^{\ast

3132: })(s_{1}s_{2}=\sigma \sigma \wedge rec_{\Re _{1}}(s_{1})\wedge

3133: rec_{\Re _{2}}(s_{2}))\rceil $$

3134: $$=\lceil rec_{\Re _{1}\Re _{2}}(\sigma \sigma )\rceil $$

3135: $$=(a\wedge b)\vee (a\wedge c).\heartsuit$$

3136: 

3137: \begin{figure}\centering

3138: \includegraphics[width=1\textwidth]{fig_7.eps}\caption{Automaton e} \label{fig 7}

3139: \end{figure}

3140: 

3141: \smallskip\

3142: 

3143: We now turn to consider the Kleene closure of an orthomodular

3144: lattice-valued language. For this purpose, we need to introduce

3145: the fold construction of an orthomodular lattice-valued automaton.

3146: Let $\Re =<Q,I,T,\delta >\in \mathbf{A}(\Sigma ,\ell )$ be an

3147: $\ell -$valued automaton, and let $q_{0}\notin Q$ be a new state.

3148: We define the fold of $ \Re $ to be $\ell -$valued automaton $\Re

3149: ^{\ast }=<Q\cup \{q_{0}\},\{q_{0}\},T\cup \{q_{0}\},\delta ^{\ast

3150: }>$ with $\varepsilon -$ moves, where

3151: $$\delta ^{\ast }:(Q\cup \{q_{0}\})\times (\Sigma \cup

3152: \{\varepsilon \})\times (Q\cup \{q_{0}\})\rightarrow L$$ is given

3153: by

3154: $$\delta ^{\ast }(p,\sigma ,q)=\left\{

3155: \begin{array}{c}

3156: I(q)\ {\rm if }\ p=q_{0}\ {\rm and }\ \sigma =\varepsilon , \\

3157: \delta (p,\sigma ,q)\ {\rm if }\ p,q\in Q\ {\rm and }\ \sigma \neq

3158: \varepsilon ,

3159: \\

3160: T(p)\wedge I(q)\ {\rm if }\ p,q\in Q\ {\rm and }\ \sigma =\varepsilon , \\

3161: 0\ {\rm otherwise.}

3162: \end{array}

3163: \right. $$

3164: 

3165: The language accepted by the fold of an orthomodular

3166: lattice-valued automaton is then clearly presented by the

3167: following proposition.

3168: 

3169: \smallskip\

3170: 

3171: \textbf{Proposition 6.7}. Let $\ell =<L,\leq ,\wedge ,\vee ,\perp

3172: ,0,1>$ be an orthomodular lattice, and let $\rightarrow $ enjoy

3173: the Birkhoff-von Neumann requirement.

3174: 

3175: (1) For any $\Re \in \mathbf{A}(\Sigma ,\ell )$ and for all $s\in

3176: \Sigma ^{\ast },$

3177: $$\stackrel{\ell }{\models }rec_{\Re ^{\ast }}(s)\rightarrow (\exists

3178: m\geq 0,s_{1},...,s_{m}\in \Sigma ^{\ast })(s_{1}...s_{m}=s\wedge

3179: \wedge _{i=1}^{m}rec_{\Re }(s_{i})).$$

3180: 

3181: (2) For any $\Re \in \mathbf{A}(\Sigma ,\ell )$ and for each $s\in

3182: \Sigma ^{\ast },$

3183: $$\stackrel{\ell }{\models }\gamma (atom(\Re ))\wedge (\exists m\geq

3184: 0,s_{1},...,s_{m}\in \Sigma ^{\ast })(s_{1}...s_{m}=s\wedge \wedge

3185: _{i=1}^{m}rec_{\Re }(s_{i}))\rightarrow rec_{\Re ^{\ast }}(s),$$

3186: and in particular if $\rightarrow =\rightarrow _{3},$ then

3187: $$\stackrel{\ell }{\models }\gamma (atom(\Re ))\rightarrow (rec_{\Re

3188: ^{\ast }}(s)\leftrightarrow (\exists m\geq 0,s_{1},...,s_{m}\in

3189: \Sigma ^{\ast })(s_{1}...s_{m}=s\wedge \wedge _{i=1}^{m}rec_{\Re

3190: }(s_{i}))).$$

3191: 

3192: (3) The following two statements are equivalent:

3193: 

3194: \ \ \ \ \ \ (i) $\ell $ is a Boolean algebra;

3195: 

3196: \ \ \ \ \ \ (ii) for all $\Re \in \mathbf{A}(\Sigma ,\ell )$ and

3197: $s\in \Sigma ^{\ast },$

3198: $$\stackrel{\ell }{\models }rec_{\Re ^{\ast }}(s)\leftrightarrow

3199: (\exists m\geq 0,s_{1},...,s_{m}\in \Sigma ^{\ast

3200: })(s_{1}...s_{m}=s\wedge \wedge _{i=1}^{m}rec_{\Re }(s_{i})).$$

3201: 

3202: \smallskip\

3203: 

3204: \textbf{Proof.} For (1), (2) and the part from (i) to (ii) of (3),

3205: it is similar to the proof of Proposition 6.6, and here we omit

3206: the details. To show that (ii) implies (i), we assume that

3207: $a,b,c\in L$ and want to construct an $\ell -$valued automaton for

3208: which the validity of (ii) leads to $a\wedge (b\vee c)=(a\wedge

3209: b)\vee (a\wedge c).$ Let $\Re

3210: =<\{q_{1},q_{2},...,q_{6}\},\{q_{1},q_{2},q_{3}\},\{q_{6}\},\delta

3211: >$ in which $\delta (q_{1},\sigma ,q_{4})=\delta (q_{3},\sigma

3212: ,q_{5})=1,$ $\delta (q_{2},\sigma ,q_{6})=a,$ $\delta

3213: (q_{4},\sigma ,q_{6})=b,$ $\delta (q_{5},\sigma ,q_{6})=c,$ and

3214: $\delta $ takes value $0$ for the other arguments. Then $\Re

3215: ^{\ast }$ is visualized as Figure 8.

3216: 

3217: \begin{figure}\centering

3218: \includegraphics[width=1\textwidth]{fig_8.eps}\caption{Automaton f} \label{fig 8}

3219: \end{figure}

3220: 

3221: We now have

3222: $$a\wedge (b\vee c)=\lceil (\exists m\geq 0,s_{1},...,s_{m}\in

3223: \Sigma ^{\ast })(s_{1}...s_{m}=\sigma ^{3}\wedge \wedge

3224: _{i=1}^{m}rec_{\Re }(s_{i}))\rceil $$

3225: $$=rec_{\Re ^{\ast }}(\sigma ^{3})$$

3226: $$=(a\wedge b)\vee (a\wedge c).\heartsuit$$

3227: 

3228: \smallskip\

3229: 

3230: From the above proposition, we are able to demonstrate that the

3231: predicate $CReg_\Sigma$ is preserved by the Kleene closure. The

3232: corresponding result for the predicate $Reg_\Sigma$ is not true in

3233: general.

3234: 

3235: \smallskip\

3236: 

3237: \textbf{Corollary 6.8.} Let $\ell =<L,\leq ,\wedge ,\vee ,\perp

3238: ,0,1>$ be an orthomodular lattice, and let $\rightarrow

3239: =\rightarrow _{3}.$ Then for any $ A\in L^{\Sigma ^{\ast }},$

3240: $$\stackrel{\ell }{\models }CReg_{\Sigma }(A)\longrightarrow

3241: CReg_{\Sigma }(A^{\ast }).$$

3242: 

3243: \smallskip\

3244: 

3245: \textbf{Proof}. It is similar to the proof of Proposition 6.2. The

3246: point here is to show the following inequality:

3247: $$\lceil \gamma (atom(\Re )\cup r(A))\rceil \wedge \lceil A\equiv

3248: rec_{\Re }\rceil \leq \lceil A^{\ast }\equiv rec_{\Re ^{\ast

3249: }}\rceil $$ for any $\Re\in \mathbf{A}(\Sigma, \ell).$ In fact, by

3250: using Lemma 2.11(1) we have

3251: $$\lceil \gamma (atom(\Re )\cup r(A))\rceil \wedge \lceil A\equiv

3252: rec_{\Re }\rceil =\lceil \gamma (atom(\Re )\cup r(A))\rceil \wedge

3253: \wedge _{s\in \Sigma ^{\ast }}(A(s)\leftrightarrow rec_{\Re

3254: }(s))$$

3255: $$\leq \lceil \gamma (atom(\Re )\cup r(A))\rceil \wedge \wedge

3256: _{s\in \Sigma ^{\ast }}(\vee _{s_{1}...s_{m}=s}\wedge

3257: _{i=1}^{m}A(s_{i})\leftrightarrow \vee _{s_{1}...s_{m}=s}\wedge

3258: _{i=1}^{m}rec_{\Re }(s_{i}))$$

3259: $$=\lceil \gamma (atom(\Re )\cup r(A))\rceil \wedge \lceil A^{\ast

3260: }\equiv (rec_{\Re })^{\ast }\rceil .$$

3261: 

3262: On the other hand, it follows from Proposition 6.7 that $$\lceil

3263: \gamma (atom(\Re ))\rceil \leq \lceil (rec_{\Re })^{\ast }\equiv

3264: rec_{\Re ^{\ast }}\rceil .$$ Then with Lemma 2.11(3) we obtain

3265: $$\lceil \gamma (atom(\Re )\cup r(A))\rceil \wedge \lceil A\equiv

3266: rec_{\Re }\rceil \leq \lceil \gamma (atom(\Re )\cup r(A))\rceil

3267: \wedge \lceil A^{\ast }\equiv (rec_{\Re })^{\ast }\rceil$$ $$

3268: \wedge \lceil (rec_{\Re })^{\ast }\equiv rec_{\Re ^{\ast }}\rceil

3269: $$

3270: $$\leq \lceil A^{\ast }\equiv rec_{\Re ^{\ast }}\rceil .\heartsuit$$

3271: 

3272: \smallskip\

3273: 

3274: To conclude this section, we show that both the predicate

3275: $Reg_\Sigma$ and $CReg_\Sigma$ are preserved by the pre-image of a

3276: homomorphism between two languages. But the closure property of an

3277: orthomodular lattice-valued language under homomorphism is left to

3278: be examined in the next section, after the notion of orthomodular

3279: lattice-valued regular expression is proposed. Let $\Sigma $ and

3280: $\Gamma $ be two alphabets of input symbols. Then each mapping

3281: $h:\Sigma \rightarrow \Gamma ^{\ast }$ can be uniquely extended to

3282: a homomorphism $h:\Sigma ^{\ast }\rightarrow \Gamma ^{\ast }$ such

3283: that $ h(\varepsilon )=\varepsilon $ and

3284: $$h(xy)=h(x)h(y)$$ for all $x,y\in \Sigma ^{\ast }.$ Furthermore, we

3285: may define images of $\ell -$valued subsets of $ \Sigma ^{\ast }$

3286: under $h$ and pre-images of $\ell -$valued subsets of $ \Gamma

3287: ^{\ast }$ under $h.$ Recall that for any $A\in L^{\Sigma ^{\ast

3288: }}$ and $B\in L^{\Gamma ^{\ast }},$ $h(A)\in L^{\Gamma ^{\ast }}$

3289: and $h^{-1}(B)\in L^{\Sigma ^{\ast }}$ are given as follows:

3290: $$h(A)(t)=\vee \{A(s):s\in \Sigma ^{\ast }\ {\rm and}\ h(s)=t\}$$

3291: for each $t\in \Gamma ^{\ast },$ and

3292: $$h^{-1}(B)(s)=B(h(s))$$

3293: for each $s\in \Sigma ^{\ast }.$

3294: 

3295: Let $\Re =<Q,I,T,\delta >\in \mathbf{A}(\Gamma ,\ell )$ be an

3296: $\ell -$valued automaton over $\Gamma .$ Then the pre-image of

3297: $\Re $ under $h$ is defined to be an $\ell -$valued automaton

3298: $$h^{-1}(\Re )=<Q,I,T,h^{-1}(\delta )>\in \mathbf{A}(\Sigma ,\ell

3299: )$$ over $\Sigma ,$ where for any $p,q\in Q$ and $ \sigma \in

3300: \Sigma ,$

3301: $$h^{-1}(\delta )(p,\sigma ,q)=\delta (p,h(\sigma ),q).$$

3302: 

3303: The pre-image of a homomorphism has a very nice compatibility with

3304: the predicates $reg_\Sigma$ and $CReg_\Sigma$, and no

3305: commutativity is needed here.

3306: 

3307: \smallskip\

3308: 

3309: \textbf{Proposition 6.9.} Let $\ell =<L,\leq ,\wedge ,\vee ,\perp

3310: ,0,1>$ be an orthomodular lattice, let $\rightarrow $ enjoy the

3311: Birkhoff-von Neumann requirement, and let $h:\Sigma \rightarrow

3312: \Gamma ^{\ast }$ be a mapping. Then for any $\Re \in

3313: \mathbf{A}(\Gamma ,\ell )$ and for any $s\in \Sigma ^{\ast },$

3314: $$\stackrel{\ell }{\models} rec_{h^{-1}(\Re )}(s)\longleftrightarrow rec_{\Re

3315: }(h(s)).$$

3316: 

3317: \smallskip\

3318: 

3319: \textbf{Proof.} Suppose that $s=\sigma _{1}\sigma _{2}...\sigma

3320: _{n}.$ Then

3321: $$\lceil rec_{h^{-1}(\Re )}(s)\rceil =\vee \{I(q_{0})\wedge

3322: T(q_{n})\wedge \wedge _{i=0}^{n-1}h^{-1}(\delta )(q_{i},\sigma

3323: _{i+1},q_{i+1}):q_{0},q_{1},...,q_{n}\in Q\}$$

3324: $$=\vee \{I(q_{0})\wedge T(q_{n})\wedge \wedge _{i=0}^{n-1}\delta

3325: (q_{i},h(\sigma _{i+1}),q_{i+1}):q_{0},q_{1},...,q_{n}\in Q\}$$

3326: $$=\lceil rec_{\Re }(h(\sigma _{1})h(\sigma _{2})...h(\sigma

3327: _{n}))\rceil $$

3328: $$=\lceil rec_{\Re }(h(s))\rceil .\heartsuit$$

3329: 

3330: \smallskip\

3331: 

3332: \textbf{Corollary 6.10.} Let $\ell =<L,\leq ,\wedge ,\vee ,\perp

3333: ,0,1>$ be an orthomodular lattice, let $\rightarrow $ enjoy the

3334: Birkhoff-von Neumann requirement, and let $h:\Sigma \rightarrow

3335: \Gamma ^{\ast }$ be a mapping. Then for any $B\in L^{\Gamma ^{\ast

3336: }},$

3337: $$\stackrel{\ell }{\models} Reg_{\Gamma }(B)\rightarrow Reg_{\Sigma

3338: }(h^{-1}(B)),$$ and

3339: $$\stackrel{\ell }{\models} CReg_{\Gamma }(B)\rightarrow CReg_{\Sigma

3340: }(h^{-1}(B)),$$

3341: 

3342: \smallskip\

3343: 

3344: \textbf{Proof.} From the above proposition we have

3345: $$h^{-1}(rec_{\Re })(s)=rec_{\Re }(h(s))=rec_{h^{-1}(\Re )}(s)$$

3346: for all $s\in \Sigma ^{\ast }.$ Then with Lemma 2.12 we obtain

3347: $$\lceil Rec_{\Gamma }(B)\rceil =\vee \{\lceil B\equiv

3348: rec_{\Re }\rceil :\Re \in \mathbf{A}(\Gamma ,\ell )\}$$

3349: $$\leq \vee \{\lceil h^{-1}(B)\equiv h^{-1}(rec_{\Re })\rceil :\Re

3350: \in \mathbf{A}(\Gamma ,\ell )\}$$

3351: $$=\vee \{\lceil h^{-1}(B)\equiv rec_{h^{-1}(\Re )}\rceil :\Re \in \mathbf{A}

3352: (\Gamma ,\ell )\}$$

3353: $$\leq \vee \{\lceil h^{-1}(B)\equiv rec_{\wp }\rceil :\wp \in \mathbf{A}

3354: (\Sigma ,\ell )\}$$

3355: $$=\lceil Reg_{\Sigma }(h^{-1}(B))\rceil .$$

3356: 

3357: It is similar for the case of commutative regularity.$\heartsuit$

3358: 

3359: \bigskip\

3360: 

3361: \textbf{7. Orthomodular Lattice-Valued Regular Expressions}

3362: 

3363: \smallskip\

3364: 

3365: One of the most interesting results in classical automata theory

3366: is the Kleene theorem which shows the equivalence between finite

3367: automata and regular expressions. The main aim of this section is

3368: to present an orthomodular lattice-valued generalization of the

3369: Kleene theorem. Let $\ell =<L,\leq ,\wedge ,\vee ,\bot ,0,1>$ be

3370: an orthomodular lattice, and let $\Sigma$ be an nonempty set of

3371: input symbols. Then the language of $\ell-$valued regular

3372: expressions over $\Sigma$ has the alphabet

3373: $(\Sigma\cup\{\varepsilon,\phi\})\cup(L\cup\{+,\cdot ,*\})$. The

3374: symbols in $\Sigma\cup\{\varepsilon,\phi\}$ will be used to stand

3375: for atomic expressions, and the symbols in $L\cup\{+,\cdot ,*\}$

3376: will be used to denote operators for building up compound

3377: expressions: $*$ and all $\lambda\in L$ are unary operators, and

3378: $+,\cdot$ are binary ones. We use $\alpha,\beta,...$ to act as

3379: meta-symbols for regular expressions and $L(\alpha)$ for the

3380: language denoted by expression $\alpha$. More explicitly,

3381: $L(\alpha)$ will be used to denote an $\ell-$valued subset of

3382: $\Sigma^{*}$; that is, $L(\alpha)\in L^{\Sigma^{*}}$. Orthomodular

3383: lattice-valued regular expressions and the orthomodular

3384: lattice-valued languages denoted by them are formally defined as

3385: follows:

3386: 

3387: (i) For each $a\in\Sigma$, $a$ is a regular expression, and

3388: $L(a)={a}$; $\varepsilon$ and $\phi$ are regular expressions, and

3389: $L(\varepsilon)={\varepsilon}$, $L(\phi)=\phi$.

3390: 

3391: (ii) If both $\alpha$ and $\beta$ are regular expressions, then

3392: for each $\lambda\in L$, $\lambda\alpha$ is a regular expression,

3393: and $$L(\lambda\alpha)=\lambda L(\alpha);$$ and $\alpha + \beta$,

3394: $\alpha \cdot \beta$ and $\alpha ^{*}$ are all regular

3395: expressions, and

3396: $$L(\alpha +\beta)=L(\alpha)\cup L(\beta),$$ $$L(\alpha \cdot

3397: \beta)=L(\alpha)\cot L(\beta),$$ $$L(\alpha ^{*})=L(\alpha)

3398: ^{*}.$$ It is easy to see that the only difference between

3399: orthomodular lattice-valued regular expressions and the classical

3400: ones is that the additional unary (scalar) operators $\lambda\in

3401: L$ are permitted to occur in the former.

3402: 

3403: The central part of the Kleene theorem is a mechanism to transform

3404: a finite automaton into a regular expression. This mechanism has a

3405: straightforward extension in the framework of orthomodular

3406: lattice-valued automata. Let $\Re =<Q,I,T,\delta >\in

3407: \mathbf{A}(\Sigma ,\ell )$ be an $\ell -$valued automaton over

3408: $\Sigma .$ For any $u,v\in Q$ and $X\subseteq Q,$ $\alpha

3409: _{uv}^{X}$ is defined by induction on the cardinality $|X| $ of

3410: $X:$

3411: 

3412: (1) $$\alpha _{uv}^{\phi }=\left\{

3413: \begin{array}{c}

3414: \Sigma_{\sigma \in \Sigma }\delta (u,\sigma ,v)\sigma \ {\rm if}\

3415: u\neq

3416: v, \\

3417: \varepsilon +\Sigma_{\sigma \in \Sigma }\delta (u,\sigma ,v)\sigma

3418: \ {\rm if}\ u=v.

3419: \end{array}

3420: \right. $$

3421: 

3422: (2) if $X\neq \phi ,$ then we choose any $q\in X$ and define

3423: $$\alpha _{uv}^{X}=\alpha _{uv}^{X-\{q\}}+\alpha

3424: _{uq}^{X-\{q\}}\cdot (\alpha _{qq}^{X-\{q\}})^{\ast }\cdot \alpha

3425: _{qv}^{X-\{q\}}.$$ Then the $\ell -$valued regular expression

3426: $$k(\Re )=\Sigma_{u,v\in Q}(I(u)\wedge T(v))\alpha

3427: _{uv}^{Q}$$ is called a Kleene representation of $\Re .$

3428: 

3429: The following theorem describes properly the relationship between

3430: the language recognized by an orthomodular lattice-valued

3431: automaton and the language expressed by its Kleene representation.

3432: 

3433: \smallskip\

3434: 

3435: \textbf{Theorem 7.1. } Let $\ell =<L,\leq ,\wedge ,\vee ,\bot

3436: ,0,1>$ be an orthomodular lattice, and let $\rightarrow$ satisfy

3437: the Birkhoff-von Neumann requirement.

3438: 

3439: (1) For any $\Re \in \mathbf{A}(\Sigma ,\ell )$ and $s\in \Sigma

3440: ^{\ast },$ if $k(\Re)$ is a Kleene representation of $\Re$, then

3441: $$\stackrel{\ell }{\models} rec_{\Re }(s)\longrightarrow s\in L(k(\Re

3442: )).$$

3443: 

3444: (2) For any $\Re \in \mathbf{A}(\Sigma ,\ell )$ and $s\in \Sigma

3445: ^{\ast },$ and for any Kleene representation $k(\Re)$ of $\Re$,

3446: $$\stackrel{\ell }{\models} \gamma(atom(\Re))\wedge s\in L(k(\Re))\longrightarrow rec_\Re

3447: (s),$$ and especially if $\longrightarrow =\longrightarrow_3$,

3448: then $$\stackrel{\ell }{\models} \gamma(atom(\Re))\longrightarrow

3449: (rec_\Re (s)\longleftrightarrow s\in L(k(\Re))).$$

3450: 

3451: (3) The following two statements are equivalent:

3452: 

3453: \ \ \ \ \ \ (i) $\ell $ is a Boolean algebra.

3454: 

3455: \ \ \ \ \ \ (ii) For any $\Re \in \mathbf{A}(\Sigma ,\ell )$ and

3456: $s\in \Sigma ^{\ast },$ and for any Kleene representation $k(\Re)$

3457: of $\Re$,

3458: $$\stackrel{\ell }{\models} rec_{\Re }(s)\longleftrightarrow s\in L(k(\Re

3459: )).$$

3460: 

3461: \smallskip\

3462: 

3463: \textbf{Proof.} We prove (1) and (2) together. To this end, we

3464: have to demonstrate that for any $u,v\in Q,$ $X\subseteq Q$ and

3465: $s\in \Sigma ^{\ast },$ $$(a)\ \vee \{\lceil path_{\Re

3466: }(c)\rceil:c\in T(Q,\Sigma ),b(c)=u,e(c)=v,M(c)\subseteq

3467: X,lb(c)=s\}\leq L(\alpha _{uv}^{X})(s),$$

3468: $$(b)\ \lceil\gamma(atom(\Re))\rceil\wedge L(\alpha _{uv}^{X})(s)\leq\ \ \ \ \ \

3469: \ \ \ \ \ \ \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \ \

3470: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3471: $$

3472: $$\ \ \ \ \ \ \ \ \vee \{\lceil path_{\Re }(c)\rceil:c\in T(Q,\Sigma ),b(c)=u,e(c)=v,M(c)\subseteq

3473: X,lb(c)=s\},$$ where $M(c)$ stands for the set of states along $c$

3474: except $u$ and $v;$ more exactly, $M(c)=\{q_{1},...,q_{k-1}\}$ if

3475: $c=u\sigma _{1}q_{1}...q_{k-1}\sigma _{k}v.$ This claim may be

3476: proved by induction on $ |X|.$ For the case of $X=\phi ,$ it is

3477: easy. We now suppose that $q\in X\neq \phi $ and $$\alpha

3478: _{uv}^{X}=\alpha _{uv}^{X-\{q\}}+[\alpha _{uq}^{X-\{q\}}(\alpha

3479: _{qq}^{X-\{q\}})^{\ast }]\alpha _{qv}^{X-\{q\}}.$$ We first show

3480: that (a) is valid in this case. From the induction hypothesis we

3481: have $$(c)\ \vee \{\lceil path_{\Re }(c)\rceil :c\in T(Q,\Sigma

3482: ),b(c)=e(c)=q,\ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ \ \ \ \ \ \ \

3483: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $$

3484: $$\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3485: M(c)\subseteq X-\{q\}, lb(c)=s\}\leq L(\alpha

3486: _{qq}^{X-\{q\}})(s)$$ for each $s\in \Sigma ^{\ast }.$ Then we

3487: assert that for all $s\in \Sigma ^{\ast},$

3488: $$(d)\ \vee \{\lceil path_{\Re }(c)\rceil :c\in

3489: T(Q,\Sigma ),b(c)=e(c)=q,M(c)\subseteq X,lb(c)=s\}

3490:  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $$

3491: $$\leq L((\alpha

3492: _{qq}^{X-\{q\}})^{\ast })(s).$$ In fact, for any $c\in T(Q,\Sigma

3493: )$ if $b(c)=e(c)=q,M(c)\subseteq X$ and $ lb(c)=s,$ we write

3494: $c_{i}$ for the substring of $c$ beginning with the $i$th $q $ and

3495: ending at the $(i+1)$th $q.$ If the number of occurrences of $q$

3496: in $c$ is $m+1,$ then

3497: $$\lceil path_{\Re }(c)\rceil =\wedge _{i=1}^{m}\lceil path_{\Re }(c_{i})\rceil .$$

3498: Furthermore, by using (c) and noting that

3499: $s=lb(c_{1})...lb(c_{m})$ we obtain

3500: $$\lceil path_{\Re }(c)\rceil =\wedge _{i=1}^{m}L(\alpha

3501: _{qq}^{X-\{q\}})(lb(c_{i}))\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3502: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3503: \ \ \ \ \ \ \ $$

3504: $$\leq\vee\{\wedge_{i=1}^{n} L(\alpha_{qq}^{X-\{q\}})(s_i):n\geq

3505: 0, s_1,...,s_n\in \Sigma^{*},s=s_1...s_n\}$$

3506: $$=(L(\alpha _{qq}^{X-\{q\}}))^{\ast }(s)$$

3507: $$= L((\alpha _{qq}^{X-\{q\}})^{\ast })(s).$$

3508: Let $c$ range over $\{c\in T(Q,\Sigma ):b(c)=e(c)=q,M(c)\subseteq

3509: X,lb(c)=s\}.$ Then (d) is proved.

3510: 

3511: Furthermore, from the induction hypothesis and (d) we have

3512: $$([L(\alpha _{uq}^{X-\{q\}})L((\alpha _{qq}^{X-\{q\}})^{\ast

3513: })]L(\alpha _{qv}^{X-\{q\}}))(s)=\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3514: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3515: \ \ $$

3516: $$\vee \{[L(\alpha_{uq}^{X-\{q\}})L((\alpha_{qq}^{X-\{q\}})^{\ast})](x)

3517: \wedge L(\alpha_{qv}^{X-\{q\}})(y):s=xy\} $$

3518: $$=\vee \{\vee\{L(\alpha_{uq}^{X-\{q\}})(x_1)\wedge

3519: L((\alpha_{qq}^{X-\{q\}})^{\ast})(x_2):x=x_1 x_2\} \wedge

3520: L(\alpha_{qv}^{X-\{q\}})(y):s=xy\}\ \ $$

3521: $$\geq \vee \{L(\alpha_{uq}^{X-\{q\}})(x_1)\wedge

3522: L((\alpha_{qq}^{X-\{q\}})^{\ast})(x_2) \wedge

3523: L(\alpha_{qv}^{X-\{q\}})(y):s=x_1x_2y\}\ \ \ \ \ \ \ \ \ \ \ \ \ \

3524: \ \ \ $$

3525: $$\geq \vee \{\lceil path_{\Re }(c_{1})\rceil \wedge \lceil path_{\Re }(c_{2})\rceil \wedge \lceil path_{\Re

3526: }(c_{3})\rceil : c_{1},c_{2},c_{3}\in T(Q,\Sigma),\ \ \ \ \ \ \ \

3527: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $$

3528: $$\ \ \ \ b(c_{1})=u, e(c_{1})=b(c_{2})=e(c_{2})=b(c_{3})=q, e(c_{3})=v,s=lb(c_{1})lb(c_{2})lb(c_{3})\}$$

3529: $$=\vee \{\lceil path_{\Re }(c)\rceil :c\in T(Q,\Sigma ),b(c)=u,e(c)=v,q\in

3530: M(c)\}.\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3531: \ \ $$ This yields further

3532: $$L(\alpha _{uv}^{X})(s)=L(\alpha _{uv}^{X-\{q\}})(s)\vee

3533: ([L(\alpha _{uq}^{X-\{q\}})L((\alpha _{qq}^{X-\{q\}})^{\ast

3534: }]L(\alpha _{qv}^{X-\{q\}}))(s)$$

3535: $$\geq \ {\rm the\ left-hand\ side\ of\ (a)}.$$

3536: 

3537: We now turn to consider (b). The induction hypothesis gives

3538: $$(e)\ \lceil \gamma(atom(\Re))\rceil \wedge L(\alpha_{uv}^{X-\{q\}})(s)\leq \{\lceil path_\Re (c)\rceil :c\in

3539: T(Q,\Sigma),\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3540: \ \ \ \ \ \ \ \ \ \ \ \ \ $$

3541: $$b(c)=u, e(c)=v, M(c)\subseteq X-\{q\}, lb(c)=s \}.$$ For any

3542: $n\geq 0$ and $s_{1},...,s_{n}\in \Sigma ^{\ast }$ with $

3543: s=s_{1}...s_{n},$ from (e) we can apply Lemmas 2.5 and 2.6 to

3544: obtain

3545: $$\lceil \gamma(atom(\Re))\rceil \wedge \wedge

3546: _{i=1}^{n}L(\alpha _{qq}^{X-\{q\}})(s_{i})=\lceil

3547: \gamma(atom(\Re))\rceil \wedge \wedge_{i=1}^{n}[\lceil

3548: \gamma(atom(\Re))\rceil \wedge L(\alpha_{qq}^{X-\{q\}})(s_i)]$$

3549: $$\leq \lceil \gamma(atom(\Re))\rceil \wedge \wedge _{i=1}^{n}\vee \{\lceil path_{\Re

3550: }(c_{i})\rceil :c_{i}\in T(Q,\Sigma ),\ \ \ \ \ \ \ \ \ \ \ \ \ \

3551: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3552: \

3553: $$

3554: $$b(c_{i})=e(c_{i})=q,M(c_{i})\subseteq X-\{q\},lb(c_{i})=s_{i}\}$$

3555: $$\leq \vee \{\wedge _{i=1}^{n}\lceil path_{\Re }(c_{i})\rceil :c_{i}\in T(Q,\Sigma

3556: ),b(c_{i})=e(c_{i})=q, M(c_{i})\subseteq X-\{q\},\ \ \ \ \ \ \ \ \

3557: \ \ \ \ \ \ \ \ \ \ $$

3558: $$lb(c_{i})=s_{i}\ {\rm for\ each}\ i=1,2,...,n\}$$

3559: $$\leq \vee \{\lceil path_{\Re }(\overline{c_{1}...c_{n}})\rceil :c_{i}\in T(Q,\Sigma

3560: ),b(c_{i})=e(c_{i})=q, M(c_{i})\subseteq X-\{q\},\ \ \ \ \ \ \ \ \

3561: \ \ \ \ \ \ \ \ \ \ $$

3562: $$lb(c_{i})=s_{i}\ {\rm for\ each}\ i=1,2,...,n\},$$ where

3563: $\overline{c_{1}...c_{n}}=c_{1}c_{2}^{\prime }...c_{n}^{\prime },$

3564: $c_{i}^{\prime }$ is the resulting string after removing the first

3565: $q$ in $c_{i}$ for each $i\geq 2.$ Note that

3566: $lb(\overline{c_{1}...c_{n}} )=s_{1}...s_{n}=s$ whenever

3567: $lb(c_{i})=s_{i}$ $(i=1,2,...,n).$ We write

3568: $$\lambda=\vee \{\lceil path_\Re (c)\rceil :c\in T(Q,\Sigma), b(c)=e(c)=q, M(c)\subseteq X,

3569: lb(c)=s\}.$$ Then it holds that

3570: $$\lceil \gamma(atom(\Re))\rceil \wedge \wedge _{i=1}^{n}L(\alpha _{qq}^{X-\{q\}})(s_{i})\leq\lambda.$$

3571: Moreover, note that $\lceil \gamma(atom(\Re))\rceil ,

3572: L(\alpha_{qq}^{X-\{q\}})(s_i)\in [atom(\Re)].$ It follows that

3573: $$\lceil \gamma(atom(\Re))\rceil \wedge L((\alpha_{qq}^{X-\{q\}})^{\ast})(s)=\lceil \gamma(atom(\Re))\rceil \wedge

3574: \lceil \gamma(atom(\Re))\rceil \wedge\ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3575: \ \ \ \ \ \ \ \ \ \ \ \ $$

3576: $$\vee\{\wedge_{i=1}^{n}L(\alpha_{qq}^{X-\{q\}})(s_i):n\geq 0,

3577: s=s_1...s_n \}$$

3578: $$\leq \vee\{\lceil \gamma(atom(\Re))\rceil \wedge \wedge_{i=1}^{n}L(\alpha_{qq}^{X-\{q\}})(s_i):n\geq 0,

3579: s=s_1...s_n \}\leq \lambda.\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3580: $$

3581: This enables us to obtain

3582: $$\lceil \gamma (atom(\Re ))\rceil \wedge \lbrack L(\alpha

3583: _{uq}^{X-\{q\}})L((\alpha _{qq}^{X-\{q\}})^{\ast })](x)\ \ \ \ \ \

3584: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3585: \ \ \ \ \ \ \ \ \ \ \ \ \ \ $$

3586: $$=\lceil \gamma

3587: (atom(\Re ))\rceil \wedge \lceil \gamma (atom(\Re ))\rceil \wedge

3588: \vee \{L(\alpha _{uq}^{X-\{q\}})(x_{1})\wedge L((\alpha

3589: _{qq}^{X-\{q\}})^{\ast })(x_{2}):x=x_{1}x_{2}\}\ \ \ $$

3590: $$\leq \vee \{\lceil \gamma (atom(\Re ))\rceil \wedge

3591: L(\alpha _{uq}^{X-\{q\}})(x_{1})\wedge L((\alpha

3592: _{qq}^{X-\{q\}})^{\ast })(x_{2}):x=x_{1}x_{2}\}\ \ \ \ \ \ \ \ \ \

3593: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $$

3594: $$=\vee \{\lceil \gamma

3595: (atom(\Re ))\rceil \wedge [\lceil \gamma (atom(\Re ))\rceil \wedge

3596: L(\alpha _{uq}^{X-\{q\}})(x_{1})]\wedge\ \ \ \ \ \ \ \ \ \ \ \ \ \

3597: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3598: \ \ $$

3599: $$[\lceil \gamma (atom(\Re ))\rceil \wedge

3600: L((\alpha _{qq}^{X-\{q\}})^{\ast })(x_{2})]:x=x_{1}x_{2}\}$$

3601: $$\leq

3602: \vee \{\lceil \gamma (atom(\Re ))\rceil \wedge [ \vee \{\lceil

3603: path_{\Re }(c_{1})\rceil :c_{1}\in T(Q,\Sigma

3604: ),b(c_{1})=u,e(c_{1})=q,\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3605: \ \ \ \ \ \ $$

3606: $$M(c_{1})\subseteq X-\{q\},lb(c_{1})=x_{1}\}]

3607: \wedge \lbrack \vee \{\lceil path_{\Re }(c_{2})\rceil :c_{2}\in

3608: T(Q,\Sigma ),b(c_{2})=$$ $$e(c_{2})=q,M(c_{2})\subseteq

3609: X,lb(c_{2})=x_{2}\}]:x=x_{1}x_{2}\}$$

3610: $$\leq \vee \{\lceil path_{\Re

3611: }(c_{1})\rceil \wedge \lceil path_{\Re }(c_{2})\rceil

3612: :c_{1},c_{2}\in T(Q,\Sigma

3613: ),b(c_{1})=u,e(c_{1})=b(c_{2})=e(c_{2})=q,$$

3614: $$M(c_{1})\subseteq X-\{q\}, M(c_{2})\subseteq

3615: X,x=lb(c_{1})lb(c_{2})\}.$$ Furthermore, we can derive in a

3616: similar way that

3617: $$\lceil \gamma (atom(\Re

3618: ))\rceil \wedge ([L(\alpha _{uq}^{X-\{q\}})L((\alpha

3619: _{qq}^{X-\{q\}})^{\ast })]L(\alpha _{qv}^{X-\{q\}}))(s)\ \ \ \ \ \

3620: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $$

3621: $$\leq \vee \{\lceil path_{\Re }(c_{1})\rceil \wedge \lceil path_{\Re }(c_{2})\rceil \wedge \lceil path_{\Re

3622: }(c_{3})\rceil :c_{1},c_{2},c_{3}\in T(Q,\Sigma ),b(c_{1})=u,\ \ \

3623: \ \ \ \ \ \ \ \ \ \ \ \ \ $$

3624: $$e(c_{1})=b(c_{2})=e(c_{2})=b(c_{3})=q,e(c_{3})=v,s=lb(c_{1})lb(c_{2})lb(c_{3})\}

3625: $$

3626: $$=\vee \{\lceil path_{\Re }(c)\rceil :c\in T(Q,\Sigma ),b(c)=u,e(c)=v,q\in

3627: M(c),s=lb(c)\}.\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $$

3628: Consequently, it holds that

3629: $$\lceil \gamma (atom(\Re ))\rceil \wedge L(\alpha _{uv}^{X})(s)=\lceil \gamma (atom(\Re

3630: ))\rceil \wedge \{L(\alpha _{uv}^{X-\{q\}})(s)\vee\ \ \ \ \ \ \ \

3631: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $$

3632: $$\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ ([L(\alpha _{uq}^{X-\{q\}})L((\alpha _{qq}^{X-\{q\}})^{\ast

3633: })]L(\alpha _{qv}^{X-\{q\}}))(s)\}$$

3634: $$\leq [\lceil \gamma (atom(\Re ))\rceil \wedge L(\alpha

3635: _{uv}^{X-\{q\}})(s)]\vee \{\lceil \gamma (atom(\Re ))\rceil \wedge

3636: ([L(\alpha _{uq}^{X-\{q\}})L((\alpha _{qq}^{X-\{q\}})^{\ast

3637: })]L(\alpha _{qv}^{X-\{q\}}))(s)\}$$

3638: $$\leq\ {\rm the\ right-hand\ side\ of\ (b)}.\ \ \ \ \ \

3639: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3640: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3641: $$

3642: 

3643: After proving (a), we can assert that

3644: $$\lceil s\in L(k(\Re ))\rceil =\vee

3645: _{u,v\in Q}[I(u)\wedge T(v)\wedge L(\alpha _{uv}^{Q})(s)]\ \ \ \ \

3646: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3647: \ \ \ \ \ $$

3648: $$\geq \vee _{u,v\in Q}[(I(u)\wedge T(v))\wedge \vee \{\lceil path_{\Re

3649: }(c)\rceil :c\in T(Q,\Sigma ),b(c)=u,e(c)=v,lb(c)=s\}]$$

3650: $$\geq \vee _{u,v\in Q}\vee \{I(u)\wedge T(v)\wedge \lceil path_{\Re }(c)\rceil :c\in

3651: T(Q,\Sigma ),b(c)=u,e(c)=v,lb(c)=s\}\ \ $$

3652: $$=\lceil rec_{\Re }(s)\rceil .\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3653: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3654: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $$

3655: 

3656: By using (b) and Lemmas 2.5 and 2.6, we have

3657: $$\lceil \gamma (atom(\Re))\rceil \wedge \lceil s\in L(k(\Re ))\rceil =\lceil \gamma (atom(\Re))\rceil \wedge \vee

3658: _{u,v\in Q}[I(u)\wedge T(v)\wedge L(\alpha _{uv}^{Q})(s)]$$

3659: $$\leq \vee

3660: _{u,v\in Q}[I(u)\wedge T(v)\wedge \lceil \gamma (atom(\Re))\rceil

3661: \wedge L(\alpha _{uv}^{Q})(s)]\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3662: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $$

3663: $$\leq \vee _{u,v\in Q}[(I(u)\wedge T(v))\wedge \lceil \gamma (atom(\Re))\rceil\wedge \vee \{\lceil path_{\Re

3664: }(c)\rceil :c\in T(Q,\Sigma ),\ \ \ \ \ \ \ \ \ \ \ \ \ \ $$

3665: $$b(c)=u,e(c)=v,lb(c)=s\}]$$

3666: $$\leq \vee _{u,v\in Q}\vee \{I(u)\wedge T(v)\wedge \lceil path_{\Re }(c)\rceil :c\in

3667: T(Q,\Sigma ),b(c)=u,e(c)=v,lb(c)=s\}$$

3668: $$=\lceil rec_{\Re }(s)\rceil .\ \ \ \ \ \ \

3669: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3670: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

3671: \ \ \ \ \ \ \ \ \ \ \ \ \ $$

3672: 

3673: Thus, (1) and (2) are proved, and the part that (i) implies (ii)

3674: of (3) is a simple corollary of (2). We now turn to prove that

3675: (ii) implies (i). For any $a,b,c\in L,$ we consider the $\ell

3676: -$valued automaton

3677: $$\Re =<\{u,v\},\delta ,u_{a},\{u,v\}>,$$ where $\delta (u,\sigma

3678: ,u)=b,$ $\delta (u,\sigma ,v)=c,$ and $\delta $ takes value $0$

3679: for other cases (see Figure 9). Then

3680: $$\lceil rec_{\Re }(\sigma )\rceil =\vee \{I(q_{0})\wedge

3681: T(q_{1})\wedge \delta (q_{0},\sigma ,q_{1}):q_{0},q_{1}\in Q\}$$

3682: $$=(a\wedge b)\vee (a\wedge c).$$

3683: 

3684: \begin{figure}\centering

3685: \includegraphics{fig_9.eps}\caption{Automaton g} \label{fig 9}

3686: \end{figure}

3687: 

3688: On the other hand, we have

3689: $$\left\{

3690: \begin{array}{c}

3691: \alpha _{uu}^{\phi }=\varepsilon +b\sigma , \\

3692: \alpha _{uv}^{\phi }=c\sigma , \\

3693: \alpha _{vv}^{\phi }=\varepsilon , \\

3694: \alpha _{vu}^{\phi }=\phi .

3695: \end{array}

3696: \right. $$ Therefore,

3697: $$\alpha _{uu}^{\{v\}}=\alpha

3698: _{uu}^{\phi }+[\alpha _{uv}^{\phi }(\alpha _{vv}^{\phi })^{\ast

3699: }]\alpha _{vu}^{\phi }$$

3700: $$=(\varepsilon +b\sigma )+[c\sigma

3701: (\varepsilon )^{\ast }]\phi $$

3702: $$=\varepsilon +b\sigma ,$$

3703: $$\alpha _{uv}^{\{v\}}=\alpha _{uv}^{\phi }+[\alpha _{uv}^{\phi

3704: }(\alpha _{vv}^{\phi })^{\ast }]\alpha _{vv}^{\phi }$$

3705: $$=c\sigma +[c\sigma (\varepsilon )^{\ast }]\varepsilon $$

3706: $$=c\sigma ,$$

3707: and

3708: $$\alpha _{uv}^{\{u,v\}}=\alpha _{uu}^{\{v\}}+[\alpha _{uu

3709: }^{\{v\}}(\alpha _{u}^{\{v\}})^{\ast }]\alpha _{uv}^{\{v\}}$$

3710: $$=\varepsilon +b\sigma +[(\varepsilon +b\sigma )(\varepsilon

3711: +b\sigma )^{\ast }](c\sigma ).$$

3712: 

3713: From the assumption (ii) we know that

3714: $$(a\wedge b)\vee (a\wedge

3715: c)=\lceil rec_{\Re }(\sigma )\rceil $$

3716: $$=L(k(\Re ))(\sigma )$$

3717: $$=[L(a\alpha _{u}^{\{u,v\}})\cup L(a\alpha

3718: _{uv}^{\{u,v\}})](\sigma )$$

3719: $$\geq L(a\alpha _{u}^{\{u,v\}})(\sigma )$$

3720: $$=a\wedge L(\alpha _{u}^{\{u,v\}})(\sigma )$$

3721: $$=a\wedge L(\varepsilon +b\sigma +[(\varepsilon +b\sigma

3722: )(\varepsilon +b\sigma )^{\ast }](c\sigma ))(\sigma )$$

3723: $$\geq

3724: a\wedge (b\vee c).$$ This completes the proof.$\heartsuit$

3725: 

3726: \smallskip\

3727: 

3728: \textbf{Corollary 7.2.} Let $\ell =<L,\leq ,\wedge ,\vee ,\bot

3729: ,0,1>$ be an orthomodular lattice, and let

3730: $\rightarrow=\rightarrow_3$. Then for any $A\in L^{\Sigma^{*}}$,

3731: $$\stackrel{\ell}{\models} CReg_{\Sigma}(A)\rightarrow (\exists\ {\rm regular\ expression}\ \alpha)(A\equiv L(\alpha)).$$

3732: 

3733: \smallskip\

3734: 

3735: \textbf{Proof.} It can be derived from Theorem 7.1 in a way

3736: similar to the proof of Corollary 4.2.$\heartsuit$

3737: 

3738: \smallskip\

3739: 

3740: We now turn to consider homomorphisms of $\ell-$valued regular

3741: expressions. Let $\Sigma$ and $\Gamma$ be two alphabet, and let

3742: $h:\Sigma \rightarrow \Gamma ^{\ast }$ be a mapping. Then it can

3743: be uniquely extended to a mapping, denoted still by $h,$ from

3744: $\ell -$valued regular expressions over $\Sigma $ into $\ell

3745: -$valued regular expressions over $\Gamma .$ For any $\ell

3746: -$valued regular expression $\alpha $ over $ \Sigma ,$ $h(\alpha

3747: )$ is defined to be the $\ell -$valued regular expression over

3748: $\Gamma $ obtained by replacing each letter $\sigma \in \Sigma $

3749: appearing in $\alpha $ with the string $h(\sigma )\in \Gamma

3750: ^{\ast }.$ Formally, $h(\alpha )$ is defined by induction on the

3751: length of $\alpha : $

3752: $$h(\varepsilon )=\varepsilon ,$$

3753: $$h(\phi )=\phi ,$$

3754: $$h(\sigma )\ {\rm is\ already\ given\ for\ each}\ \sigma \in \Sigma

3755: ,$$

3756: $$h(\lambda \alpha )=\lambda h(\alpha ),$$

3757: $$h(\alpha _{1}+\alpha _{2})=h(\alpha _{1})+h(\alpha _{2}),$$

3758: $$h(\alpha _{1}\cdot\alpha _{2})=h(\alpha _{1})\cdot h(\alpha _{2}),$$

3759: $$h(\alpha ^{\ast })=(h(\alpha ))^{\ast }.$$

3760: 

3761: \smallskip\

3762: 

3763: For each $\ell-$valued regular expression $\alpha$ over $\Sigma$,

3764: we write $\Lambda (\alpha )$ for the set of scalar values $\lambda

3765: \in L$ occurring in $\alpha .$ Indeed, $\Lambda (\alpha )$ may be

3766: formally defined by induction on the length of $\alpha $ as

3767: follows:

3768: $$\Lambda (\varepsilon )=\Lambda (\phi )=\Lambda (\sigma )=\phi\ {\rm for\ every}\

3769: \sigma \in \Sigma ,$$

3770: $$\Lambda (\lambda \alpha )=\{\lambda \}\cup

3771: \Lambda (\alpha ),$$

3772: $$\Lambda (\alpha _{1}+\alpha _{2})=\Lambda (\alpha _{1}\cdot \alpha

3773: _{2})=\Lambda (\alpha _{1})\cup \Lambda (\alpha _{2}),$$

3774: $$\Lambda

3775: (\alpha ^{\ast })=\Lambda (\alpha ).$$ It is easy to see that

3776: $\Lambda (\alpha )$ is a finite subset of $L.$ Moreover, we write

3777: $$\Delta(\alpha)=\{\mathbf{a}:a\in \Lambda (\alpha)\}$$ for the

3778: set of (constant) propositions in our logical language

3779: corresponding to the elements in $\Lambda (\alpha)$.

3780: 

3781: The following two lemmas are very useful when we are dealing with

3782: orthomodular lattice-valued expressions, they evaluate the range

3783: of language generated by an orthomodular lattice-valued regular

3784: expression. In particular, it will be shown in Lemma 7.4 that this

3785: range is a finite set whenever the lattice $\ell$ of truth values

3786: is a Boolean algebra.

3787: 

3788: \smallskip\

3789: 

3790: \textbf{Lemma 7.3.} Let $\ell =<L,\leq ,\wedge ,\vee ,\bot ,0,1>$

3791: be an orthomodular lattice. Then for any $\ell -$valued regular

3792: expression $\alpha ,$ $ \{L(\alpha )(s):s\in \Sigma ^{\ast

3793: }\}\subseteq [\Lambda (\alpha )],$ where $[A]$ denotes the

3794: subalgebra of $\ell$ generated by $A$ for any $A\subseteq L.$

3795: 

3796: \smallskip\

3797: 

3798: \textbf{Proof.} We use an induction argument on the length of

3799: $\alpha .$ For simplicity, we only consider the following two

3800: cases, and the other cases are easy or similar.

3801: 

3802: (1) From the induction hypothesis we know that

3803: $$L(\lambda .\alpha

3804: )(s)=\lambda \wedge L(\alpha )(s)\in \overline{\{\lambda \}\cup

3805: \Lambda (\alpha )}=\overline{\Lambda (\lambda .\alpha )}$$ for

3806: each $s\in \Sigma ^{\ast }.$

3807: 

3808: (2) Let $s\in \Sigma ^{\ast }.$ For any $s_{1},...,s_{n}\in \Sigma

3809: ^{\ast }$ with $s_{1}...s_{n}=s,$ we suppose that

3810: $s_{i_{1}},...,s_{i_{m}}\neq \varepsilon $ and $s_{i}=\varepsilon

3811: $ for every $i\in \{1,...,n\}-\{i_{1},...,i_{m}\}.$ Then

3812: $s_{i_{1}}...s_{i_{m}}=s$ and

3813: $$L(\alpha )(s_{1})\wedge ...\wedge

3814: L(\alpha )(s_{n})=\left\{

3815: \begin{array}{c}

3816: L(\alpha )(s_{i_{1}})\wedge ...\wedge L(\alpha )(s_{i_{m}})\ {\rm

3817: if }\ m=n,

3818: \\

3819: L(\alpha )(s_{i_{1}})\wedge ...\wedge L(\alpha )(s_{i_{m}})\wedge

3820: L(\alpha )(\varepsilon )\ {\rm if }\ m<n.

3821: \end{array}

3822: \right. $$ Furthermore, we note that $$\{(s_{1},...,s_{n}):n\geq

3823: 0,s_{1},...,s_{n}\in \Sigma ^{\ast }-\{\varepsilon \}\ {\rm and}\

3824: s_{1}...s_{n}=s\}$$ is finite. Therefore, $$\{L(\alpha

3825: )(s_{1})\wedge ...\wedge L(\alpha )(s_{n}):s_{1}...s_{n}=s\}$$ is

3826: also finite, and with the induction hypothesis we have

3827: $$L(\alpha ^{\ast })(s)=\vee \{L(\alpha )(s_{1})\wedge ...\wedge

3828: L(\alpha )(s_{n}):s_{1}...s_{n}=s\}\in \overline{\Lambda (\alpha

3829: )}.\heartsuit$$

3830: 

3831: \smallskip\

3832: 

3833: \textbf{Lemma 7.4.} If $\ell =<L,\leq ,\wedge ,\vee ,\bot ,0,1>$

3834: is a Boolean algebra, then for any $\ell -$valued regular

3835: expression $\alpha ,$ $ \{L(\alpha )(s):s\in \Sigma ^{\ast }\}$ is

3836: a finite set.

3837: 

3838: \smallskip\

3839: 

3840: \textbf{Proof. }From Lemma 7.3 and the distributivity of $\wedge $

3841: over $\vee $ we know that for any $s\in \Sigma ^{\ast },$ there

3842: are $\lambda _{ij_{i}}\in \Lambda (\alpha )$

3843: $(i=1,...,m;j_{i}=1,...,n_{i})$ such that

3844: $$L(\alpha )(s)=\vee

3845: _{i=1}^{m}(\wedge _{j_{i}=1}^{n_{i}}\lambda _{ij_{i}}).$$ Since

3846: $\Lambda (\alpha )$ is finite, both $$\Lambda (\alpha )^{(\wedge

3847: )}=\{\lambda _{1}\wedge ...\wedge \lambda _{n}:n\geq 0,\lambda

3848: _{1},...,\lambda \in \Lambda (\alpha )\}$$ and $$\Lambda (\alpha

3849: )^{(\wedge )(\vee )}=\{\vee M:M\subseteq \Lambda (\alpha

3850: )^{(\wedge )}\}$$ are also finite. Therefore, $$\Lambda (\alpha

3851: )^{(\wedge )(\vee )}\supseteq \{L(\alpha )(s):s\in \Sigma ^{\ast

3852: }\}$$ is a finite set.$\heartsuit$

3853: 

3854: \smallskip\

3855: 

3856: The following proposition shows that a homomorphism preserves the

3857: language generated by an orthomodular lattice-valued regular

3858: expression under the condition that all elements in the range of

3859: the expression under consideration are commutative.

3860: 

3861: \smallskip\

3862: 

3863: \textbf{Proposition 7.5.} Let $\ell =<L,\leq ,\wedge ,\vee ,\bot

3864: ,0,1>$ be an orthomodular lattice and $\rightarrow$ fulfil the

3865: Birkhoff-von Neumann requirement, and let $\Sigma$ and $\Gamma$ be

3866: two alphabets.

3867: 

3868: (1) For any mapping $h:\Sigma\rightarrow \Gamma ^{\ast }$, and for

3869: any $\ell -$valued regular expression $\alpha $ over $\Sigma ,$

3870: $$\stackrel{\ell}{\models} h(L(\alpha ))\subseteq L(h(\alpha )).$$

3871: 

3872: (2) For any mapping $h:\Sigma\rightarrow \Gamma ^{\ast }$, for any

3873: $\ell -$valued regular expression $\alpha $ over $\Sigma ,$ and

3874: for any $t\in \Gamma^{*}$,

3875: $$\stackrel{\ell}{\models}\gamma(\Delta(\alpha))\wedge t\in L(h(\alpha))\rightarrow

3876:  t\in h(L(\alpha)),$$ and if $\rightarrow=\rightarrow_3$ then

3877: $$\stackrel{\ell}{\models}\gamma(\Delta(\alpha))\rightarrow

3878: L(h(\alpha))\equiv h(L(\alpha)).$$

3879: 

3880: (3) The following two statements are equivalent:

3881: 

3882: \ \ \ \ \ \ (i) $\ell $ is a Boolean algebra.

3883: 

3884: \ \ \ \ \ \ (ii) for any mapping $h:\Sigma\rightarrow \Gamma

3885: ^{\ast }$, and for any $\ell-$valued regular expression $ \alpha $

3886: over $\Sigma ,$

3887: $$\stackrel{\ell}{\models} h(L(\alpha ))\equiv L(h(\alpha )).$$

3888: 

3889: \smallskip\

3890: 

3891: \textbf{Proof.} We only prove (2) and (3), and (1) can be observed

3892: from the proof of (2). The part that (i) implies (ii) of (3) may

3893: be derived from (2); and it can also be proved directly by using

3894: Lemma 7.4.

3895: 

3896: Our first aim is to prove that $$\lceil

3897: \gamma(\Delta(\alpha))\rceil\wedge L(h(\alpha ))(t)=h(L(\alpha

3898: ))(t)$$ for any $t\in \Gamma ^{\ast }$ and for any $\ell -$valued

3899: regular expression $\alpha $ over $ \Sigma .$ We proceed by

3900: induction on the length of $\alpha .$

3901: 

3902: (a) It is obvious for the case of $\alpha =\varepsilon $ or $\phi

3903: ,$ or $ \alpha \in \Sigma .$

3904: 

3905: (b) With the definitions of $h(\cdot )$ and $L(\cdot )$ and the

3906: induction hypothesis we derive that

3907: $$L(h(\lambda .\alpha ))(t)=L(\lambda .h(\alpha ))(t)$$

3908: $$=\lambda \wedge L(h(\alpha ))(t)$$

3909: $$=\lambda \wedge h(L(\alpha ))(t)$$

3910: $$=\lambda \wedge \vee \{L(\alpha )(s):s\in \Sigma ^{\ast }\ {\rm

3911: and}\ h(s)=t\}.$$ Then from Lemmas 2.5, 2.6 and 7.3, it follows

3912: that

3913: $$\lceil \gamma(\Delta(\alpha))\rceil\wedge L(h(\lambda

3914: .\alpha ))(t)\leq \vee \{\lambda \wedge L(\alpha )(s):s\in \Sigma

3915: ^{\ast }\ {\rm and}\ h(s)=t\}$$

3916: $$=\vee \{L(\lambda .\alpha )(s):s\in

3917: \Sigma ^{\ast }\ {\rm and}\ h(s)=t\}$$

3918: $$=h(L(\lambda .\alpha

3919: ))(t).$$

3920: 

3921: (c) It is easy to observe that $h(A\cup B)=h(A)\cup h(B)$ for all

3922: $A,B\in L^{\Sigma ^{\ast }}.$ This together with the induction

3923: hypothesis as well as Lemmas 2.5 and 2.6 yields

3924: $$\lceil \gamma(\Delta(\alpha_1 + \alpha_2))\rceil\wedge L(h(\alpha _{1}+\alpha

3925: _{2}))(t) =\lceil \gamma(\Delta(\alpha_1 + \alpha_2))\rceil\wedge

3926: L(h(\alpha _{1})+h(\alpha _{2}))(t)$$

3927: $$=\lceil \gamma(\Delta(\alpha_1 + \alpha_2))\rceil\wedge\lceil \gamma(\Delta(\alpha_1 + \alpha_2))\rceil\wedge

3928: [L(h(\alpha _{1}))(t)\vee L(h(\alpha _{2}))(t)]$$ $$\leq [\lceil

3929: \gamma(\Delta(\alpha_1 + \alpha_2))\rceil\wedge

3930: L(h(\alpha_1))(t)]\wedge [\lceil \gamma(\Delta(\alpha_1 +

3931: \alpha_2))\rceil\wedge L(h(\alpha_2))(t)]$$ $$\leq [\lceil

3932: \gamma(\Delta(\alpha_1))\rceil\wedge L(h(\alpha_1))(t)]\wedge

3933: [\lceil \gamma(\Delta(\alpha_2))\rceil\wedge L(h(\alpha_2))(t)]$$

3934: $$h(L(\alpha _{1}))(t)\vee h(L(\alpha _{2}))(t)$$

3935: $$=h(L(\alpha _{1})\cup L(\alpha _{2}))(t)$$

3936: $$=h(L(\alpha _{1}+\alpha _{2}))(t).$$

3937: 

3938: (d) For any $t\in \Gamma ^{\ast },$ Lemmas 2.5, 2.6 and 7.3 enable

3939: us to assert that $$\lceil \gamma(\Delta(\alpha_1\cdot

3940: \alpha_2))\rceil\wedge L(h(\alpha_1\cdot \alpha_2))(t)=\lceil

3941: \gamma(\Delta(\alpha_1\cdot \alpha_2))\rceil\wedge

3942: L(h(\alpha_1)\cdot h(\alpha_2))(t)$$ $$=\lceil

3943: \gamma(\Delta(\alpha_1\cdot \alpha_2))\rceil\wedge

3944: L(h(\alpha_1))L(h(\alpha_2))(t)$$

3945: $$=\lceil \gamma(\Delta(\alpha_1\cdot

3946: \alpha_2))\rceil\wedge \vee\{L(h(\alpha_1))(t_1)\wedge

3947: L(h(\alpha_2))(t_2):t_1t_2=t\}$$

3948: $$\leq \vee\{\lceil \gamma(\Delta(\alpha_1\cdot

3949: \alpha_2))\rceil\wedge L(h(\alpha_1))(t_1)\wedge

3950: L(h(\alpha_2))(t_2):t_1t_2=t\}$$

3951: $$=\vee\{\lceil \gamma(\Delta(\alpha_1\cdot

3952: \alpha_2))\rceil\wedge (\lceil

3953: \gamma(\Delta(\alpha_1))\rceil\wedge L(h(\alpha_1))(t_1))\wedge

3954: (\lceil \gamma(\Delta(\alpha_2))\rceil\wedge

3955: L(h(\alpha_2))(t_2)):t_1t_2=t\}$$

3956: $$\leq \vee\{\lceil \gamma(\Delta(\alpha_1\cdot

3957: \alpha_2))\rceil\wedge h(L(\alpha_1))(t_1)\wedge

3958: h(L(\alpha_2))(t_2):t_1t_2=t\}.$$ Furthermore, by using Lemmas

3959: 2.5, 2.6 and 7.3 again we obtain $$\lceil

3960: \gamma(\Delta(\alpha_1\cdot \alpha_2))\rceil\wedge

3961: h(L(\alpha_1))(t_1)\wedge h(L(\alpha_2))(t_2)=\lceil

3962: \gamma(\Delta(\alpha_1\cdot \alpha_2))\rceil\wedge

3963: (\vee\{L(\alpha_1)(s_1):h(s_1)=t_1\})$$

3964: $$\wedge (\vee\{L(\alpha_2)(s_2):h(s_2)=t_2\})$$

3965: $$\leq \vee\{L(\alpha_1)(s_1)\wedge L(\alpha_2)(s_2):h(s_1)=t_1\ {\rm and}\

3966: h(s_2)=t_2\}.$$ Therefore, it follows that

3967: $$\lceil \gamma(\Delta(\alpha_1\cdot

3968: \alpha_2))\rceil\wedge L(h(\alpha_1\cdot \alpha_2))(t)\leq

3969: \vee\{L(\alpha_1)(s_1)\wedge$$ $$L(\alpha_2)(s_2):h(s_1)=t_1,

3970: h(s_2)=t_2\ {\rm and}\ t_1t_2=t\}$$

3971: $$=\vee\{L(\alpha_1)(s_1)\wedge L(\alpha_2)(s_2):h(s_1s_2)=t\}$$

3972: $$=h(L(\alpha_1)L(\alpha_2))(t)$$ $$=h(L(\alpha_1\alpha_2))(t).$$

3973: 

3974: 

3975: (e) For every $t\in \Gamma ^{\ast },$ Lemmas 2.5, 2.6 and 7.3

3976: guarantee that $$\lceil \gamma (\Delta (\alpha ^{\ast }))\rceil

3977: \wedge L(h(\alpha ^{\ast }))(t)=\lceil \gamma (\Delta (\alpha

3978: ^{\ast }))\rceil \wedge L((h(\alpha ))^{\ast })(t)$$

3979: $$=\lceil \gamma (\Delta (\alpha ^{\ast }))\rceil \wedge

3980: (L(h(\alpha )))^{\ast }(t)$$

3981: $$=\lceil \gamma (\Delta (\alpha ^{\ast }))\rceil \wedge \vee

3982: \{\wedge _{i=1}^{n}L(h(\alpha ))(t_{i}):n\geq 0,t_{1},...,t_{n}\in

3983: \Gamma ^{\ast },t_{1}...t_{n}=t\}$$

3984: $$\leq \vee \{\lceil \gamma (\Delta (\alpha ^{\ast }))\rceil \wedge

3985: \wedge _{i=1}^{n}L(h(\alpha ))(t_{i}):n\geq 0,t_{1},...,t_{n}\in

3986: \Gamma ^{\ast },t_{1}...t_{n}=t\}$$

3987: $$=\vee \{\lceil \gamma (\Delta (\alpha ))\rceil \wedge \wedge

3988: _{i=1}^{n}(\lceil \gamma (\Delta (\alpha ))\rceil \wedge

3989: L(h(\alpha ))(t_{i})):n\geq 0,t_{1},...,t_{n}\in \Gamma ^{\ast

3990: },t_{1}...t_{n}=t\}$$

3991: $$\leq \vee \{\lceil \gamma (\Delta (\alpha ))\rceil \wedge \wedge

3992: _{i=1}^{n}h(L(\alpha ))(t_{i}):n\geq 0,t_{1},...,t_{n}\in \Gamma

3993: ^{\ast },t_{1}...t_{n}=t\}.$$ On the other hand, we have

3994: $$\lceil \gamma (\Delta (\alpha ))\rceil \wedge \wedge

3995: _{i=1}^{n}h(L(\alpha ))(t_{i})=\lceil \gamma (\Delta (\alpha

3996: ))\rceil \wedge \wedge _{i=1}^{n}(\vee \{L(\alpha

3997: )(s_{i}):h(s_{i})=t_{i}\})$$

3998: $$\leq \vee \{\wedge _{i=1}^{n}L(\alpha )(s_{i}):h(s_{i})=t_{i}\

3999: (i=1,...,n)\}.$$ This further yields

4000: $$\lceil \gamma (\Delta (\alpha ^{\ast }))\rceil \wedge L(h(\alpha

4001: ^{\ast }))(t)\leq \vee \{\wedge _{i=1}^{n}L(\alpha )(s_{i}):n\geq

4002: 0,h(s_{i})=t_{i}\ (i=1,...,n)\ {\rm and}\ t=t_{1}...t_{n}\}$$

4003: $$=\vee \{\wedge _{i=1}^{n}L(\alpha )(s_{i}):n\geq

4004: 0,h(s_{1}...s_{n})=t\}$$

4005: $$=\vee \{L(\alpha )^{\ast }(s):h(s)=t\}$$

4006: $$=h((L(\alpha ))^{\ast })(t)$$

4007: $$=h(L(\alpha ^{\ast }))(t).$$

4008: 

4009: What remains is to prove that (ii) implies (i) in (3). This needs

4010: indeed to show that the distributivity of $\wedge$ over $\vee$ is

4011: derivable from the statement (ii). Suppose that $a,b,c\in L.$ We

4012: choose an symbol $\sigma \in \Sigma $ and an symbol $\gamma \in

4013: \Gamma ,$ and define $h(\sigma )=\varepsilon $ and $h(\sigma

4014: ^{\prime })=\gamma $ for every $\sigma ^{\prime }\in \Sigma

4015: -\{\sigma \}.$ We further set $\alpha _{1}=a.\sigma $ and $\alpha

4016: _{2}=b.\varepsilon +c.\sigma .$ Then

4017: $$L(\alpha _{1}.\alpha

4018: _{2})(\sigma )=\left\{

4019: \begin{array}{c}

4020: a\wedge b\ {\rm if }\ n=1, \\

4021: a\wedge c\ {\rm if }\ n=2, \\

4022: 0\ {\rm otherwise,}

4023: \end{array}

4024: \right. $$ and

4025: $$h(L(\alpha _{1}.\alpha _{2}))(\varepsilon )=\vee

4026: _{n=0}^{\infty }L(\alpha _{1}.\alpha _{2})(\sigma ^{n})$$

4027: $$=(a\wedge b)\vee (a\wedge c).$$

4028: On the other hand, we have

4029: $$L(h(\alpha _{1}.\alpha

4030: _{2}))(\varepsilon )=L((a.\varepsilon ).(b.\varepsilon

4031: +c.\varepsilon ))(\varepsilon )$$

4032: $$=L(a.\varepsilon )(\varepsilon

4033: )\wedge L(b.\varepsilon +c.\varepsilon )(\varepsilon )$$

4034: $$=a\wedge

4035: (b\vee c).$$

4036: 

4037: From (ii) we know that $h(L(\alpha _{1}.\alpha _{2}))(\varepsilon

4038: )=L(h(\alpha _{1}.\alpha _{2}))(\varepsilon ).$ This indicates

4039: that $ (a\wedge b)\vee (a\wedge c)=a\wedge (b\vee c).\heartsuit$

4040: 

4041: \bigskip\

4042: 

4043: \textbf{8. Pumping Lemma for Orthomodular Lattice-Valued Regular

4044: Languages}

4045: 

4046: \smallskip\

4047: 

4048: The pumping lemma in the classical automata theory is a powerful

4049: tool to show that certain languages are not regular, and it

4050: exposes some limitations of finite automata. The purpose of this

4051: section is to establish a generalization of the pumping lemma for

4052: orthomodular lattice-valued languages. It is worth noting that the

4053: following orthomodular lattice-valued version of pumping lemma is

4054: given for the commutative regularity $CReg_\Sigma$. In general,

4055: the pumping lemma is not valid for the predicate $Reg_\Sigma$.

4056: 

4057: \smallskip\

4058: 

4059: \textbf{Theorem 8.1.} (The pumping lemma) Let $\ell =<L,\leq

4060: ,\wedge ,\vee ,\perp ,0,1>$ be an orthomodular lattice, and let

4061: $\rightarrow =\rightarrow _{3}.$ Then for any $A\in L^{\Sigma

4062: ^{\ast }},$ if $Range(A)$ is finite, then

4063: $$\stackrel{\ell }{\models}CReg_{\Sigma }(A)\rightarrow (\exists n\geq 0)(\forall s\in

4064: \Sigma ^{\ast })[s\in A\wedge |s|\geq n\rightarrow $$

4065: $$(\exists u,v,w\in \Sigma ^{\ast })(s=uvw\wedge |uv|\leq n\wedge

4066: |v|\geq 1\wedge (\forall i\geq 0)(uv^{i}w\in A))],$$ where for any

4067: word $t=\sigma _{1}...\sigma _{k}\in \Sigma ^{\ast },$ $|t|$

4068: stands for the length $n$ of $t.$

4069: 

4070: \smallskip\

4071: 

4072: \textbf{Proof.} For simplicity, we use $X(s,n)$ to mean the

4073: statement that $u,v,w\in \Sigma ^{\ast },\ s=uvw,\ |uv|\leq n,\

4074: {\rm and}\ |v|\geq 1$ for each $s\in \Sigma^{\ast}$ and $n\geq 0$.

4075: Then it suffices to show that

4076: $$\lceil CReg_{\Sigma }(A)\rceil \leq \vee _{n\geq 0}\wedge _{s\in

4077: \Sigma ^{\ast },|s|\geq n}(A(s)\rightarrow \vee _{X(s,n)}\wedge

4078: _{i\geq 0}A(uv^{i}w)).$$ From Definition 3.3 we know that

4079: $$\lceil CReg_{\Sigma }(A)\rceil =\vee _{\Re \in \mathbf{A}(\Sigma

4080: ,\ell )}(\lceil \gamma (atom(\Re )\cup r(A)\rceil \wedge \lceil

4081: A\equiv rec_{\Re }\rceil ).$$ Thus, we only need to prove that for

4082: any $\Re \in \mathbf{A}(\Sigma ,\ell ),$

4083: $$\lceil \gamma (atom(\Re )\cup r(A)\rceil \wedge \lceil A\equiv

4084: rec_{\Re }\rceil \leq \vee _{n\geq 0}\wedge _{s\in \Sigma ^{\ast

4085: },|s|\geq n}(A(s)\rightarrow $$ $$\vee _{X(s,n)}\wedge _{i\geq

4086: 0}A(uv^{i}w)).$$

4087: 

4088: Let $Q$ be the set of states of $\Re .$ First, it holds that for

4089: any $s\in \Sigma ^{\ast }$ with $|s|\geq |Q|,$ $$(1)\ \ \ \ \ \ \

4090: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ rec_{\Re

4091: }(s)\leq \vee _{X(s,n)}\wedge _{i\geq 0}rec_{\Re }(uv^{i}w).\ \ \

4092: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $$ In fact, suppose

4093: that $s=\sigma _{1}...\sigma _{k}.$ Then

4094: $$(2)\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ rec_{\Re }(s)=\vee _{q_{0},q_{1},...,q_{k}}[I(q_{0})\wedge

4095: T(q_{k})\wedge \wedge _{i=0}^{k-1}\delta (q_{i},\sigma

4096: _{i+1},q_{i+1})].\ \ \ \ \ \ \ \ \ \ \ \ \ \ $$ Therefore, it

4097: amounts to showing that for any $q_{0},q_{1},...,q_{k}\in Q,$

4098: $$ (3)\ \ \ \ \ \ \ \ \ \  \ \ \ I(q_{0})\wedge T(q_{k})\wedge \wedge _{i=0}^{k-1}\delta

4099: (q_{i},\sigma _{i+1},q_{i+1})\leq \vee _{X(s,n)}\wedge _{i\geq

4100: 0}rec_{\Re }(uv^{i}w).\ \ \ \ \ \ \ \ \ \ \ \ $$ Since $k=|s|\geq

4101: |Q|,$ there are two identical states among $

4102: q_{0},q_{1},...,q_{|Q|};$ in other words, there are $m\geq 0$ and

4103: $n>0$ such that $m+n\leq |Q|$ and $q_{m}=q_{m+n}.$ We set

4104: $u_{0}=\sigma _{1}...\sigma _{m},$ $v_{0}=\sigma _{m+1}...\sigma

4105: _{m+n},$ and $w_{0}=\sigma _{m+n+1}...\sigma _{k}.$ Then

4106: $s=u_{0}v_{0}w_{0},$ $|u_{0}v_{0}|=m+n\leq |Q|, $ $|v|=n\geq 1,$

4107: and $$(4) \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \vee

4108: _{X(s,n)}\wedge _{i\geq 0}rec_{\Re }(uv^{i}w)\geq \wedge _{i\geq

4109: 0}rec_{\Re }(u_{0}v_{0}^{i}w_{0}).\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

4110: \ \ \ \ \ \ \ \ \ \ \ \ $$ From the definition of $rec_{\Re },$ it

4111: is easy to see that for all $i\geq 0, $ $$(5)\ \ \ \ \ \ \ \ \ \ \

4112: \ \ rec_{\Re }(u_{0}v_{0}^{i}w_{0})\geq \lceil path_{\Re

4113: }(q_{0}\sigma _{1}q_{1}...\sigma _{m}q_{m}\ \ \ \ \ \ \ \ \ \ \ \

4114: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

4115: \ \ \  \ \ \ \ \ \ $$

4116: $$(\sigma _{m+1}q_{m+1}...\sigma _{m+n}q_{m+n})^{i}\sigma

4117: _{m+n+1}q_{m+n+1}...\sigma _{k}q_{k})\rceil $$

4118: $$=I(q_{0})\wedge T(q_{k})\wedge \wedge

4119: _{j=0}^{m+n-1}\delta (q_{j},\sigma _{j+1},q_{j+1})\wedge \wedge

4120: _{l=1}^{i-1}[\delta (q_{m+n},\sigma _{m+1},q_{m+1})\wedge $$

4121: $$\wedge _{j=m+1}^{m+n-1}\delta (q_{j},\sigma

4122: _{j+1},q_{j+1})]\wedge \wedge _{j=m+n}^{k-1}\delta (q_{j},\sigma

4123: _{j+1},q_{j+1})$$

4124: $$=I(q_{0})\wedge T(q_{k})\wedge \wedge _{j=0}^{k-1}\delta

4125: (q_{j},\sigma _{j+1},q_{j+1})$$ because $q_{m+n}=q_{m}$ and

4126: $\delta (q_{m+n},\sigma _{m+1},q_{m+1})=\delta (q_{m},\sigma

4127: _{m+1},q_{m+1}).$ Thus, by combining (4) and (5), we obtain (3)

4128: which, together with (2), yields (1).

4129: 

4130: Now we use Lemmas 2.11(1) and (3) and obtain

4131: $$\vee _{X(s,|Q|)}\wedge _{i\geq 0}rec_{\Re }(uv^{i}w)\rightarrow

4132: \vee _{X(s,|Q|)}\wedge _{i\geq 0}A(uv^{i}w)\geq \lceil \gamma

4133: (atom(\Re )\cup r(A)\rceil \wedge $$ $$\wedge _{X(s,|Q|)}(\wedge

4134: _{i\geq 0}rec_{\Re }(uv^{i}w)\rightarrow \wedge _{i\geq

4135: 0}A(uv^{i}w))$$ $$\geq \lceil \gamma (atom(\Re )\cup r(A)\rceil

4136: \wedge \wedge _{X(s,|Q|)}\wedge _{i\geq 0}(rec_{\Re

4137: }(uv^{i}w)\rightarrow A(uv^{i}w))$$

4138: $$\geq \lceil \gamma (atom(\Re )\cup r(A)\rceil \wedge \wedge

4139: _{t\in \Sigma ^{\ast }}(rec_{\Re }(t)\rightarrow A(t))$$

4140: $$=\lceil \gamma (atom(\Re )\cup r(A)\rceil \wedge \lceil rec_{\Re

4141: }\subseteq A\rceil .$$ Furthermore, from the above inequality we

4142: have

4143: $$\lceil \gamma (atom(\Re )\cup r(A)\rceil \wedge \lceil rec_{\Re

4144: }\equiv A\rceil =\lceil \gamma (atom(\Re )\cup r(A)\rceil \wedge

4145: \lceil A\subseteq rec_{\Re }\rceil \wedge \lceil rec_{\Re

4146: }\subseteq A\rceil $$

4147: $$=\lceil \gamma (atom(\Re )\cup r(A)\rceil \wedge \wedge _{s\in

4148: \Sigma ^{\ast }}(A(s)\rightarrow rec_{\Re }(s))\wedge \lceil

4149: rec_{\Re }\subseteq A\rceil $$

4150: $$\leq \lceil \gamma (atom(\Re )\cup r(A)\rceil \wedge \wedge

4151: _{s\in \Sigma ^{\ast },|s|\geq |Q|}(A(s)\rightarrow rec_{\Re

4152: }(s))\wedge \lceil rec_{\Re }\subseteq A\rceil $$

4153: $$=\wedge _{s\in \Sigma ^{\ast },|s|\geq |Q|}(\lceil \gamma

4154: (atom(\Re )\cup r(A)\rceil \wedge (A(s)\rightarrow rec_{\Re

4155: }(s))\wedge \lceil \gamma (atom(\Re )\cup r(A)\rceil \wedge \lceil

4156: rec_{\Re }\subseteq A\rceil )$$

4157: $$\leq \wedge _{s\in \Sigma ^{\ast },|s|\geq |Q|}(\lceil \gamma

4158: (atom(\Re )\cup r(A)\rceil \wedge (A(s)\rightarrow rec_{\Re

4159: }(s))$$

4160: $$\wedge (\vee _{X(s,|Q|)}\wedge _{i\geq 0}rec_{\Re

4161: }(uv^{i}w)\rightarrow \vee _{X(s,|Q|)}\wedge _{i\geq

4162: 0}A(uv^{i}w))).$$ Then from (1) it follows that

4163: $$\lceil \gamma (atom(\Re )\cup r(A)\rceil \wedge \lceil rec_{\Re

4164: }\equiv A\rceil \leq \wedge _{s\in \Sigma ^{\ast },|s|\geq

4165: |Q|}(\lceil \gamma (atom(\Re )\cup r(A)\rceil \wedge$$

4166: $$(A(s)\rightarrow \vee _{X(s,|Q|)}\wedge _{i\geq 0}rec_{\Re

4167: }(uv^{i}w))\wedge$$ $$(\vee _{X(s,|Q|)}\wedge _{i\geq 0}rec_{\Re

4168: }(uv^{i}w)\rightarrow \vee _{X(s,|Q|)}\wedge _{i\geq

4169: 0}A(uv^{i}w))).$$ By using Lemmas 2.11(1) and (3) we know that

4170: $$\lceil \gamma (atom(\Re )\cup r(A)\rceil \wedge \lceil rec_{\Re

4171: }\equiv A\rceil \leq \wedge _{s\in \Sigma ^{\ast },|s|\geq

4172: |Q|}(A(s)\rightarrow \vee _{X(s,|Q|)}\wedge _{i\geq

4173: 0}A(uv^{i}w))$$

4174: $$\leq \vee _{n\geq 0}\wedge _{s\in \Sigma ^{\ast },|s|\geq

4175: n}(A(s)\rightarrow \vee _{X(s,n)}\wedge _{i\geq 0}A(uv^{i}w)),$$

4176: and this completes the proof.$\heartsuit$

4177: 

4178: \bigskip\

4179: 

4180: \textbf{9. Conclusion}

4181: 

4182: \smallskip\

4183: 

4184: It is argued that a theory of computation based on quantum logic

4185: has to be established as a logical foundation of quantum

4186: computation. This paper is the first one of a series of papers

4187: toward such a new theory. Quantum logic is treated as an

4188: orthomodular lattice-valued logic in this paper, and the aim of

4189: the paper is to develop elementally a theory of finite automata

4190: based on such a logic by employing the semantical analysis

4191: approach. The notions of orthomodular lattice-valued finite

4192: automaton and regular language are introduced. Some modifications

4193: of orthomodular lattice-valued automaton are presented, including

4194: the orthomodular lattice-valued generalizations of deterministic

4195: and nondeterministic automata and automata with

4196: $\varepsilon-$moves, and their equivalence are thoroughly

4197: analyzed. We also examine the closure properties of orthomodular

4198: lattice-valued regular languages under various operations. The

4199: concept of orthomodular lattice-valued regular expressions is

4200: proposed, and the Kleene theorem concerning the equivalence

4201: between finite automata and regular expressions is generalized

4202: within the framework of quantum logic. Also, an orthomodular

4203: lattice-valued version of the pumping lemma is found. Furthermore,

4204: a theory of pushdown automata or Turing machines based on quantum

4205: logic will be developed in the continuations of the present paper.

4206: 

4207: In the development of automata theory based on quantum logic, some

4208: essential differences between the computation theory established

4209: by using the classical Boolean logic as the underlying logical

4210: tool and that whose meta-logic is quantum logic have been

4211: discovered. First, it is found that the proofs of some even very

4212: basic properties of automata appeal an essential application of

4213: the distributivity for the lattice of truth values of the

4214: underlying logic. This indicates that these properties holds only

4215: in Boolean logic but not in quantum logic. We believe that there

4216: are also many fundamental properties of pushdown automata and

4217: Turing machines whose universal validity requires the

4218: distributivity of meta-logic. In a sense, this observation

4219: provides us with a set of negative results in the theory of

4220: computation based on quantum logic. These negative results might

4221: hints some limitations of quantum computers. More explicitly, some

4222: methods based on certain properties of classical automata maybe

4223: have been successfully used in the implementation of classical

4224: computer systems, but they do not apply to quantum computers, or

4225: at least they are only conditionally effective for quantum

4226: computers. On the other hand, although these negative results are

4227: found in the computation theory based on quantum logic, it seems

4228: that some similar negative results exist in other mathematical

4229: theories based on nonclassical logics. This stimulates us to

4230: consider the problem of a logical revisit to mathematics. Various

4231: classical mathematical results have been established based upon

4232: classical logic, and sometimes, their universal validity can only

4233: be established by exploiting the full power of classical logic.

4234: Mathematicians usually use logic implicitly in their reasoning,

4235: and they do not seriously care which logical laws they have

4236: employed. But from a logician's point of view, it is very

4237: interesting to determine how strong a logic we need to validate a

4238: given mathematical theorem, and which logic guarantees this

4239: theorem and which does not among the large population of

4240: nonclassical logics. To be more explicit and also for a

4241: comparison, let us present a short excerpt from A. Heyting [He63,

4242: page 3]:

4243: $$$$

4244: \textit{"It may happen that for the proof of a theorem we do not

4245: need all the axioms, but only some of them. Such a theorem is true

4246: not only for models of the whole system, but also for those of the

4247: smaller system which contains only the axioms used in the proof.

4248: Thus it is important in an axiomatic theory to prove every theorem

4249: from the least possible set of axioms."}

4250: $$$$

4251: We now are in a similar situation. The difference between our case

4252: and A. Heyting's one is that we are concerned with the limitation

4253: or redundance of power of the logic underlying an axiomatic

4254: theory, whereas he considered that of axioms themselves. It seems

4255: that the semantical analysis approach provides a nice framework

4256: for solving this problem, much more suitable than a

4257: proof-theoretical approach.

4258: 

4259: As stated above, some fundamental properties of automata are not

4260: universally valid in quantum logic due to lack of distributivity.

4261: However, a certain commutativity are able to regain a local

4262: distributivity, and to give further a partial validity of these

4263: properties in the theory of automata based on quantum logic. One

4264: typical example of such properties is the equivalence of automata

4265: and their various modifications. It is well-known that one

4266: important witness for the Church-Turing thesis which asserts the

4267: Turing machine is a general model of computation is that various

4268: extensions of the Turing machine are all equivalent to itself. The

4269: fact that the equivalence between automata and their modifications

4270: depends upon the commutativity of their basic actions suggests us

4271: to guess that the equivalence between the Turing machine and some

4272: of its extensions may also need a support from a certain

4273: commutativity. In the introduction, we already gave a physical

4274: interpretation to the role of commutativity based on the

4275: Heisenberg uncertainty principle, and pointed out that an

4276: interesting connection may reside between the Heisenberg

4277: uncertainty principle and the Church-Turing thesis. If this is

4278: true, then it will give once again an evidence to the unity of the

4279: whole science and to the fact that science is not only a simple

4280: union of various subjects.

4281: 

4282: \bigskip\

4283: 

4284: \textbf{References}

4285: 

4286: \smallskip\

4287: 

4288: [Ba85] J. Barwise, in: J. Barwise and S. Feferman, eds.,

4289: \textit{Model Theoretic Logics}, Springer-Verlag, Berlin, 1985,

4290: pp. ?.

4291: 

4292: [Be80] P. A. Benioff, The computer as a physical system: a

4293: microscopic quantum mechanical Hamiltonian model of computer s as

4294: represented by Turing machines, \textit{Journal of Statistical

4295: Physics} \textbf{22}(1980)563-591.

4296: 

4297: [Ben73] C. H. Bennet, Logical reversibility of computation,

4298: \textit{IBM Journal of Research and Development}

4299: \textbf{17}(1973)525-532.

4300: 

4301: [BN36] G. Birkhoff and J. von Neumann, The logic of quantum

4302: mechanics, \textit{Annals of Mathematics},

4303: \textbf{37}(1936)823-843.

4304: 

4305: [BH00] G. Bruns and J. Harding, Algebraic aspects of orthomodular

4306: lattices, in: B. Coecke, D. Moore and A. Wilce (eds.),

4307: \textit{Current Research in Operational Quantum Logic: Algebras,

4308: Categories, Languages,} Kluwer, Dordrecht, 2000, pp. 37-65.

4309: 

4310: [CZ95] J. I. Cirac and P. Zoller, Quantum computation with cold

4311: trapped ions, \textit{Physical Review Letters}

4312: \textbf{74}(1995)4091-4094.

4313: 

4314: [CM00] J. P. Crutchfield and C. Moore, Quantum automata and

4315: quantum grammar, \textit{Theoretical Computer Science}

4316: \textbf{237}(2000)275-306.

4317: 

4318: [DC81] M. L. Dalla Chiara, Some meta-logical pathologies of

4319: quantum logic, in: E. Beltrametti and B. C. van Fraassen (eds.),

4320: \textit{Current Issues in Quantum Logics}, Plenum, New York, 1981,

4321: pp. 147-159.

4322: 

4323: [DC86] M. L. Dalla Chiara, Quantum logic, in: D. Gabbay and E.

4324: Guenthner (eds.), \textit{Handbook of Philosophical Logic, volume

4325: III: Alternatives to Classical Logic}, D. Reidel Publishing

4326: Company, Dordrecht, 1986, pp. 427-469. Also see arXiv:

4327: quant-ph/0101028 for an extended and revised version.

4328: 

4329: [De85] D. Deutsch, Quantum theory, the Church-Turing principle and

4330: the universal quantum computer, \textit{Proc. Roy. Soc. Lond}.

4331: \textbf{A400}(1985)97-117.

4332: 

4333: [De89] D. Deutsch, Quantum computational networks, \textit{Proc.

4334: Roy. Soc. Lond}. \textbf{A425}(1989)73-90.

4335: 

4336: [Di78] J. Dieudonne, The current trend of pure mathematics,

4337: \textit{Advances in Mathematics} \textbf{27}(1978)235-255.

4338: 

4339: [E74] S. Eilenberg, \textit{Automata, Languages, and Machines,

4340: volume A}, Academic Press, New York, 1974.

4341: 

4342: [Fe82] R. P. Feynman, Simulating physics with computers, \textit{

4343: International Journal of Theoretical Physics},

4344: \textbf{21}(1982)467-488.

4345: 

4346: [Fe86] R. P. Feynman, Quantum mechanical computers,

4347: \textit{Foundations of Physics,} \textbf{16}(1986)507-531.

4348: 

4349: [Fi70] P. D. Finch, Quantum logic as an implication algebra,

4350: \textit{Bulletin of Australian Mathematical Society}

4351: \textbf{2}(1970)101-106.

4352: 

4353: [Gr96] L. K. Grover, A fast quantum mechanical algorithm for

4354: database search, in: \textit{Proceedings of the 28th ACM STOC,}

4355: 1996, pp. 212-219.

4356: 

4357: [Gu00] S. Gudder, Basic properties of quantum automata,

4358: \textit{Foundations of Physics}, \textbf{30}(2000)301-319.

4359: 

4360: [Ha82] W. Hatcher, \textit{The Logical Foundations of

4361: Mathematics}, Pergamon, Oxford (1982).

4362: 

4363: [He63] A. Heyting, \textit{Axiomatic Projective Geometry,}

4364: North-Holland, Amsterdam, 1963.

4365: 

4366: [Ho89] H. Hodes, Three-valued logics - an introduction, a

4367: comparison of various logical lexica, and some philosophical

4368: remarks, \textit{Annals of Pure and Applied Logic},

4369: \textbf{43}(1989)99-145.

4370: 

4371: [Hu37] K. Husimi, Studies on the foundations of quantum mechanics

4372: I, \textit{Proceedings of the Physicomath. Soc. of Japan}

4373: \textbf{19}(1937)766-789.

4374: 

4375: [HMP75] L. Herman, E. Marsden and R. Piziak, Implication

4376: connectives in orthomodular lattices, \textit{Notre Dame J. Formal

4377: Logic} \textbf{16}(1975)305-328.

4378: 

4379: [HU79] J. E. Hopcroft and J. D. Ullman, \textit{Introduction to

4380: Automata Theory, Languages, and Computation,} Addison-Wesley,

4381: Reading, 1979.

4382: 

4383: [Ka74] G. Kalmbach, Orthomodular logic, \textit{Zeitschr. f. math.

4384: Logik und Grundlagen d. Math} \textbf{20}(1974)395-406.

4385: 

4386: [Ka83] G. Kalmbach, \textit{Orthomodular Lattices}, Academic

4387: Press, London, 1983.

4388: 

4389: [KW97] A. Kondacs and J. Watrous, On the power of quantum finite

4390: state automata, in: \textit{Proc. of the 38th Annual Symposium on

4391: Foundations of Computer Science}, pp.65-75, 1997.

4392: 

4393: [Ko97] D. C. Kozen, \textit{Automata and Computability,}

4394: Springer-Verlag, New York, 1997.

4395: 

4396: [L93] S. Lloyd, A potentially realizable quantum computer,

4397: \textit{Science} \textbf{261}(1993)1569-1571.

4398: 

4399: [Ma90] J. Malinowski, The deduction theorem for quantum logic -

4400: some negative results, \textit{Journal of Symbolic Logic}

4401: \textbf{55}(1990)615-625

4402: 

4403: [Mo65] A. Mostowski, \textit{Thirty Years of Foundational Studies:

4404: Lectures on the Development of Mathematical Logic and the Study of

4405: the Foundations of Mathematics in 1930-1964,} Acta Philosophica

4406: Fennica 17, Helsinki, 1965.

4407: 

4408: [N62] J. von Neumann, Quantum logics (strict- and

4409: probability-logics), summarized in: J. von Neumann,

4410: \textit{Collected Works, vol. IV}, Macmillan, New York(1962).

4411: 

4412: [RS00] J. P. Rawling and S. A. Selesnick, Orthologic and quantum

4413: logic: models and computational elements, \textit{Journal of the

4414: ACM} \textbf{47}(2000)721-751.

4415: 

4416: [RR91] L. Rom\'{a}n and B. Rumbos, Quantum logic revisited,

4417: \textit{ Foundations of Physics}, \textbf{21}(1991)727-734.

4418: 

4419: [RZ99] L. Rom\'{a}n and R. E. Zuazua, Quantum implication,

4420: \textit{ International Journal of Theoretical Physics,}

4421: \textbf{38}(1999)793-797.

4422: 

4423: [RT52] J. B. Rosser and A. R. Turquette, \textit{Many-Valued

4424: Logics,} North-Holland, Amsterdam, 1952.

4425: 

4426: [Sc99] K. -G. Schlesinger, Toward quantum mathematics. I. From

4427: quantum set theory to universal quantum mechanics, \textit{Journal

4428: of Mathematics Physics,} \textbf{40}(1999)1344-1358.

4429: 

4430: [Sh94] P. W. Shor, Polynomial-time algorithm for prime

4431: factorization and discrete logarithms on quantum computer, in:

4432: \textit{Proc. 35th Annual Symp. on Foundations of Computer

4433: Science, Santa Fe,} IEEE Computer Society Press, 1994.

4434: 

4435: [Sv98] K. Svozil, \textit{Quantum Logic,} Springer-Verlag, Berlin,

4436: 1998.

4437: 

4438: [T81] G. Takeuti, Quantum set theory, in: E. Beltrametti and B. C.

4439: van Fraassen (eds.), \textit{Current Issues in Quantum Logics},

4440: Plenum, New York, 1981, pp. 303-322.

4441: 

4442: [TD88] A. S. Troelstra and D. van Dalen, \textit{Constructivism in

4443: Mathematics: An Introduction,}, volume I, II, North-Holland,

4444: Amsterdam, 1988.

4445: 

4446: [VP] V. Vedral and M. B. Plenio, Basics of quantum computation,

4447: \textit{ Prog. Quant. Electron}. \textbf{22}:1(1998).

4448: 

4449: [Ya93] A. C. Yao, Quantum circuit complexity, \textit{Proc. of the

4450: 34th Ann. IEEE Symp. on Foundations of Computer Science}, pp.

4451: 352-361, 1993.

4452: 

4453: [Yi91] M. S. Ying, Deduction theorem for many-valued inference,

4454: \textit{ Zeitschr. f. math. Logik und Grundlagen d. Math}.

4455: 37:6(1991).

4456: 

4457: [Yi92a] M. S. Ying, The fundamental theorem of ultraproduct in

4458: Pavelka's logic, \textit{Zeitschr. f. math. Logik und Grundlagen

4459: d. Math.} 38:2(1992).

4460: 

4461: [Yi92b] M. S. Ying, Compactness, the Lowenheim-Skolem property and

4462: the direct product of lattices of truth values, \textit{Zeitschr.

4463: f. math. Logik und Grundlagen d. Math}. 38:4(1992).

4464: 

4465: [Yi91-93] M. S. Ying, A new approach for fuzzy topology (I), (II),

4466: (III), \textit{Fuzzy Sets and Systems,} \textbf{39}(1991)303-321;

4467: \textbf{47} (1992)221-232; \textbf{55}(1993)193-207.

4468: 

4469: [Yi93] M. S. Ying, Fuzzifying topology based on complete

4470: residuated lattice-valued logic (I), \textit{Fuzzy Sets and

4471: Systems,} \textbf{56}(1993)337-373.

4472: 

4473: [Yi94] M. S. Ying, A logic for approximate reasoning, \textit{J.

4474: Symbolic Logic} \textbf{59}(1994).

4475: 

4476: [Yi00] M. S. Ying, Automata theory based on quantum logic (I),

4477: (II), \textit{International Journal of Theoretical Physics}

4478: \textbf{39} (2000), 985-995; 2545-2557.

4479: 

4480: \end{document}

4481: