Re: プログラミングと論理学(Re:Re[2]: 大文字と小文字の区別)
久野です。
kono@ie.u-ryukyu.ac.jpさん:
> 最近は「単に動くだけ」じゃだめで、「信頼性高く動く」ってのが
> 要求されるじゃないですか。それはスクリプト言語だってそうだと
> 思う。「素朴に論理的に考える」では足りなくなってきていると思
> う。
ああpreとかpostとか書き出すとそうなるのは賛成します。
> 型とかって論理学として定式化されたものの典型だったりしますよ
> ね。(で、割りと役に立たないわけだが...) クラス=型みたいな考
> えだと、推論とか自然に出て来るし、そこで、否定の扱いが難しい
> とかってのも論理学の成果だったりますよね。そういうのを余計って
> いうなら、そうかも。
未だに型の理論は判りません。型と型に包含関係があって、Javaのイ
ンタフェースみたいに複数の包含関係があって(しかも順位があって平
等ではなくて)、それらのさまざまな型が複数テンプレートパラメタに
現れることで新しい型が構築されて、そしてC++のようにそのテンプレー
トパラメタが自分自信の親クラスだったりして、それを論理学の型で
「プログラミングの役に立つように」定式化できてるんだろうか。そう
いうのがスッキリ扱えるという論文知ってたら教えてください。
そういう部分では現実は理論より奇なりという気がする。 久野
Fnews-brouse 1.9(20180406) -- by Mizuno, MWE <mwe@ccsf.jp>
GnuPG Key ID = ECC8A735
GnuPG Key fingerprint = 9BE6 B9E9 55A5 A499 CD51 946E 9BDC 7870 ECC8 A735