SLACS '97 (Oct. 29-31, 1997 at Kyushu University, Fukuoka) のプログラム

10月29日
13:00 藤田 憲悦 (九州工業大学 情報工学部)

On the Church-Rosser property of λ_{exc}^v

We introduce a call-by-value calculus based on classical propositional logic, called λ_{exc}^v. The classical system is simple and a simple exit mechanism can be implemented by the use of classical proofs. We will prove that λ_{exc}^v without so-called renaming rules has the Church-Rosser property by the well-known method of parallel reductions and the lemma of Hindley-Rosen. It is observed that for λ_ {exc}^v with renaming rules, a straightforward use of the parallel reduction method could not work to prove the Church-Rosser property.

13:30 Ver-Jan de Vries (電子技術総合研究所)

Typings for infinite lambda calculus

14:00 小林 聡 (龍谷大学 理工学部)

S4 の realizability 再考

講演者は以前に構成的な S4 様相論理に対する realizability interpretation を提案した。そこでは、様相記号が副作用と非決定性を持っ たプログラムを用いて解釈される。しかし、他の論理記号については、従来通 りの純関数的な解釈を採用していた。本講演では、通常の論理記号に対しても 純関数的でない解釈を許すような realizability interpretation について考 察する。それにはいくつかのバリエーションがあり、その1つは call by value の計算に、別の1つは call by name の計算に対応すると考えられる。

14:30 Break
14:40 長谷川 立 (東京大学大学院 数理科学研究科)

Wreath model of system F

15:10 白旗 優 (慶応大学 商学部)

A coherence space semantics for linear set theory with quantifiers

We present an extension of the coherence space semantics for linear set theory to include quantifiers. The universe of sets is obtained by combining the coherence space semantics for propositional linear logic and Scott style inverse limit construction. We then define the interpretation of terms in the universe through the well-known cardinality argument from the theory of inductive definition.

15:40
Break
15:50 龍田 真 (京都大学 理学研究科)

q-realizability for Feferman's theory

Feferman の constructive set theory T_0 に対する変数を二重化しな いq-realizability の定義とその健全性定理は未解決問題であったが、これを 解決した。T_0 + set induction axiom の体系に対して q-realizability を 定義しその健全性を証明する。講演者が今まで得ていた解は無限論理の枠組み が必要であったが、constructive set の公理化を変更することによって、普 通の論理での枠組みにおける解を得た。変数を二重化しないためこの q-realizability は構成的プログラミングに適することを示す。

16:20 尾崎 正光 (名古屋大学大学院人間情報学研究科)

On MODkP Counting Degrees : Lattice Embedding Theorems


10月30日
10:00 長野大介、馬場健介(九州大学大学院システム情報科学研究科)
佐塚 秀人 (久留米工業大学)廣川佐千男(九州大学大型計算機センター)

自然推論に基づく証明探索と反例生成

直観主義命題論理の証明探索において、探索の道順を記 憶しておくことで、証明できる場合には証明図を、証明できない場合には 反例としてのクリプケ・モデルを構成する手法を述べる。高さが2以上の クリプケ・モデルが生成される場合には古典論理におけるその命題の証明 も返す。また、この手法を用いて開発中の証明システムを紹介する。

10:30 加藤直行 (九州大学大学院システム情報科学研究科)
佐塚秀人 (久留米工業大学)廣川佐千男(九州大学大型計算機センター)

初等幾何証明システムのための正確な図の作成

初等幾何の問題を、具体的に描かれた図の情報を用いて 証明を生成するシステムを開発している。利用者が描いた雑な図を変形し、 仮定を満たすような座標を求める。こうして得られる正確な図に対しケー ディンガー、アンダーソンのPerceptual Chunksの手法を適用し、結論に至 る証明を構成する。

11:00
Break
11:10 姜 京 順 (神戸大学大学院自然科学研究科)

A Leveled IO-model for a Linear Logic Programming Language

A logic programming language Lolli which is based on intuitionistic linear logic is a superset of Prolog and I/O-model was proposed by Hodas and Miller as a execution-model for Lolli. In order to solve multiplicative goals (that is,the connection operation of the goal is multiplicative conjuntion) from the bottom up in the intuitionistic linear logic, we need to split the resource into two disjoint part. In the I/O-model ,to remove the non-determinism of such splits, each goal has its input resource and output resource and then all resource not used to prove a subgoal G1 will be used to prove the other subgoal G2 when proving the goal G1*G2. / In this paper, we propose a Leveled IO-model as an implementation-model that manage resource efficiently for Lolli. Input resource and output resource of the Leveled IO-model have an integer called consumption-level as the information that resource is either consumable or unconsumable. Our Leveled IO-model eliminate checking that each resource used to prove subgoals are same whenever proving the goal include additive conjuntion. In the Leveled IO-model, only resource used to prove a subgoal G1 will be used to prove the other subgoal G2 when proving the goal G1&G2. This idea is used at a compiler system of LLP which is a linear logic programming language and is a subset of Lolli. And also we can remove the non-determinism of “top” by improving the idea of consumpution-level.

11:40 赤間 陽二 (東京大学)

Type theory for partial combinatory algebras

Partial combinatory algebra (pca, for short) is a strict generalization of combinatory algebra, and it is not necessarily embedded into a combinatory algebra. With this notion, we can prove strong normalization of higher type theories semantically. By a type-theoretic method, we will analyze the pca, and find the intrinsic relation to the set of sn terms of combinatory logic. This leads to the solution of Bethke-Klop's question.

12:20
Lunch
13:30 沢村 一 (新潟大学 工学部)

HOLによるRelevant logicの定理証明機

 Relevant Logicは,古典論理に見られる「ならば」に 関する論理的違和感を取り除くことを目指した論理である。しかしながら、 この論理の難解さゆえに、それに対する自動定理証明法の研究は進んでい ない。
 本論文では、Relevant Logic Rに対する可能世界意味論を HOLの論理表現に翻訳することによって、適切論理の論理式の妥当性を証明 する方法を与える。次に、この翻訳に基づいて、適切論理のいくつかの論 理式の妥当性を、実際にHOLの証明機能を使って証明し、Relevant logic定 理証明機へのHOLによるアプロ−チの有効性を示す。

14:00 立木秀樹 (京都産業大学計算機科学科)

Gray code に基づいた実数の表現

実数を近似値として行うのではなく無限リストとして扱うことにより、無限に 精度の高い計算を考えることを、Exact real という。そのための実数の表現 方法として、通常の2進表現や10進表現を用いたのでは、3を掛けるなどの基本 的な関数も計算可能でなくなってしまう。その欠点を補うために、いろいろな コード系が今までにも提案されているが、それらは、一般に、高い冗長性を伴っ ている。この講演では、十分広い計算可能性を持ち、しかも、冗長性が低いコー ド系として、Gray code と呼ばれる2進表現に基づいたコード系を提案する。

14:30
Break
14:40 小澤正直 (名古屋大学情報文化学部)西村治道 (大学院人間情報学研究科)

量子チューリング機械と量子回路族の計算量の同等性について

素因数分解問題と離散的対数問題は従来の計算量理論で は,効率的アルゴリズムの存在しない問題とみなされてきた.いくつかの 公開鍵暗号系の安全性もそのことに依拠している.ところが,1994年に Shorによってこれらの問題を効率的に解く量子計算アルゴリズムが発見さ れ,量子計算機の研究がにわかに注目を集めることになった.量子計算の 研究は,1980年頃,Feynmanによって,量子力学系を古典力学的計算機で模 倣することの複雑性から,量子力学の原理を利用した,より効率の高い計 算の可能性が示唆されたことから始まった.1985年から90年にかけて, Deutsch は量子チューリング機械と量子回路の2種類の計算モデルを定式 化し,現在,量子アルゴリズムは,これら2種類のモデルを通して表現さ れる.本講演では,量子チューリング機械と量子回路の厳密な数学的定式 化を与え,量子回路族に対する一様性の概念を導入することで,この2種 類の計算モデルの計算能力が計算量の観点から同等であることの証明を示 す.

15:20 鴨 浩靖 (奈良女子大学理学部) 河邑 紀子 (奈良女子大学人間文化研究科)
竹内 泉 (京都大学工学研究科)

「分裂次元図形と計算量」

 最近、数学の諸概念を計算可能性の立場から眺めた計 算可能性数学が注目されている。その方法を使って、分裂次元図形の図形 の複雑さを計算の複雑さによって測ることが出来ないかどうか、という問 題は興味深い問題である。 今回の研究は、計算可能性数学の中で多項式 時間計算可能性を定義し、次元分裂図形と多項式時間計算可能性との関係 を幾つか証明する。また、次元が1であり、NP完全であるような次元分 裂図形を紹介する。

15:50
Break
16:00 亀山幸義 (京都大学)

部分継続の計算系

関数型プログラミング言語における継続が古典論理の計算的意味との 関連で注文を集めているが,より論理的に取り扱うことが容易で,プログラミ ング上も有用な部分継続について,型理論の枠内で定式化する.

16:30
Business Meeting
18:30
懇親会

10月31日
10:00 渡邊 宏 (北海道大学大学院理学研究科)

The subobject classifier of the category of labeled transition systems and simulation maps

遷移系と呼ばれるラベル付きグラフは,プロセス代数あるいは様相論理の意味領 域・計算のモデルなど,さまざまな分野で利用されている.
本研究では,遷移系の模倣写像を射とする圏を考察した結果,この圏が(積は持 たないが)自然な対称閉単圏の構造だけでなく,分類対象(subobject classifier)も持つことを見いだした.分類対象の存在証明は,木の形をした遷 移系からなる稠密な小部分圏が存在すること,この小部分圏上の前層圏に遷移系 の圏を埋め込めること,そしてこの埋め込みがreflectionを持つこと,に基づく. 存在証明の鍵となる補題は,部分圏上の前層圏に関する一般的事実であり,他の 圏への応用もあると思われる.
以上の考察により,遷移系の模倣写像を射とする圏は,分類対象の存在する対称 閉単圏となる.このようなタイプの圏の理論的意義は今後の課題である.

10:40 Stefanescu, Gheorghe (九州大学・ University of Bucharest)

Network Algebra: Past, Present, and Future

Kleene's calculus of regular expressions and the associated regular algebra describe in an elegant way cyclic processes with global states. This calculus has a deep mathematical theory and many applications to sequential programs, automata, formal languages, circuits, etc. but less in parallel/distributed computation.
The ``Network Algebra'' and the associated ``Calculus of Flownomials'' may be seen as an extension of the above calculus to cope with processes having multiple entries and exits, i.e., pins for connections. Each pin may be seen as a local state and this makes the extension well-suited for distributed computation. Applications to dataflow networks, process graphs, or action calculi have already been done. Technically speaking, the main ingredient is a new axiomatic looping operation, called ``feedback''; it connects an output to an input and then both pins are hidden.
This new setting allows for a simple algebra (BNA) for flowgraphs modulo graph isomorphism. We claim that whenever a cyclic process is implicitely of explicitely present, a semantic algebra fulfilling the BNA axioms may be constructed.
On top of this algebra one may add simple axioms to cope with correct and complete axiomatisations for certain classical equivalences, e.g., the equivalences associated to the input behaviour (or equivalently, those given by unfolding flowgraphs into trees), bisimulation or input-output behaviour. The so called `enzymatic rule' which produces these equivalences is a rule to reason in a cyclic environment.
The first part of the talk includes a short introduction to network algebra. Then we present some new results, mainly related to the mixed network algebra project. The BNA axioms seem to be very basic. After their introduction (Stefanescu 1986) the BNA axioms were rediscovered in various setting, e.g by Bartha (systolic systems), Stark (dataflow networks), Milner (action calculi), Joyal-Street-Verity (traced monoidal categories), etc. The last part of the talk includes some comments on these papers.

11:10
Break
11:20 大塚 寛 (九州大学大学院数理学研究科)

ブロードキャストを考慮したプロセス代数におけるデッドロック

従来のプロセス代数におけるプロセス間の通信とは、基 本的に1対1通信である。他方、分散メモリ型並列コンピュータ上のプログ ラミング環境ではプロセス間通信を支援するために、1対1通信のほかに一 斉通信や集団的通信等の通信機能が提供されている。
ここで、たとえ 集団的通信が1対1通信で実装されていたとしても、集団的通信の性質等を 直接解析し、集団的通信を伴うプロセスの仕様の検証を行なうには、集団 的通信を直接記述できるプロセス代数の体系のほうが望ましい。そこで本 研究では、集団的通信のうちブロードキャストに代表される1プロセス対複 数プロセス間の通信に対する代数的取り扱いを試みた。本報告では、1対1 通信に伴うより複雑な振る舞いをする集団的通信に伴うデッドロックの性 質などについてのべる予定である。

11:50 田辺 誠 (科学技術振興事業団 さきがけ21)

時相線型論理と時間ペトリネット

It is well known that Petri nets constitute the algebraic structure of quantales, which can be models of linear logic. As a timed extension to quantales, timed R-monoids are defined, which are constructed from timed Petri nets.
Next, temporal linear logic is introduced, which has timed Petri nets as its models, i.e., whose formulas can be interpreted as sets of timed markings of a timed Petri net.
Finally, examples show how to express properties of timed Petri nets by temporal linear logic.

12:20
Lunch
13:30 中松 和已 (兵庫県立姫路短期大学 経営情報学科)

ベクトル真理値付き論理について(On the Vector Annotated Logic)

defeasible推論、マルチエイジェントシステムのモデルへの応用 を目的として、ベクトル真理値付き論理を提唱する。 これは、 V.S.Subrahmanian, Newton,C.A.Da Costaらによって提唱された 真理値付き論理(annotated logic)の真理値(annotation)をベクトルに 拡張したものである。

14:10 下田 守 (下関市立大学)

ファジィ集合の基本演算について

 ファジィ理論で最も基礎となるファジィ集合は,普通 の集合の概念を拡張して,集合への所属度の真理値集合を二値から実数の [0,1]区間に拡大したものである.今までのファジィ集合論では,和集合・ 共通集合・補集合という最も基本的な3演算についても,さまざまな定義 が数式だけで提案されている.また,同じ集合の上のファジィ集合の間の 演算だけが考えられており,異なる集合の上のファジィ集合の間の演算の 定義はほとんど見受けられない. ここでは,ある完備ハイティング代数 を真理値集合とする直観主義的集合論の階層モデルにおいて,通常のファ ジィ集合を拡張してファジィ集合を定義すると,ファジィ集合の包含関係・ 和集合・共通集合などの基本的な関係と演算が普通の集合と同様に自然な 意味をもつことを示す.この自然な解釈に従えば,異なる集合の上のファ ジィ集合の間の演算も容易に考えることができる.

14:50 古澤 仁 (九州大学大学院システム情報科学研究科)

A Representation Theorem for Relation Algebras: Concepts of Scalar Relations and Point Relations

関係計算とは, 二項関係の演算のもつ性質を考察するた めの形式的枠組であり,関係計算を公理的に取り扱うために提案されたの がTarski(1941)によるブール関係代数である.Tarskiは1941年の論文の中 で「ブール関係代数は通常の関係のなす代数と同型か?」という表現問題 を提示した.これに対しSchmidtら(1985)は点関係とこれに関する公理を導 入することによりブール関係代数の表現定理の平易な証明を与えた.
一方,Goguen(1967)は,Zadehによるファジィ関係の概念を,ファジィ関係 が帰属度として0-1閉区間の実数をとるのに対して帰属度として任意の束上 の値をとるような概念に拡張し,これをL-関係と名付けた.本研究では, スカラー関係と点関係の概念とそれらに関する公理を導入することにより ブール的でない関係代数がL-関係のなす代数と同型であること(関係代数の 表現定理)を示す.



SLACS '97 @ Kyushu University 幹事
森   雅  生@九州大学システム情報科学研究科
              情報理学専攻
E-mail:masa@i.kyushu-u.ac.jp
http://www.i.kyushu-u.ac.jp/~masa/
Tel:092-642-2693