神戸です。

On Wed, 8 Sep 2004 07:28:53 GMT, <kuno@gssm.otsuka.tsukuba.ac.jp> wrote:
> 久野です。
> 未だに型の理論は判りません。型と型に包含関係があって、Javaのイ
> ンタフェースみたいに複数の包含関係があって(しかも順位があって平
> 等ではなくて)、それらのさまざまな型が複数テンプレートパラメタに
> 現れることで新しい型が構築されて、そしてC++のようにそのテンプレー
> トパラメタが自分自信の親クラスだったりして、それを論理学の型で
> 「プログラミングの役に立つように」定式化できてるんだろうか。

論理学でラッセルのパラドックス（だったかな？）を解決するために考え出された
純粋なType Theoryは私もよく知りません。
数学辞典でさえ、歴史的に重要だが現代ではもはや重要ではないという扱い
だったと思います。
データ型の理論では集合に「型」というラベルをつけて区別して整理するという
アイディアだけ頂いて、元ネタである純粋なType Theoryはあまり気にしていないと思います。

現状のデータ型と論理の関係について私の理解を書きますと：

プログラムを構成する式とその部分式に対する
それぞれの型の間に成り立つ関係式は
全て包含関係（＝半順序関係）か同値関係なので全体として型の代数構造は束になります。
で、型検査や型推論はその上で関数と変数のある方程式を解くことと考えることができて、
自動定理証明分野の話に持っていけて、
その証明プログラムの中身は論理学由来のアルゴリズムでゴリゴリと動いていると。
ただし、言語の型システムに制約を加えるとアルゴリズムが簡素化できたりして
そうなるとプログラムには論理学由来の部分が
明らかには現われなくなったりするでしょう。
（変数と関数引数の型宣言必須で多相型がないとか。ユーザー定義型がないとか。）

けどここまでくるともう論理学だけでは実際問題として間に合わないので
代数学の枠組みを使って定式化されています。
そして論理学が方程式の解を求める手順を記述するなどの
基礎構造に使われてる訳です。

…というようなことを考えると論理学の範囲に拘ってそれだけで
話を終わらせようとするのは実際的でありません。
（代数学という「高級言語」があるのに論理学だけで頑張ることはないというか。）
けれど論理学抜きにすると基礎がガタガタになって証明や基礎付けができなくなるんで
天下り式に定義と定理をズラズラ並べてとにかく覚えてもらったり、
例を挙げまくって帰納的に学習してもらったりということになって
やっぱり学習効率が落ちるかナァという話に。

結局、勉強しといた方がいいよリストに
「（初等）論理学」に加えて
「（初等）代数学」、「（初等）集合論」追加の予感
…（´・ω・｀；）ドンドン増える？

-- 
http://www.nerimadors.or.jp/~kando/
kando@nerimadors.or.jp
kando_takayuki@hotmail.com : MSN Messenger