この集会（及び過去２年間のslacs）は、科研費基盤(B)(1)「算術と計算の 論理構造に関する研究」（研究代表者：田中一之（東北大理））の援助を受けて 行わています。 この会での成果を論文等に発表されるときは、当科研費による 部分的なサポートがあったことを記していただければ幸いです。 また、今年度末に報告集を作成するため、最近２，３年の論文、プレプリント等で 報告できるものをお持ちの方は、田中（郵便の場合）または赤間（e-mailの場合） に１２月１７日までにお送り下さい。 ご協力よろしくお願い致します。 以下のプログラムは10月21日現在です。
広川は、線型項とβ正規な準線型項の最汎型の特徴付を行なった。 庄司は、それと同様の証明方法で、βη正規な線型項の最汎型の特 徴付を行なった。本研究では、ベラルディの枝刈の方法によって、 これらの証明の関係を与える。その応用として、βη正規な準線型 項の最汎型の特徴付を与える。
We introduce the notion of ω-hypergraphs, a higher dimensional generalization of hypergraphs. They are obtained in the way of pursueing proper notions of weak hyper-dimensional categories. Our definitions are folly mutually inductive.
階層的な型の上で定義された、多相的な関数の定義の一様性が異なる３つの計算に ついて、構文論、意味論的性質を調べる。
部分継続の１つの定式化を与え，これが Dybvig らの subcontinuation の一般 化になっていることを示す．この体系は，複数の部分継続がそれぞれ異なる Answer Type を持つため，通常の（単純な）形のCPS変換を与えることができ ない．本講演では，多数の継続を渡していく方式での CPS変換を与え，この変 換が型と簡約を保存することを示す．
論理プログラミングの意味論において、bilattice の理論は重要な役割を果たす。bilattice とその prime bifilter からなる構造で特徴付けられる論理の公理化は Avron により得られているが、一般に、bilattice においては prime bifilter は存在しない。ここでは、分配的な bilattice においては常に prime bifilter が存在することを示し、これらの構造で特徴付けられる論理について述べる。
WKL_0 is RCA_0 plus weak K\"onig's lemma: every infinite tree of sequences of 0's and 1's has an infinite path. In this paper, we first show that for any countable model (M,S) of RCA_0, there exists a countable model (M,S') of WKL_0 such that S ∩ S' consists of all Delta^0_1 subsets of M. By sophisticating this argument, we show that if a functional is arithmetically definable in WKL_0, it is already so in RCA_0. More precisely, it is shown that if WKL_0 proves ∀x∀X∃! Y. φ(x,X,Y) with φ arithmetical, so does RCA_0.
In this talk, we discuss correctness criteria for commutative Moltiplicative Linear Logic (MLL). One of such criteria is due to Guerrini, announced in LICS'99, which implements Danos' parsing reduction algorithm by means of a so-called sequential unification algorithm in linear-time. We shall compare the algorithm with other correctness criteria based on Girard's original trip condition.
NFL is a system of natural deduction which is obtained by deleting all the structural inference roles, namely Contraction, Weakening, and Exchange. We first point out that there can be various definitions of redexes for NFL, and then, we will investigate deferent types of normalization theorems for NFL.
This paper presents the notion of D-normal proofs, which is defined syntactically and gives one of the weakest condition for uniqueness of normal proofs. This paper proves the following resolts: (1) βηD-normal proofs of a formola are unique. (2) A β-normal proof of a PNN-formola is D-normal. (3) A β-normal proof of a minimal formola in BCK logic is D-normal. These resolts give other proofs of uniqueness of βη-normal proofs of a PNN-formola, and uniqueness of βη-normal proofs of a minimal formola in BCK logic.
クリプキモデルに関して完全であるような様相無限論理にcut-free systemを与える． 様相無限論理がクリプキ完全であるためには，様相述語論理において 「定領域の公理」の名で知られている論理式にちょうど対応する，あ る公理を満たさなければならない．また，与えられたシステムの完全 性を示すにあたり，無限論理が通常コンパクト性を満たさないことか ら，よく知られたHenkin流のcanonical modelの構成がうまく働かない． これらの点をクリアするために，Gentzen流のsequent calculusにある 拡張を施したformal systemを導入する．
ここで扱う命題論理は、最小の直観主義様相論理に２つの公理 ｐ⊃□ｐ、□□ｐ⊃□ｐを追加して得られる様相論理である。この様相論 理における様相記号□にはいくつかの解釈が与えられてきている。 Goldblattの1981年の論文では、□Ａ が正しいことを「Grothendieck topology においてＡが局所的に正しい」と解釈している。Fairtlough and Mendlerの1985年の論文では、□Aを「ある制限のもとでA」と解釈し、論 理回路におけるONとOFF以外の不安定な状態も表そうとしている。 Benton, Bierman and de Paiva の1998年の論文では、この様相論理を、 Moggiによって導入されたcomputational typed lambda calculus と Curry-Howard の対応付けができる様相論理として取り上げている。 本報告では、直観主義命題論理におけるDiegoの定理、およびUrquhart の定理を、この直観主義様相論理に拡張した結果を示す。
休憩
型はデータの仕様であるという考え方に基づいた型体系を提案し、その 完全性と型チェックのアルゴリズムを示す。この型体系では、型チェックの枠 組の中で、より詳しいデータの整合性の検証が行なえる。
Hindley/Milner流のパラメータ多相型の型推論を、制約型システムの枠組みの中 で議論する。パラメータ多相型は型変数に対する代入によって多相性を表すが、 これを一般化し、多相性を制約の特殊化によって表すような制約多相型の枠組み を提案する。この一般化された制約多相型の枠組みの中で、ある型がある型の代 入によるinstanceであるという制約をもつような制約系に限定したものを考える。 このような制約系のもとでパラメータ多相型推論アルゴリズムの変種を定義し、 その変種アルゴリズムの正しさを証明する。この証明の過程で、変種アルゴリズ ムが正しく動くために必要な、パラメータ多相型の型推論に共通する条件が明らかになる。
From the viewpoint of partially typed terms, we introduce fine structures between Church-style and Curry-style. In the uniform framework, we study the problems of type checking, typability, and type inference of the lambda-terms between the two styles. It is found that in the second-order lambda-calculus (strictly speaking, at the rank 2 fragment), domain-freeness and type-holes [ ] are independently responsible for the undecidability of the partial type reconstruction problem.
This talk is about termination of rewrite systems. The aim of dummy elimination, a termination method introduced by Ferreira and Zantema, is to transform a given rewrite system into a rewrite system whose termination is easier to prove. We show that dummy elimination is subsumed by the dependency pair method of Arts and Giesl. More precisely, if dummy elimination succeeds in transforming a rewrite system into a so-called simply terminating rewrite system then termination of the given rewrite system can be directly proved by the dependency pair method. Even stronger, there is no need to use dummy elimination as a preprocessor to the dependency pair method. To a large extent these results also hold for the recent argument filtering transformation of Kusakari et al. The talk is based on joint work with Juergen Giesl.
1900-- 懇親会(@海鮮屋、国分町、022-261-5559;出欠を２６日１６００までにお知らせ下さい。)
強計算可能距離空間には自然に計算可能性構造が入ることと、実効的可分な 距離空間は計算可能距離空間であることを示す。
回路の深さが iterated logarithm の多項式で押さえられる 関数のクラスを考えると, これらは AC^1 の部分クラスになることが わかる. 講演ではこれらのクラスに対する弱い recusion scheme を 用いた特徴づけを, unbounded fan-in と bounded fan-in のそれぞれの 場合に与える.
Epistemic logics with moltiple players are ones with modal operators describing belief and/or knowledge of the players. We develop epistemic world semantics for epistemic logics of shallow depths for investigation of game theoretical problems. Here, by shallow depths, we mean that nesting and alternating occurrences of belief operators in formolae are restricted by a given epistemic structure. We prove the completeness theorem on the epistemic logics of shallow depths with respect to the epistemic world semantics. We present an application of our semantics to obtain a game theoretical theorem concerning decision making in a game.
E. Moggi の computational λ-calculus における緩論理的関係 (lax logical relation) について基本補題を示す。緩論理的関係は論理的関係を弱め たもので，合成について閉じており、高階データのデータ精製を論じるのに適当 な概念と思われる。