第19回 「記号論理学と情報科学」(SLACS 2002) 講演要旨

2002年9月18日(水)午後 〜 9月20日(金)

千葉大学 理学部 (西千葉キャンパス 理学部1号館 2階 121講義室)

高橋正子, 論理学の歴史とコンピュータ

現代のコンピュータの原型といわれる万能コンピュータが半世紀前に登場し,更にその約半世紀前に(数学的な)論理学が誕生した.本論では,一足先に生まれた論理学がコンピュータの誕生に際してどのような役割を演じたかについて考察する.

坂本伸幸, 選択汎関数と高階逆数学

従来の2階算術の枠組みでは取り扱えない、高階の対象に関する逆数学現象について話す。

宮崎 裕, There exists a continuum of normal modal logics over KTB

We show the fact of the title by presenting a class of ortholattices, each of which defines an incomparable orthologic with one another, and then by embedding every different orthologic into a distinct normal modal logic above KTB.

菊池健太郎, 明示的代入計算とカット除去の強正規化性について

Herbelinの明示的代入計算はGentzen流の型システムをもち、代入増植の簡約規則を加えれば、λ計算のβ簡約を模倣することができる。この体系における型付き項の強正規化性について検討する。

西澤弘毅, 多様な Context の形式化のための Logical Framework

数学、論理学、計算機科学などにおける演繹システムについて, その文法, 公理, 推論規則などを形式化して性質を証明する手法として, 型理論を用いる logical framework が盛んであり, そのためのさまざまな型理論やそれらの実装方法が研究されてきた. logical framework では, 形式化手段となる型理論における変数や, その集まりである context の性質を最大限に活用し, 形式化される対象システムに似た性質があれば, それらを直接的に対応させて形式化する. それにより、対象システムの複雑な性質をも簡単に形式化し証明できる. しかし, 対象システムに特化したさまざまな型理論が必要となり汎用性に欠ける. たとえば, Linear LF(Logical Framework), Ordered LF, Relevant LF, Concurrent LF などがある.

そこで本研究では, そのようなさまざまな LF の context を統一的に形式化するための型理論として 2-level LLF(Linear Logical Framework)を提案する. これは今までのさまざまな LF の context が果たしていた役割を基本的には一つの linear な context に果たさせ, それをコントロールするためにさらに high-level の linear な context を用意したものである. 2-level LLF の型検査の decidability は Linear LF とほぼ同じ方法で示すことができた.

2-level LLF では, linear な context の中で特定の変数宣言が無いということを検査できる. このような一種の negation により, 形式システムをシミュレートした時に証明探索の戦略に依存しないような negation を実現できる. また, 定義した演算子ごとに, linear な context の中で additive に使われるものと multiplicative に使われるものを自由に指定できる. これは, Ordered LF, Relevant LF, Concurrent LF を統一的に形式化するには必要な拡張である. さらに必要な拡張としては, 変数の型の中に他の変数が出現できる関係である dependency を形式化できるようにすることなどがあり, これらは今後の課題である.

松野裕、佐藤周行, Flow Analytic Type System for Array Bound Checks

Array Bound Checkのためのデータフロー解析をもとにした型理論の枠組みを提案する。

山本章博, 論理と機械学習の接点に関する一考察 --反単一化の拡張を出発点として--

近年,記号論理学と機械学習の密接な関係が明らかになりつつある.両者にどのような関係があり,今後どのような問題が解決されるべきかを,反単一化を出発点として概観する.

本多 和正, Dedekind圏の不等式命題の自動証明システム

項書き換えにより証明図生成を行う。

古森 雄一, Russel の逆理と BCK\beta\eta

ラッセルの逆理は表現 $\{x\mid x\notin x\}$ を項として認め \[\mbox{任意の項} t \mbox{および任意の論理式} \ \alpha(x) \ \mbox{について, \ } t\in \{x\mid \alpha(x)\} \Longleftrightarrow \alpha(t)\] という原理さえ認めれば他の(外延性公理など)公理は一切なしでも出てくるので, 論理の矛盾としてとらえられ深刻な影響を与えた[注: 当時, ここに書いたように認識していたわけではない。ここでは, 現代の立場でしかも構文論を強調した書き方をした。当時は構文論と意味論の区別もはっきりしていなかった]。

古典論理や直観主義論理では, ゲンツェンのシークエント計算でいうと縮約(contraction)が推論規則であること, 同じくゲンツェンの自然演繹でいうと一度に 2 つ以上の仮定が落とせること等が, ラッセルの逆理が導けることと密接に関係している。BCK 論理は宿約を推論規則として持たないのでラッセルの逆理はでない。このことは 1970 年代には分かっていたことであるが, より精密なことが最近分かってきた。

福井 清香,鹿島 亮, Standardization Theorem for Left-normal Orthogonal TRSs

一般的な Left-normal Orthogonal (non-overlapping) Term Rewriting Systems に関する標準化定理を、「標準変換で到達する」という二項関係を用いて簡潔に証明する。

SLACS 2002 Homeへ戻る


Last modified: Sun Sep 15 17:54:43 JST 2002