#「ソースから演繹できる情報を全て使って...」< それが静的解析ってもんです。♪り、り、りすばーこい、こっちのみーずはあーまいぞ :)
#そうなんだけど、動的言語だってコンパイラは静的解析やってるわけで、言語として動的静的って話じゃないってこと。
#それはそうなんだけど、どこまで静的解析ができるかは言語の性質にかなり依存するのではということ。
#どういった情報を、いつまでに確定させておくか、という見方をすると、動的/静的というのは0/1ではなく、連続したスペクトルと考えた方が自然だよね。
#静的型というのは、「コンパイル時までにこういうフレームワークで情報を確定させておくといろんな性質が解析しやすい」っていう体系
#そう観るとHaskellは面白いな。メタ情報については早めに確定、実行時の情報についてはできるだけ確定を遅らせる、というアプローチか。
#もし実行というフェーズがはっきりとあるなら、その前後で。
#かぶった。
#LispのREPLセマンティクスでは、ある式の定義/評価はそれまで積み上げられた環境に対して行われるわけだけど、その環境にある情報は(メタ情報であろうと、実行時データであろうと)利用できる。
#たとえばGaucheのtrunkで、
#(use srfi-1)
(define-constant ones (circular-list 1))
(define-inline (foo x) (if (pair? x) (car x) #f))
(define (boo) (foo ones))
#Lispには定義と実行が混在するので
#こんな定義をすると、booのコンパイル時にはfooもonesも値が確定しているので、booは単なる定数関数になる。
#gosh> (disasm boo)
CLOSURE #<closure boo>
main_code (name=boo, code=0xab83a0, size=2, const=0, stack=0):
args: #f
0 CONSTI(1)
1 RET#これは型情報を使ってないけれど、静的解析ではあるよね。
#「動的/静的というのは0/1ではなく、連続したスペクトルと考えた方が自然」ということかな。
#Haskellでさ、メタ情報に関する遅延計算っていうのはあるの? つまりコンパイル時には型が完全に確定しなくて、実行時に与えれる情報を見て初めて確定するような。
#s/与えれる/与えられる/
#型に関してはないと思う。unsafeCoerceとか変なの以外は
#あ、問いの立てかたが変か。「型情報」は「実行前までに確定できる情報」なんだとすれば、by definitionでそういう計算はない。でも、少しでも多くの情報をメタの方に押し込められるように「型情報」の仕組み自体がどんどん拡張されている。そんな感じ?
#個人的な感覚では、実行時にきまるものは外界からの入力で、それ以外はすべて静的に定まるもの。「型情報」そのものは静的なものとして扱う。「型情報」の仕組みの進化は、「型」をどれだけ抽象的に扱えるかという方向に拡張されているという感じ。
#依存型みたいなものは型を拡張して少しでも実行時の情報を実行前に移す試み、と見れない?
#うーん。入力が絡めばそうみなせるけど、そうでなければbooの例と同じで最初から確定しているとも見なせますよね。
#例えばユーザ入力値がvalidateされて非負であることが確定してる、とかさ。booの例だって(define-constant x (read)) ってすればユーザ入力値になるよ。
#「入力があれば」もちろん、そうです。
#そこで入力をとりたてて区別する必要とは? Haskellが、区別した方が都合が良いって立場を取ってるから区別するってのはわかるんだけれど。
#これも個人的感覚ですが、評価すれば決まるものは静的情報で、実行しなければきまらないのが動的情報
#その感覚はわかるけれど、それ
#それは「そう決めたからそうなんだ」以上のことを言ってない気がする。
#ソースコードもユーザ入力も全部インクリメンタルに与えられる情報の一片であって、処理系がひたすらそれまでの情報を総合してpartial evaluationをやっている、というありかたもありで、本質的に優劣があるわけじゃなく、「どういう立場を取ったらどっちの方が都合が良いか」という話になりそうな。
#うーむ。そう決めた理由ということですよね。
#ごめんちょっと出かけます。
#たぶん、Haskellでは参照透明な記述を堅持するということです。
#了解
#私も出掛けます
#ユーザ入力だと話がわかりにくいけど、例えば、アプリケーションのユーザ設定ファイルなんてどうだろう。そこに書かれた式は静的情報か動的情報か、っていうのは、実行という線をどこに引こうと決めたか、って差にすぎないのでは。
#もちろん実行という線をどこに引くかという問題なんですが、私としてはプログラム（算譜）にはない情報を与えるのが実行という感覚でいます。ここに固定するのがブレがなくてよいと思います。(移動中なので、返事が中途半端にとぎれます)
#しかし、ユーザ設定ファイルの例のように「どこまでがプログラムか」という線は曖昧であって、むしろ「ここから先の情報は今はわからない」と判断した時点までの情報がプログラムである、としか定義できない。とすれば「プログラムに無い情報を与えるのが実行」というのはトートロジーになってしまう。
#プログラムの境界については，プログラムの正しさというものを考えれば自ずと境界ははっきりすると思います．特定の設定ファイルを含めて正しいといいたいのなら，設定を含めてプログラムでしょう．
#プログラムの「正しさ」の定義は? それが静的なチェックをパスすること、であればやっぱりトートロジーのような。
#正しさの定義は重要です。静的チェックを通ることが正しいというなら、静的チェックを通る条件を満たすことが正しさの条件になります。もちろん、これを正しさの必要条件になっていなければなりませんが。
#ああでも循環しているか。
#静的云々を抜きにして、プログラムの正しさというのはどのようなものと考えますか？
#それはどのように確かめられるものなんでしょうか？
#プログラムの外に何らかの制約が必要だよねぇ。プログラムは(バグも含めて)書かれた通りに動くわけだから、それが不正なプログラムであるということは、外にある基準に照らして不正だということだよなあ。
#操作的な見方としては、ある計算モデルを考えて、それに食わせた場合にモデルの状態が「正常である」と定義された状態以外を取らない、とか?
#んー、計算モデルとしてTMを考えたら、不正な状態というのはあり得ない (せいぜい止まらないのを不正とするくらい?) から、当然ここで考えてるモデルというのはより高度な、もしくは制約のきついモデルということになる。
#静的検査というのは、その高度なモデルの定義と、与えられたTMプログラムだけから、そのTMプログラムが高度なモデルの状態をはみ出ないことを調べるもの…とか? あれ、やっぱりなんだか同じところをぐるぐる回ってる気がしてきた。
#それは、表明とかの形で人間が与えてあげないといけないんじゃないでしょうか？
#その一つの方法が型宣言だよね＞表明とかの形
#はい。あとは、契約とかですかね。
#この「何に照らして正しさを考えるか」っていうモデルのところに、型システムを持ってくるのは、それが扱いやすくてかつ有効性が高いからだと思う。それはそれでいいんだけど、他の形もあり得るだろうなと妄想する。
#不変表明を書いておくと静的に解析してくれるシステムみたいなのありませんでしたっけ？
#私が学生の頃、いやもうちょっと前かな。知識処理界隈では、ある程度矛盾を許容する知識ベースの作り方ってのをやってた。エキスパートシステムとか関連なんだけど、どんどん知識を追加していった時に、矛盾を許さないと現実のデータではあんまりスケールしない (早々に破綻する)。
#人によって言うことが違いますからね(笑)。
#Lispみたいに実行と解析がぐちゃぐちゃになってて、実行イメージ中の泥団子をこねるような言語の場合、「それまでに与えられた情報」の総体が一種の知識ベースになってて、正しいモデルが何なのかなんてわからないけれど新しい定義を加えたらそれまでの知識を元に解析して、「まあいいんじゃないの」とか「これはまずくないか」みたいな答えが返ってくる、なんてのはありだろうか。
#ぼくはむしろ、これまでのことは忘れてほしいんですよね。だから、REPL で開発するのってなじめないです。
#忘れて欲しいこともあるけど。でも、デバッガっていうのは実行状態の中にいるのが基本じゃない? REPLってずっとデバッガの中にいるようなものだと思えば。
#まあでも、Common Lispで開発してて、REPLでちゃんと動いてテストも通ったのにクリーンコンパイルしたら動かなかった (実は古い定義を参照してた) なんて罠はあるからなあ。
#あーそれはそうですね。＜デバッガ
#clang で gauche build してみました。warning の出方も違いますね。
#diff --git a/ext/zlib/gauche-zlib.c b/ext/zlib/gauche-zlib.c
index 7cd8e0f..1893f3e 100644
--- a/ext/zlib/gauche-zlib.c
+++ b/ext/zlib/gauche-zlib.c
@@ -240 +240 @@ static int deflate_flusher(ScmPort *port, int cnt, int forcep)
- info->flush == Z_SYNC_FLUSH;
+ info->flush = Z_SYNC_FLUSH;
diff --git a/src/bignum.c b/src/bignum.c
index 37c167d..4055e63 100644
--- a/src/bignum.c
+++ b/src/bignum.c
@@ -432 +432 @@ double Scm_BignumToDouble(ScmBignum *b)
- && (dst[0]&1 == 1
+ && ((dst[0]&1) == 1
diff --git a/src/regexp.c b/src/regexp.c
index a899baa..311b92f 100644
--- a/src/regexp.c
+++ b/src/regexp.c
@@ -260 +260 @@ static int regexp_compare(ScmObj x, ScmObj y, int equalp)
- for (i=0; i++; i<rx->numCodes) {
+ for (i=0; i<rx->numCodes; i++) {
@@ -263 +263 @@ static int regexp_compare(ScmObj x, ScmObj y, int equalp)
- for (i=0; i++; i<rx->numSets) {
+ for (i=0; i<rx->numSets; i++) {
diff --git a/ext/net/net.c b/ext/net/net.c
index a625082..bd7b369 100644
--- a/ext/net/net.c
+++ b/ext/net/net.c
@@ -534 +534 @@ ScmObj Scm_SocketBuildMsg(ScmSockAddr *name, ScmVector *iov,
- (void*)get_message_body(SCM_CAR(SCM_CDDR(c)), &clen);
+ (void)get_message_body(SCM_CAR(SCM_CDDR(c)), &clen);#このあたりは直したほうが良さそうですかね。
#こりゃありがたい。regexpのは、つまり今までループを回ってなかったわけか。
#そういうことになりますね。他にも Scm_Init_rfc__zlib が Scm_Obj 返すことになっているとか、/* がコメントの中にあるとかいわれてます。
#/*がコメントの中に、というのは生成されたコードでですか?
#一つはこれだからそうですね。
#compile.scm:6415:118: warning: '/*' within block comment [-Wcomment]
...Scm_MakeClosure(SCM_OBJ(&scm__rc.d996[108]), NULL)); /* subst-lvars/* */
#cgenの方をいじって出ないようにしておこう
#ndbm-makedb.c:7:9: warning: '/*' within block comment [-Wcomment]
*.dir/*.pag from the original dbm, while BSD-traits uses *.db (they
#'*/' が生成されちゃうともっとまずいな
#これがもうひとつ。
#ちゃんとcgen-safe-commentって用意してあった。MakeClosureを出す部分だけ入れ忘れ。
#TMをモデルにして考えれば，初期状態がプログラムで，特定の初期状態からはじめれば，望んだ結果を表す終了状態で停止するというのが，そのプログラムの正当性ということになる．プログラムを初期状態から停止状態への関数と見なせば，その正当性は望む停止状態がでるかで決定的に判断できる．これは言語にかかわらず同じかな？とはいうものの，これは計算途中で系の外側からの影響（入力）がないという前提なので，現実的ではない．入力のがおこったときその系を観測していれば，それは予期せぬ副作用のように見える．どのような入力あるかは実行前には（値としては）確定できない．静的チェックのしようがない．逆に，入力に直接かかわらない部分については切り出せれば静的にチェックできるだろうという希望はある．
#でも入力にかかわらないのなら、はじめから定数で置き換えちゃえばいいんじゃないですかね？
#答がわかっているなら書く必要はないし、そうでなければ一度うごかせば捨てるものかもです。でも、関数適用としては一回かぎりでしょうけど、関数抽象は使いまわしが効くかもしれませんね。
#定数というのは確定済ということにすぎないので、それが関数抽象の可能性もあるということです
#関数抽象って、たとえば、静的な関数のインライン展開みたいな？
#ジャンプ先の番地とかなんでもいいとおもいます
#計算結果が関数抽象である場合、それを「使いまわす」っていうのは、将来何らかの引数にそれを適用するってことですよね。その何らかの引数って、今はまだわからない。外部入力というのも実行前には確定してないという意味で同じじゃないですか。
#あーもちろんHaskellで入力とプログラムを区別するのはわかるんだけど。Lispみたいにプログラムとデータの境界が曖昧な立場では、「プログラムが動作して入力を受け取る」のと、「途中でプログラムが追加されて全体が再構成される」のは外部から観測していて同じじゃないか、とも言えるので。
#これはどちらが正しいかというのではなく、どう見ると都合が良いかという違いだと思いますが。
#プログラムを入力としてみとめるなら、ここでは、そのプログラムを処理・実行するメタプログラムみたいなものを問題にしないといけないんじゃないでしょうか？ ただ、Lisp の場合は、そのメタプログラムも通常のプログラムと見分けがつかないので、話がややこしくなるんだと思うんですが。
#なので、入力、それを処理するプログラム、入力としてのプログラム、プログラムを入力としてとるメタプログラム、みたいなそれぞれのレイヤーに対して個別になら、ある程度の正しさのチェックはできそうな気がします。
#そうそう。そこで、メタプログラムとプログラムをはっきりわけるかわけないかって話になるんだけれど、その分類は単に「都合がよい」からそうしているだけなんではないか、ということです。
#そんで、きっちり分けて分け方を工夫すれば個別のレイヤに閉じた中で言えることは増えるんだけど、分けないという立場をとると実行時に情報がわかればわかるほどさらに言えることが増える、とも考えられます。
#はい、同意です > 「都合がよい」からそうしているだけ
#これも同意 > 実行時に情報がわかればわかるほど言えることが増える
#ただ、実行時の情報をどう使うかという情報は、やっぱり実行前に組みこまれていて、情報について実行まえになんらかの判断ができるといいだろうなぁ。と思うのでした。
#もちろん、言語の性格上、実行時前の情報では有用な判断はできないということがあるでしょう。Haskellでは静的型付けと参照透明な記述と非正格な意味とを確保することで実行前に判断できることを増やしていると見ることができます。
#Haskellの選択が実行前にチェックできることをなるべく増やすものだって点には異存はないんですが、それによって「プログラムの正しさ」がどれだけ検証できるかというと、結局は「与えられた情報の中では矛盾はない」というところまでしか言えない。「与えられた情報の中で矛盾が無い」ことを「正しい」のだ、と言ってしまうと定義が循環しちゃう。なので正しさについては別途議論が必要、って感じかな。
#仕様記述言語とかの話につながるんですかね。人間の意図をいかにしてプログラムと結びつけるかですよね。
#たしかに「正しさ」を曖昧にしか考えてませんでした。> shiro
Gauche > Archives > 2010/07/02