理论计算机科学中的几个问题应明生清华大学计算机科学与技术系 智能技术与系统国家重点实验室nEATCS(欧洲理论计算机科学协会)：主办杂志： Theoretical Computer Science主办会议：ICALP (International Colloquim on Automata, Languages, and Programming) “Theoretical Computer Science is mathematical and abstract in spirit, but it derives its motivations from practical and everyday computation. Its aim is to understand the nature of computation and, as a consequence of this understanding, provide more efficient methodologies.” Section A: Algorithms, automata, complexity and gamesSection B: Logic, semantics and theory of programmingSection C: Natural computing (evolutionary computing, neural network, molecular computring, quantum computing, )n美国的理论计算机科学：ACM STOC, IEEE FOCS算法与复杂性， 人工智能理论（如 Logical AI）n欧洲的理论计算机科学：形式化方法， 形式语义学， n我国在理论计算机科学（包括美式、欧 式）方面有许多非常出色的工作如何进一步发展我国的理论计算机科学 ？P. R. Halmos: “问题是数学的心脏”推而广之： “问题是一切（纯）科学的 心 脏”发展理论计算机科学，我们需要好的问 题！n波兰（华沙、里沃夫）数学学派的启示 ：有自己特色的、根本性的问题有与国际上同类工作相同的深度问题1：n可否建立基于量子逻辑（或其它非 经典逻辑）的计算理论？是否需要 建 立这样的理论？nAn axiomatization of a mathematical theory consists of a system of fundamental notions as well as a set of axioms about these notions nA mathematical theory is then the set of theorems which can be derived from the axiomsnOne needs a certain logic to provide tools for reasoning in the derivation of these theorems from the axiomsA. Heyting (1963), Axiomatic Projective Geometry, North-Holland, Amsterdam, 1963nIn elementary axiomatics logic was used in an unanalyzed formnThe studies for foundations of mathematics beginning in the early of twentieth century:It had been realized that a major part of mathematics has to exploit the full power of classical (Boolean) logic, the strongest one in the family of existing logicsnA few mathematicians took some kind of constructive position which is in more or less explicit opposition to certain forms of mathematical reasoning used by the majority of the mathematical community: L. E. J. Brouwer, H. Poincare, L.Kronecker, H. WeylnSome of them even endeavored to establish so-called constructive mathematics, the part of mathematics that could be rebuilt on constructivist principlesnThe logic employed in the development of constructive mathematics is intuitionistic logic which is weaker than classical logicn20世纪逻辑学家创造了许多不同于经典 （Boolean）逻辑与直觉主义逻辑的非经典逻 辑逻辑学家的问题: 是否可能建立基于除直觉主义逻辑之外的非经 典 逻辑的数学理论？J. B. Rosser and A. R. Turquette, Many-Valued Logics, North-Holland, Amsterdam, 1952“The fact that it is thus possible to generalize The ordinary two-valued logic so as not only to cover the case of many-valued statement calculi, but of many-valued quantification theory as well, naturally suggests the possibility of further extending our treatment of many-valued logic to cover the case of many- valued sets, equality, numbers, etc. Since we now have a general theory of many valued predicate calculi, there is little doubt about the possibility of successfully developing such extended many-valued theories. . we shall consider their careful study one of the major unsolved problems of many-valued logic.”A. Mostowski, Thirty Years of Foundational Studies Acta Philosophica Fennica, 1965nJ. Lukasiewicz (1920s) hoped that there would be some non-classical logics which can be properly used in mathematics as non-Euclidean geometry doesMost of non-classical logics invented so far have not been really used in mathematics, and intuitionistic logic seems that unique one of non-classical logics which still has an opportunity to carry out the Lukasiewiczs projectJ. Dieudonne, The current trend of pure mathematics, Advances in Mathematics 27(1978)235-255nMathematical logicians have been developing a variety of non-classical logics such as second-order logic, modal logic and many-valued logic, but these logics are completely useless for mathematicians working in other research areasn计算理论也是基于经典（Boolean）逻 辑 的数学理论（理论）计算机科学家的问题：是否需要建立基于非经典逻辑的计算理 论？量子计算的主要研究方向:1. 物理实现 2. 物理模型 3. 数学模型 4. 算法与复杂性问题: 量子计算的逻辑基础何在?G. Birkhoff and J. von Neumann, The logic of quantum mechanics, Annals of Mathematics, 37(1936)823-843“what logical structure one may hope to find in physical theories which, like quantum mechanics, do not conform to classical logic.Our main conclusion, , is that one can reasonably expect to find a calculus of propositions which is formally indistinguishable from the calculus of linear subspaces of Hilbert space with respect to set products, linear sums, and orthogonal complements and resembles the usual calculus of propositions with respect to and, or, and not.”Sasaki定理(1957): (1) The set of all closed subspaces of a Hilbert space with the inclusion relation is a complete orthomodular lattice; (2) It is a modular lattice if and only if the Hilbert space is finite-dimensional量子逻辑: （1） The theory of orthomodular lattices（2） A logic whose set of truth values is an orthomodular lattice量子逻辑已经存在！（真正的）问题： 能否建立基于量子逻辑的计算理 论？问题2：何为计算智能？什么是计算可实现的 智能？注：这里“计算智能”指的不是作