東北大学・電気通信研究所・外山研究室ではNUEセミナーを開催しています． テーマはプログラム理論や定理自動証明を中心に， 情報科学の理論的なさまざまな話題をとりあげています． 興味をおもちの方はどなたでもフラリと気楽におたちより下さい．
| 日時 | 2000年12月21日 |
|---|---|
| 講演者 | 佐藤 雅彦 (京都大学) |
| 題目 | $\alpha$: A purely functional language with imperative language inside |
| 要旨 |
We present a purely functional language $\alpha$ that naturally
contains an imperative language as its sublanguage. $\alpha$ is pure
in the sense that (1) it is confulent and (2) it is a conservative
extension of the pure $\lambda$ calculus. The purity of $\alpha$
makes it a mathematically and logically well founded language. For
example, it becomes possible to prove properties of programs written
in $\alpha$ by equational reasoning. The main characteristic of $\alpha$ is that it has environments as first-class objects. By using first-class environments, we can encapsulate imperative programs by treating imperative programs as {\it environment tranformers}. In this way, side-effects caused by the execution of imperative programs becomes invisible from outside. We also discuss another usages of first-class environments. For example, we show that given an abstract obtained by abstracting several variables, we can instantiate any of these variables by specifying the name of the variable to be instantiated and the value which will replace the variable. |
| 日時 | 2000年11月8日 |
|---|---|
| 講演者 | Jean-Pierre Jouannaud (Universite de Paris Sud) |
| 題目 | A Higher-Order Recursive Path Ordering for Typed Lambda-Calculi |
| 要旨 |
This work extends the termination proof techniques based on
reduction orderings to a higher-order setting,
by adapting the recursive path ordering definition
to terms of a typed lambda-calculus
generated by a signature of higher-order function symbols.
The typing discipline is based on
ML-like polymorphism and sort constructors.
The obtained ordering is well-founded, includes beta-reductions,
is monotonic with respect to the function symbols,
and stable under substitution.
It can therefore be used to prove the strong normalization property
of higher-order calculi in which constants can be defined
by higher-order rewrite rules.
For example, the polymorphic version of Goedel's recursor
for the natural numbers is easily oriented.
And indeed, our ordering is polymorphic, in the sense
that a single comparison allows to prove the termination property
of all monomorphic instances of a polymorphic rewrite rule.
Many non-trivial examples are given
which examplify the expressive power of the ordering. This work is an extended and improved version of our LICS'99 paper. The ordering itself has been made much more powerful, in particular by replacing the congruence on types used there by a well-founded ordering on types. This yields a very elegant presentation of the whole machinery by integrating both orderings into a single one operating on terms and types as well. This presentation will be in turn the basis for generalizing it to dependent type calculi. We will briefly discuss this generalization if time permits. |
| 日時 | 2000年11月7日 |
|---|---|
| 講演者 | 奥居哲 (三重大学) |
| 題目 | λ項を用いた抽象ナローイングとその完全性 |
| 要旨 | 抽象的なナローイングを定式化し，その完全性を論じる． もともと一階の等式の求解法として提案されたナローイングは 関数・論理型プログラミング言語の基礎として発展し， 現在では高階項書換え系を用いた高階の項におけるナローイングや， グラフ書換え系を用いたナローイングも提案されている． 前者はHaskelやMLのような高階関数を扱う機能をもつ言語の， 後者は遅延評価機構の計算機上への実装のモデル化に適している． これらのナローイングに共通するもっとも重要な理論的性質は 求解完全性であるが，その証明はそれぞれの定式化の枠組みで 別個に行わざるを得なかった． そこで我々は，これらのナローイングを統一的に扱える 抽象的な枠組みを提供し， 種々のナローイングの求解完全性を簡潔に示すことを目指す． 我々の定式化はvan Oostrom による高階項書換え系を用いる． この定式化で特徴的なのは， 代入をλ項上の計算として抽象化している点である． 本稿では，ナローイングをこのように定式化することで， 求解完全性の証明が従来のものと比べ はるかに簡潔で見通しよくなることを示す． また一階のナローイングをこの枠組みでモデル化することで， 抽象ナローイングにおける求解完全性から 一階のナローイングの求解完全性を導けることを示す． |
| 日時 | 2000年6月29日 |
|---|---|
| 講演者 | 竹内泉 (京都大学) |
| 題目 | λ方体の中の共形性とパラメトリシティー |
| 要旨 | パラメトリシティーの性質は，多相型の計算体系の意味論的な性質である． 多相型の計算体系には，例えばジラールの体系Ｆがある． パラメトリシティーの性質の許では， 体系Ｆの中で直積や直和，初代数や終夜代数などの圏論的な性質が表現できることが， 長谷川立らによって示されている． また，体系Ｆに対しるパラメトリシティーは， アバディ，キュリアン，プロトキンらによって 形式論理の上での公理化がなされている． 本研究では，体系Ｆに対して定義されていたパラメトリシティーを バレンドレヒトのλ方体に拡張する． λ方体上のパラメトリシティーを定義する際には， 共形性の関係が本質的に働いている． λ方体の最高頂点であるλＰωでは， パラメトリシティーの公理系から，随伴函手の性質など， 一部圏論的な性質を証明することが出来る． |
まで．