東北大学・電気通信研究所・外山研究室ではNUEセミナーを開催しています． テーマはプログラム理論や定理自動証明を中心に， 情報科学の理論的なさまざまな話題をとりあげています． 興味をおもちの方はどなたでもフラリと気楽におたちより下さい．
| 日時 | 2003年11月6日 |
|---|---|
| 講演者 | Christiane Frougny (Universite Paris 8) |
| 題目 | On-line arithmetic algorithms in real and complex base |
| 要旨 | In this talk we consider numbers represented in base beta when beta is a negative integer, a positive non-integer real number, or a complex number of the form i \sqrt{r}, where r is a positive integer. We give on-line algorithms (from most significant to least significant digit) for addition and multiplication of numbers represented in these number systems. We also show that when beta is a Pisot number (for instance the golden mean), addition is computable by an on-line finite automaton. |
| 日時 | 2003年10月21日 |
|---|---|
| 講演者 | Jacques Sakarovitch (CNRS, Paris) |
| 題目 | From finite automata to regular expressions and back: organizing the old results and exploring pathes toward the ultimate version of Kleene theorem |
| 要旨 | Kleene's theorem states the equality of two families of languages. But its proof relies indeed on algorithms that transform respectively a finite automaton into a regular expression and conversely a regular expression into a finite automaton. We shall first review the different algorithms that have been proposed so far -- and which are more or less well-known -- and explain how they are related to each other. We shall then explore the possibilities of finding algorithms that are inverses of each other. |
| 日時 | 2003年10月15日 |
|---|---|
| 講演者 | 横山哲郎 (東京大学) |
| 題目 | Deterministic Higher-order Patterns in Program Transformation |
| 要旨 | Higher-order patterns, together with higher-order matching, enable concise specification of program transformation, and have been implemented in several program transformation systems. However, higher-order matching generally generates nondeterministic matches, and the matching algorithm is so expensive that even second-order matching is NP-complete. It is orthodox to impose constraint on the form of patterns so as to obtain the desirable matches satisfying certain properties such as decidability and finiteness. In the context of unification, Miller's higher-order patterns have a single most general unifier, while unification of general patterns is nondeterministic (and even undecidable). We relax the restriction of his patterns without changing determinism in the context of matching instead of unification. As a consequence, our deterministic second-order pattern covers a wide class of useful patterns for program transformation. Our deterministic matching algorithm is as fast as the first-order matching algorithm, almost in proportion to the size of the term. |
| 日時 | 2003年5月8日 |
|---|---|
| 講演者 | Gaétan Hains (LIFO, CNRS - University of Orleans) |
| 題目 | A Synchronous Bisimulation-Based Approach for Information Flow Analysis |
| 要旨 | We define a process algebra where parallel composition is structured around synchronous communication. Its essential difference with CCS is the hypothesis that internal actions must be observable for the clock; consequently, in our formalism (strong) bisimulation will be the basis for information flow analysis, instead of equivalences based on trace or weak bisimulation. Bisimulation reduces in our formalism to equality modulo an ACUID equational theory extended with prefixes. We show that information flow analysis based on our formalism is finer than analyzes based on trace or weak bisimulation. This work applies to the mechanization of information-flow analysis for security properties. We outline ongoing work concerning unification, symbolic bisimulation and other infinite-state extensions. |
| 日時 | 2003年3月3日 |
|---|---|
| 講演者 | 竹内 泉 (東邦大学) |
| 題目 | 実効的極限作用素と計算可能性数学 |
| 要旨 |
計算可能性数学はこれまで実数に対する議論が中心であったが、近年、
一般的な数学構造に対する適用も行なわれるようになってきた。ハートリング
は一般的な代数構造の上で計算可能性を論ずる為の表現について論じている
(Hertling, MLQ, '99) が、位相については論じていない。シュレーダーは計
算可能性を論ずる為の弱極限作用素について論じている (Schroder, CCA'00)
が、収束の効率について論じていない。
計算可能性数学にとっては位相と収束の効率は極わめて重要なものである。 本研究はこのような先行研究を位相と効率に適用することを試みる。その為に、 弱極限作用素の変りに実効的極限作用素を導入する。実効的極限作用素は一様 位相を定義する。一様位相については八杉らの結果 (Yasugi, et al., CCA'00) がある。本研究はその八杉らの結果を包摂することを目標とする。 |
| 日時 | 2003年2月27日 |
|---|---|
| 講演者 | Irek Ulidowski (University of Leicester) |
| 題目 | Modelling and Verification of Concurrent Systems: an Operational Approach |
| 要旨 |
A process language framework for the modelling of concurrent
systems is presented. The framework is defined using the Ordered
Structural Operational Semantics (OSOS) approach, where traditional
Plotkin-style transition rules have orderings associated with them.
The orderings allow one to control the order of application of
transition rules when deriving transitions of process terms. The
framework is very expressive: it allows one to express easily a wide
range of functional and temporal behaviour of concurrent systems.
Also, it allows the user to define new task specific operators and
features such as, for example, random delays.
Once the user has chosen her process language (i.e. the operators, time and other features, and a suitable semantics), the process language is given an operational definition by means of OSOS transition rules and orderings on rules, as well as several restricting conditions that depend on the chosen semantics. These conditions restrict the structure of OSOS rules and the type of rule orderings that can be used. As a result, the defined process language preserves the chosen semantics. For example, a class of OSOS process languages preserves bisimulation semantics. Software tools such as Concurrency Workbench and PAC (Process Algebra Compiler) can be adapted to accept general process languages and to perform verification with respect to the chosen semantics. In the concurrency literature, there are several procedures for automatic derivation of axiom systems and term rewrite systems for general process languages. I will describe briefly two of my procedures: one for axiom systems and testing equivalence, and one for priority rewrite systems (PRSs) and bisimulation. The axiom systems and PRSs generated by these procedures can be used in conjunction with theorem proving and term rewrite tools to assist in the verification of concurrent systems. |
| 日時 | 2003年2月25日 |
|---|---|
| 講演者 | Zhenjiang Hu (University of Tokyo & JST) |
| 題目 | Optimization of Skeletal Parallel Programs |
| 要旨 |
Parallel skeletons are designed to encourage programmers to
build parallel programs from ready-made components for which efficient
implementations are known to exist, making both parallel programming
and parallelization process simpler. However, because parallel
programming relies on a set of parallel primitive skeletons for
specifying parallelism, it is often hard for programmers to choose
proper ones and to integrate them well in order to develop efficient
parallel programs to solve their problems, and it remains as a
challenge how to systematically optimize skeletal parallel programs.
In this talk, I would like to present a calculational framework supporting efficient parallel programming using skeletons, showing (1) how to design a more general and efficient parallel skeleton so that programmers can use it easier to solve their own problems; (2) how to fuse composition of skeletons in a cheap and systematic way; (3) how to flatten nested skeletons so that irregular parallelism can be exposed; and (4) how to implement an environment supporting skeletal parallel programming. Being more constructive, our method is not only helpful in design of efficient parallel programs in general but also promising in construction of parallelizing compiler. |
まで．