仕様の近似過程を表現する様相付き型付けシステムを応用すると、非常に広 い範囲の仕様や実現に対して、自然な構成的プログラミングが可能となるこ とをいくつかの例によって示す。
Refinement (nonstandard) typeとは，通常の型上の１変数述語を意味し，そ の型チェックないしは型推論の枠組の中で，様々なプログラムの解析が可能で あることが知られている．この発表では，単純型体系の上に，intersection とunionの集合演算と備えたrefinement typeの形式体系を定義し，その型チェッ ク・アルゴリズムを提案する．また，実際に計算機上で実装した結果を示し， 実用化システムに向けてのいくつかの課題を検討する．
従来の Kleene の関数適用 f|g より直感的に理解しやすい関数適用 f`g を定義 し,この関数適用を用いても countable functional を定義できることを示す.ま た,この関数適用を用いて type-free theory APP のモデルを構成できることも 示される.
XPE(X Proof Editor)は、TeXでの証明図の作成を支援するソフトである。こ のXPE上でtheorem proverを呼び出すことにより、容易に利用できる可読性と 再利用性の極めて高いtheorem proverとなった。 2000/8/15現在の利用可能な体系(命題論理):classical logic, intuitionistic logic, FLe, FLew, FLec, K, KT, S4, S5(高野の決定手続きによる),type assign
ω正則言語の測度は有理数である。
We present an extension of term rewriting systems with the mechanism of synchronization, called synchronized TRS's. The notion of synchronization is newly introduced for synchronizing applications of rewriting rules. We prove the fundamental properties of the synchronized ground TRS's: (1) The reachability problem of synchronized ground TRS's is equivalent to the Post's Correspondence Decision Problem. (2) The halting problem of synchronized ground TRS's is equivalent to that of a two-counter automaton.
In this talk, I propose simply typed term rewriting systems, which extend first order term rewriting systems to the higher order case by allowing higher order symbols but without using bound variables. We discuss a semantic method for ensuring termination of simply typed term rewriting systems.
weak interlaced bilattice は論理プログラミングの意味論において 重要な役割を果たしているが，この代数系の数学的構造については 不明な点が多い．ここでは，この代数系の持つ基本的な性質を 考察し，得られたいくつかの結果について述べる．
ファジィ関係については，今まではほとんどの場合にクリスプ集合の上の ファジィ関係，すなわちクリスプ集合の直積のファジィ部分集合が扱われて きた．今回は一般のファジィ集合（クリスプ集合のファジィ部分集合）の上 のファジィ関係のいろいろな性質について考えてみたい．
In most cases fuzzy relations have been treated as fuzzy relations on crisp sets, that is, as fuzzy subsets of cartesian products of crisp sets. In my talk various properties on fuzzy relations on fuzzy sets (fuzzy subsets of crisp sets) will be discussed.
We study Goedel's Dialectica interpretation of HA by T from the perspective of the game semantics of PCF. The higher-order functions are then seen as the first-order functions plus strategies. To make this point concrete, we define a version of Hintikka game for the first-order formulas and show how to read out the winning strategy from a proof.
theoretical computer science は難しすぎるという声を時々耳にします． 私の考えでは，tcs は底の浅い分野ではないから当然だという気持ちと， もう一つは，歴史の浅さやその他の事情から未成熟な部分をいろいろ抱え たまま教育が行われているためではないかという気がします．この後者の 観点から，「証明と型」と「計算論」に関する私のささやかな試みについ てお話してみたいと思います．
We present a new proof of the standardization theorem in lambda-calculus, which is performed by inductions based on an inductive definition of beta-reducibility with a standard sequence.
We introduce a new natural deduction formulation with one conclusion for implicational classical logic. The idea of the formulation is based on proof by ``case analysis''. We define reduction rules and prove weak normalization. As a corollary, we have the subformula property for normal proofs.
This is a joint work with Sachio Hirokawa, Ryo Kashima, Yuichi Komori and Izumi Takeuti.
There have been much interest in the conditions for uniqueness of normal form proofs in intuitionistic logic. [Tatsuta99] introduced a notion of D-normal form proof and showed that D-normal form proof is unique for any implicational formula. But this result means the uniqueness of D-normal form proof. There may be some other normal form proof which is not D-normal. We show that D-normality yields the uniqueness of proofs as long as the long-normal form proofs are concerned.
The duality between values and continuations enables us to exchange the call-by-name programming paradigm for the call-by-value one and vice versa. Since recursion is an essential factor for programming languages and the $\lambda\mu$-calculi fit in this duality, we extend the $\lambda\mu$-calculi with recursion operators and demonstrate the duality between recursion and iteration in the $\lambda\mu$-calculi.
We introduce structural rules mingle, and investigate theorem-equivalence, cut- eliminability, decidability, interpolability and variable sharing property for sequent calculi having the mingle. These results include new cut-elimination results for the extended logics: FLｍ(full Lambek logic with the mingle), GLm(Girard's linear logic with the mingle) and Lm(Lambek calculus with restricted mingle). Moreover we show that Lm is useful for an application to the categorial grammar.
Propositional lax logic(PLL)はMoggiが導入したComputational typed lambda calculus とカリー・ハワードの対応が つけられる直観主義様相論理である。ここでは、PLLにおいて、ｎ個の命題変数と⊥から選言以外の論理記号を用いてで きる論理式の集合Fについて述べる。具体的には、順序集合(Ｆ／≡、≦)の構造を、それと同型なモデルを帰納的に定義 することで明らかにする。ただし、A,B∈Fに対して、[A]≦[B] iff Ａ⊃Ｂ∈PLLである。
We present some proof systems for common knowledge predicate logic which is complete with respect to the class of Kripke frames with constant domains.
According to Church's Thesis, all reasonable (sufficiently expressive) programming languages have the same computational power in the sense that they can compute the same class of functions on the natural numbers. However, if we measure the computational power of programming languages in more subtle ways (e.g. we consider which operations are computable at higher types), then interesting differences emerge between different languages, and we discover several natural notions of "computability". In this talk I will give a brief survey of various notions of computability, and of current research in this area.