2008-05-01 [長年日記]
λ. 久しぶりのSFC
SFCで「現代のチベット情勢(仮)」と題した講演が行われるそうなので、聞きに行ってきた。その後、学食でご飯を食べたり、κ208でジャンプを読んだり、向井研と萩野・服部研に顔を出したり、ロフトで色々な人に会ったり。
写真は、メディアセンター裏の木と、鴨池。 2月に来たときは寒々しかったけど、もうすっかり新緑の季節。 ずっと見てたときは意識しなかったけど、たまに来ると季節の変化にはっとさせられる。
そういえば、去年もゴールデンウィークにはSFCに来たなぁ。
λ. 現代のチベット情勢
SFC CLIP: 聞けばみえてくるチベットの真実 で、ダライ・ラマ法王庁アジア太平洋地区代表として活動してきたペマ・ギャルポ(Pema Gyalpo)氏の公演があると知り、聞きに来てみた。 寝坊してちょっと遅刻して行ったら、ちょうどペマ・ギャルポ氏の紹介が終わるところだった。
最近、チベットについては大きな話題となっているが、私はチベットの歴史を近現代についてさえよく知らなかったので、興味深かった。次は中国側の人の話も聞いてみたいところ。
撮影していたので、後でSFC-GCで公開されるのかな。されるといいな。
参考
- ペマ・ギャルポ氏
- ダライ・ラマ法王日本代表部事務所
関連
メモ
以下はメモ。 不完全かつ私の誤解も多いと思うので注意。
はじめに
世界地図も私たちの顔と同じように変わってきているが、毎日見ていると変わっていないように思ってしまう。1950年まではチベットという国があったが、現在は中国の自治区。「〜族自治区」「自治州」などは、本来は中国人の領土ではない。
近代国家が地図上に線を引いているのは、人類の歴史の中では短い期間であり、それ以前は山や川、共通の宗教と文化によるアイデンティティによって国々は分かれていた。
中国はチベット人を「蔵族(ぞうぞく)」と呼んでいる。 そして、チベット人が住んでいる本来のチベットの領土は、全部今でも一応「蔵族自治県」「蔵族自治州」「蔵族自治区」などと呼んでいる。 それで、中華人民共和国について地図をなぞっていただけると、大体現在の中華人民共和国の1/4のチベットで約230万平方キロメートル。
その中で、私が生まれたのは現在は四川省に入っているヤロン(?)というところ。 子供のときの私の名前は「シェド(?)」で、名前を意識するころにはすでに中国の人がいた。 私の村では金が取れ、中国は許可を取って入ってきていた。
今回の抗議行動
今回3/10にラサから始まったもの。 ある人は「暴動」と呼び、私たちは「決起」と呼んでいる。立場によって違うと思う。 それが、今回の場合には日本の新聞などによるとチベット以外の四川省、雲南省、甘粛省や青海省などに波及している。 しかし、チベット人が四川省や雲南省や青海省に行っているのではない。 あくまでも、本来チベットの領土であったところのチベット人が、全土において約50箇所において抗議・デモなどが行われたということ。
昨日もらったある手紙によると、現在も戒厳令のような形で軍が完全に監視していて、県から県へと移動することもできない。 また、今は食料が足らず、捕まった人たちや怪我した人たちには薬が与えられていない。
それから、中国では未だに国民一人ひとりの通信(メールも含めて)を、国家が検閲しているというのが今の状況。 それは、チベット人だけではなく、中国の人たちに対しても同様のことを、中華人民共和国という国はやっている。
2001年に中国が初めてオリンピックの開催に立候補したときは、中国は「それまでの天安門事件による悪い印象を良くしたい」「2008年までにはいかに発展しているか、人権などの点でも進歩していることを示したい」といって立候補した。 私たちもそれには賛成だったし、そうすれば中国が世界に対して誇れる国、経済大国になるだけではなくて、世界の常識が通用するような国になるのではないかと期待していた。
しかし、今オリンピックまであと100日以内に入り、焦った中国はチベット人も中国人もどんどん捕まえて刑務所にいれている。 かつてヒトラーは1200万人殺したということで悪人として扱われているが、毛沢東は8000万人殺した。 もし、その前で世界の人たち、指導者たちがまじめな顔をして、そして世界の選手たちが、健全な精神の宿る健全な肉体を披露するために毛沢東の肖像画の前で行進したら、これはお笑いものだと思う。
そういう意味で、今回チベットのお坊さんたちは特に10月と3月10日にデモをやった。 でも、デモそのものは1959年から49年間毎年、世界のどこかで国内外でやっている。 そして、今年は残念ながら、チベット人そして中国の一般の方が犠牲になってしまった。
チベット支配の歴史
中華人民共和国は1949年に成立し、1950年にチベットなどに侵攻。 「わが祖国の正当な領土を取り戻す」が大義名分で、「正当な領土」とは宗主権のあった場所を全てを含む。沖縄もそう。 「チベットから帝国主義者を追い出す」がもう一つの大義名分。 しかし、チベット全土でたった5名しか白人はおらず、その人たちも50年の時にはもういなかった。 にも関わらず、「帝国主義者からチベットを守るために開放する」と。
やがて、チベットは最初はインドとネパールと近隣諸国に助けを求めた。ロンドンにも。 なぜならばそれらの国々とは条約があった。 英国との条約は独立したインドが提唱していた。 現にチベットには、中国の駐在員、インドの駐在員、英国の駐在員、今日でいったら各国の外交部の事務所があった。 なので、チベットは周囲の国に助けを求めたが、インドは独立したばかりで他国を助けるだけの余裕がなく、ネパールもモンゴルも弱いという状況で、結局助けることはできなかった。
国連は最初チベット問題をアメリカなどで扱おうとしたが、これに対してはインドは「これはアジアの問題」と主張。 ネールとしては平和五原則(Pancha Sila)に基づき、(ロシアと米国の二極の冷戦構造の中で)第三の勢力として中国・インド・インドネシアなどで「アジアの問題はアジアで解決する」ことを求め、中国に対して説得する側に立った。
それで条約(十七か条協定)を結んだ。 条約は本来は対等平等の精神にたってお互いの同意によって成り立つものだが、この条約は印鑑までが用意されていて半強制的に結ばされた。 しかし、一応当時のチベットは国際社会に異を唱えなかったし、その後1957年にダライ・ラマ法王がインドに行ったときも無効とは主張しなかった、1954年に中国に行き全人大会に出て新しい憲法を作ることにも参加した。 1951年から1959年まではこの条約に基づいて一応共存していた。
共存して一生懸命努力して一緒にやろうとしていたが、1956年ごろから中国は宗教弾圧を始めた。 言い分は「チベットは封建社会がまだ残っていて、農奴がいる」「チベットの封建社会から開放する」で、チベット国内でいわゆる人民裁判が始まった。 対象は旧官僚、貴族、僧侶、地主。 共産主義の理論における階級闘争。 その中では、例えば「宗教はアヘン」であり、「お祈りをして、お布施を頂いて生活しているお坊さんは非生産的集団」であり、そういう人たちを排除するというのが中国共産党の最初の言い分。 チベット各地で人民裁判のようなものが起き、階級闘争を強制された。
その中において、高僧や有力者を当局に招いては帰さない、ということが頻繁に起こった。 そして、1959年3月10日になって、ダライ・ラマ法王に護衛なしで解放軍の駐屯地へという招待状が。 法王が二度と帰ってこないことを恐れた民衆が立ち上がった(1959年のチベット蜂起)。 小競り合いになり、一人のチベット人で当時中国と比較的仲がよく通訳などをやっていた人が、チベット人から裏切り者だとされ、最終的には群集がその人を殺害してしまったのだったと思う。 今度は中国軍がダライ・ラマ法王の夏の宮殿に向かって大砲を撃つというようなことがあった。 以来この3月10日を「スンチュ」と呼んでいる。 「スン」は3、「チュ」は10で、「チェン」は「大きな日」「記念日」なので、「スンチュチェン」としてそれ以来やっている(チベット民族蜂起記念日?)。
1959年、1961-1963、国連はチベット問題を取り上げた。 国連に取り上げるにはスポンサーの国が必要で、マレーシア(当時はマレー連邦)や北アイルランドらがスポンサーとしてチベット問題を取り上げた(アイルランド及びマラヤ共同決議案など?)。 国連は中国に対して即時撤退と平和を取り戻すことなどを勧告したが、中華人民共和国はまだ数少ない国としか国交を結んでおらず、国連にも入っていなかった。
私は12,3歳くらいのときにインドの難民学校から英国系の学校に行って、そのときインドの『New Leaders of India (インドの新しい指導者たち)』というシリーズの本を読み、そこではガンジーもネールもみんな法律家になって日本と戦っていた。 私も日本へ来て法律家になって国連で中国と戦おうと思った。 それで日本に来て法学の勉強をしたのだけど、そのときは毎晩・毎朝、中華人民共和国が国連にはいるようにと祈っていた。 なぜなら、中華人民共和国が国連に入ったら、もしかしたら国連の決議・そして国際司法委員会(国際司法裁判所?)の決議に……
もちろん、国際司法委員会は世界の裁判所でなければ、なんの罰則もない ただ世界の有名な法律家たちが自分たちの法的な知識に基づいて何が正しいか、何が正しくないか、について判断を下すというだけ。 この国際司法委員会は「チベットにおいて計画的、組織的大虐殺が行われた」とはっきり判決を下した。 もちろん、一方的にやってはいけないので、中国大使館に対しても弁論の機会を与えるためにお招きしたが、内政干渉だとして中国側は参加しなかった。
それから、1979年まで中国側とチベット側の間の接触がなかった。 その間、長い間ゲリラ戦もあり、1972年までゲリラ戦が続いた。 一方、中国においては1967年から1977年まではいわゆる文化大革命を行っていた。 その間、お互いに特に中国からは情報はほとんど入ってこなかった。
1979年に鄧小平が三度目の復活、「この問題について話し合う用意がある」ということになり、ダライ・ラマ法王の兄と鄧小平とが会った。 鄧小平はチベット問題について「独立という言葉はだめだが、独立以外は何でも話し合う用意がある」といって、それで私も第二回目の代表団の一員として三ヶ月間行ってきた。
私たち第二段の代表団の目的は、自分たちの領土の境を確認すること。 そのときにびっくりしたことは、それまで6700-7000くらいあった寺があったが、三ヶ月歩いて(車もあったけど)、完璧に残っているのは1つもなかった。 かろうじて残っていたのが8つだけ。 お寺は全部破壊されていた。お坊さんも沢山強制労働所に送られて死んだ。 その時点では中国の指導者たちは、北京で私たちが文句を言うと「全部四人組がやった」と言い訳。 我々は四人組ではなくもっと早くからやっていたことを知っていたが、やったこと自体を認めるならば良いと思っていた。 しかし、最近になって中国はそれも認めなくなった。
1980年の5月から7月まで。三ヶ月掛けてチベット全土をまわった。 そのとき、私たちが成都に着いたころ、胡耀邦という新しい総書記がチベットに行き、「チベットの生活は1959年よりも貧しい。チベットの人たちには大変申し訳なかった」「向こう3年間税金を取らない」「80%の中国人を引き上げる」と発言。 また、チベット人はチベットの意味ある名前を持つことは禁止されていて、もちろん道路の標識なども中国語だけだった。 本来、自治に関する(特に社会主義インターなども含めての)考え方の中では、そこの住民が多数を示さなくてはならなず、そこの言葉を尊重しなくてはならない。 それで、胡耀邦はチベット語を教えることを許した。 チベット人は「罪を憎んで人を憎まず」と考えていて、あくまで中国が政策を変えてくれればいいと思っていたので、胡耀邦さんは勇気のある素晴らしい人だと思った。 しかし、「チベットに対して勝手に譲歩したこと」と「中曽根首相との青年交流事業を党の機関を通さずに決めてしまった」こと等でで失脚してしまった。
ずっと、その後も話し合いをして、中国の副首相クラスの人と会った。 「これから中国は変わる。良くなる」。 で、新しい憲法を作ると。 ちなみに、中国の憲法はだいたい大会がある度に変わっている。日本みたいに世界一古い憲法、50年間変わらない憲法を持っている国はなかなかない。 で、私も「もしかしたら」と思って、連邦制のための憲法を研究。 アメリカに初めて留学して博士号をとった中国人の王さんのような人とも交流した。 いい方向を見出せないかと色々やっていた。
ところが、1987年1988年くらいになると、また態度が変わって強気に。 それまで言っていた独立以外の方法、例えば連邦政府などについても、祖国を分離することでとんでもないというようになった。
1989年の3月に大規模なデモがあった。 このときに胡錦濤さんがチベットの第一書記。 中国では、総理大臣がそのまま行政をできるわけではなく、あくまで「党の指導のもと行う」。 ですから、中華人民共和国の13億人の人は、私達がやっているように自由意志で選挙に出たこともなければ、投票したこともない。 あらかじめ党が根回しして、○×式で選ばれるようなもの。 胡錦濤さんが日中友好青年団の団長としてとして来日したときには、私もニューオータニのバーで二時間、夜中の二時まで話をした。
しかし、彼が総督のような立場の第一書記として、「無慈悲・無差別」という言葉を使って、デモ隊を撃つ事を許した。 そのときは、中国側は数百人の犠牲者と発表しているが、チベット側は数千人の犠牲者と発表している。 いつも中国政府の発表する数とは数が違ってくる。 しかし、真実は隠しきれないないと思う。
そのときの6月4日に今度は天安門事件が起こった。 天安門事件では何が起こったかは皆さんご存知のとおり。
色々
時々、海外でこういった形で勉強会にでると、中国からの留学生から「中国は昔から中国領だった」「ダライ・ラマという名前は中国の皇帝がつけた」という声が出る。 しかし、「ダライ」はモンゴル語であって中国語ではない。モンゴルが中国を侵略して王朝を作った。
残念ながら、現在の中華人民共和国には真実の記録としての歴史は存在せず、あくまでも作文として、当局にとって都合のよいことしか記録しない歴史が存在するだけ。 その良い証拠は、わずか2,30年前に起きた天安門事件について、今中国のどれだけの人が真実を知っているのか、また真実を喋れるのか。 100年200年前の真実はともかくとして、つい最近の真実をどれだけ知っているのか。
残念ながら、現在はチベットだけでなく、中国の13億人の人は皆ある意味犠牲者だと思っている。
それで、ダライ・ラマ法王は鄧小平との約束通り独立は求めず、真の自治、高度な自治を求めている。 もちろん、それに反対する人もいる。 私も、法王の意思に最終的には従うと思うが、100%賛成なわけではない。 なぜかというと、現在の中国の憲法のもとでは、今までの中国の体制のもとでの体験からすると、真の自治などということはあり得ない。 真の自治を獲得するためには、中華人民共和国が完全な民主国家として存在しない限り、多分自治というのは名ばかりで何の意味もない。今と同じ。 ボトルのラベルだけ美味しいワインに変えても、中が毒水だったら、意味がない。
チベットの人がやろうとしていることは、チベット人と中国人の対立ではなく、政治のあり方。 例えば「民族自決権」というと中国の指導者は身構えてしまう。 しかし、例えばEUを見ると独立国家が共通する利益を求めて連合体を作っている。 また、アメリカ合衆国、オーストラリア、カナダ、インド、みな連邦制でやっている。 民族自決だからといって、すぐ離れていくとは限らず、良い政策があれば共にやっていける。
私が思うには、もし誰かが隣の綺麗な女の子に恋をしたら、その人を強姦して、しかも「解放」という名のもとに「気持ちよかっただろう」というようなことを言うのはやめたほうが良い。 むしろ、お互いに愛し合えるかどうか。 お互いが幸せになるためにどういう家庭を作るか。 一緒に夢を語って、そしてお互いに愛し合えるように結婚するというのが大切。
そういう意味で、私達が申し上げているのは、中国そのものにおいて、世界の1/6の人たちが、自分の意思で読みたい本が読める、自分の考えが表現できること。 当然、そのなかでチベット人にはチベット人の価値観、モノの順位がある。 ある人は辛いものが好き、ある人は甘いものが好き。 チベット人にはチベット人の価値観がある。 例えば、チベット人が一生のうちにやりたいことの一つは、東の果てから西の果てまで五体投地して歩くこと。 それがチベット人にとっての幸せの一つ。 それを誰かが「間違っている」といっても、それはあまり意味がない。 もし間違っているならば、正しいことを示せばいい。
最初にインドの難民学校に行った時、学校の先生が髪の毛を切れといった。 チベット人は本来はお相撲さんみたいに男も女も髪を長く伸ばす。 「衛生的に良くないから」といわれたが、学校をやめても切りたくないと思った。 疱瘡にかかって隔離され、結局切って、DDTをかけられた。 けれど、一回切ったからといって、男でなくなったわけでもなく、それもなかなか気持ちよかったので、それから伸ばしたことはない。
また、いつの間にか私達はネクタイをするようになった。 背広の何分の一の値段で買うべきとか色々言われる。 あるとき、弟にグッチのネクタイを贈ったことがある。 弟はそれを壁にかけて、いつか大事なときに使おうと思っていた。 気がついたら、母が物を縛るのに使ってた。 「誰も使っていなかった。ものは使われていきてくる」
私達は人はそうやって価値観を学んでいく。 押し付けなくても、みながやっていて良いと思えば、自分もやるようになる。 良い模範を示してくれれば。
(色々省略)
今世界中が、現段階までで人類が知恵を絞ったより多くの人たちを幸せにするための制度は民主主義。 完璧ではないから、より良いものを作ろうと努力する。 が、現段階では少なくとも多くの人たちにとって、個人には人権が、民族には民族自治権があり、それを尊重することは大事なこと。 しかも、チベット人の人権、モンゴル人の人権、中国人の人権は、決して日本人の人権と無関係ではないと思う。 なぜならば、人権を普遍的な価値として共有するのであれば……、チベット人、日本人、モンゴル人、白人、中国人、形容詞をとればみんな「人間」。
最近、日本では SAVE TIBET というホームページがあってデモ等をやっているが、SAVE という言葉はあまり好きではない。 まず第一にチベット人自身がしっかりしなくてはいけない。 そして、それを助けて欲しい。 「人を救済する」ということは、中国の「解放する」に似たようなところがある。
さっきは中国に指を差してきたが、3本の指は自分たちを指している。 チベット人自身がもっとしっかりしていれば、そう簡単に侵略などは許さなかっただろう。
チベットに関する誤った情報など
「チベットの農奴を解放した」というが、チベットはだいたい騎馬民族で遊牧民が多い。 ラサ周辺には小作農もいたけれども、「農奴」という言葉は中国の偉い人が考えて作った言葉。
「チベットの人は2%しか文字を読めなかった」というが、1940年にアジアで文字を読めた人がどれだけいたか? むしろチベットは文明国家だった。というのも、(中国のいう非生産的人口の)お坊さんはみなお経を、つまり字を読め、男性の人口の2〜3割がお坊さんだった。 これもプロパガンダとして誰かが作文した言葉に過ぎず、現実ではない。
チベットの迷信というが、当時の他の地域に比べて劣っていたわけではない。
「チベットの平均寿命は38歳だった」というが、当時の中国の平均寿命は? また、どのような統計に基づくのか? 当時のチベット人は自分の村のことすら良く分かっておらず、また統計をとるという発想すらなかった。
学問をする上では疑いの気持ちは大事だし、今日私が話したことについても疑いの気持ちをもって自分で調べて欲しい。
質疑応答
- 質問
-
「罪を憎んで人を憎まず」という言葉に共感を受けた。
週末に長野に行き、またネット上で中国人留学生などに対する心無い言動や行動を目にした。チベットの旗を掲げて、人を憎むような行動をとっている人がいるということは、ペマ先生自身も本意ではないと思うが、それについてどう思うか?
また、チベットの方でも、チベット側の人も、そういったことが起こらないように積極的に呼びかけなどを行っていくべきではないかと思うが、どう考えているか?
- 回答
-
チベット問題はかつての拉致問題と同じくらい日本で関心の高い問題になったので、色々なグループが色々な思惑をもって、便乗してくると思う。 私にはそれを止めるような力はないが、今の中国の若い世代には何の罪もないことは間違いない。
むしろ、留学生たちに優しくすることが、日本の外交・防衛にも繋がるのではないか。教科書などで教えられた日本人と違うことを見せることが大事。
一方、留学生の側も挑戦的なことをしていたと聞いている。 それは(学問が第一である)留学生としての身分をわきまえるべきだと思うし、言動にはもう少し注意すべきだ。 お客さん(留学生)を迎えるホストの側の礼節も大事だが、土足であがってくる事も正しくないし、お互いに礼儀を守ることが大切。
- 質問 (続き)
- あちらがやればこちらもやっていいという議論は成り立ちませんよね?
- 回答
-
それはもちろん成り立たない。どっちかが我慢するしかない。 チベットの人たちには「たとえ手を出されても手は出すな」と言っている。「右の頬を打たれたら、左の頬も差し出せ」というのは正直言って難しいが、それをやはり目標にしないければならないと思う。
残念ながら、今何世代もお互いに憎しみあっている民族もいるが、チベットとは例えば明の時代、元の時代、清の時代、お互いに仲良くやってきた実績がある。それができないことはないと思う。
- 質問
- 今のチベットの亡命政府が独立するつもりがなくて、自分の文化や習慣などを尊重して欲しいというだけなのかを確認したい。
- 回答
- 亡命政府の考えとしてはその通り。ただ、チベットの中でもダライ・ラマ法王と同じ考えを持たない人も多いことは事実。その理由は、私達人間の関係、信頼関係は、行いによってのみ変わるから. 今まで中国政府は約束事を守ってきていない。 だから、何よりもまずお互いに信頼関係を作ることが大事。
- 質問
- 今回の事件はたまたまオリンピックと結びついたのか、それともオリンピックを利用したのか?
- 回答
-
北京政府もチベット側もオリンピックを利用していると、個人的には思う。
オリンピックは世界中が注目しているからこそ、北京政府も例えば聖火リレーをわざわざチベットからはじめて、マスコットにチベットの動物を使うと、こういうことは中国としては世界に対してアピールするために当然やっていると思う。
一方、チベットの人たちも、こういうときに世界の注目を浴びられるから、それに反対するという立場でインドから101人が行進した。これは、かつてマハトマ・ガンジーが塩をとるために(塩の行進)、それからキング牧師は黒人の公民権のために行進をやったことの真似て、オリンピックにあわせてやったもの。
双方ともにオリンピックを意識していること、これは間違いない。
- 質問
- 中国も対話に応じるなど変わってきているのでは?
- 回答
-
対話についてはあまり期待していない。 おそらく、胡錦濤さんが来日するときに、世界中のマスコミからチベット問題について非難されると困るので、我々と話をしますというだけのジェスチャーではないか。
本格的に話をするためには、まずチベット人の捕まっている人たちに治療を受けさせるとか釈放するとか、それから中国人も今回、例えばそのチベットに対して支援した良心的な人々も捕まっているが、そういった人々も釈放して、それから対話をすることが本当の対話だと思う。 だけど、今のところは世界の世論をかわすための単なる口実としての対話ではないか。
ただ、それと同時にそうでない良い方向に行って欲しいという気持ちもある。
- 質問
- 現在のチベット自治区で、本当に自治が可能になったとき、一番最初に着手すべきと考えている政策があったら教えて欲しい。
- 回答
-
人間は食べること、着ること、寝ること、これが多分幸せの最低条件。その他に何があるかというと、意識していないけど、息をすること。息をするためにはいい環境が必要。
チベット全土において、それぞれの価値観に基づいて生きる権利を獲得することが、本当においしい空気を吸えることだと思う。それが最初の条件。 人間らしく暮らすための環境をまず取り戻したい。
λ. 今日の向井研メモ
今は、Short Introduction to Modal Logic (Center for the Study of Language and Information Publication Lecture Notes)(Grigori Mints) をやっているらしい。
Prologの導入として、意味木(semantic tree)というのを用いる方法があるとかで、この本はそれにも関係するケーニッヒの補題(König's lemma)に拘りのある本らしい。あと、monadic logic は良い性質を持っているとか。
2008-05-03 憲法記念日 [長年日記]
λ. monadic logic
Monadic Logic で検索して <URL:http://www.cs.tau.ac.il/~rabinoa/logic6-1-04.pdf> というスライドを発見。 monadic logic の satisfiability が decidable であることの証明と、あと指標 {<, =} からなる有理数上の論理式がdecidableであることの証明が面白かった。
2008-05-05 こどもの日 [長年日記]
2008-05-06 [長年日記]
λ. PEGにマッチする文字列をAlloyで生成する
この間の正規表現にマッチする文字列をAlloyで生成すると同様のことを今度はPEG(解析表現文法)に対して行う。文字列の表現などは前回と同じ。
単純化するために、e* と e+ の e が非終端記号Nになるように文法があらかじめ変形されているものとする。
式に対する解釈は大体以下のような感じ。
- [[ ε ]](x,y) = (x==y)
- [[ c ]](x,y) = (x.tail==y && x.head==c)
- [[ N ]](x,y) = y in x.N
- [[ e1 e2 ]](x,y) = some z : String | [[ e1 ]](x,z) && [[ e2 ]](z,y)
- [[ e1 / e2 ]](x,y) = [[ e1 ]](x,y) || ((no z : x.*tail | [[ e1 ]](x,z)) && [[ e2 ]](x,y))
- [[ N* ]](x,y) = y in x.*N && (no z : y.^tail | z in y.N)
- [[ N+ ]](x,y) = y in x.^N && (no z : y.^tail | z in y.N)
- [[ e? ]](x,y) = [[ e / ε ]](x,y)
- [[ &e ]](x,y) = x==y && (some z : String | [[ e ]](x,z))
- [[ !e ]](x,y) = x==y && (no z : String | [[ e ]](x,z))
その上で解析規則の集合
N1 ← e1 … Nn ← en
を
pred Rules(N1, …, Nn : String -> String) all x, y : String { y in x.N1 <=> [[ e1 ]](x,y) … y in x.Nn <=> [[ en ]](x,y) } }
として不動点を表す述語にする。 (これだと最小不動点であることは表せていないけど、Alloyでは最小性を直接記述できないので、とりあえずその辺りは気にしないことにする)
で、Niにマッチする文字列を適当に生成するには以下のようにする。
pred test() { some N1,…,Nn : String -> String { Rules[N1,…,Nn] some x : String | Nil in x.Ni } } run test for 10
具体例: A ← a A a / a
-- A <- a A a / a pred Rules(A : String -> String) { all x, y : String { y in x.A <=> (p[A,x,y] || q[A,x,y]) } } pred p(A : String -> String, x, y : String) { some z, w : String { x.head==C_a x.tail==z w in z.A w.head==C_a w.tail==y } } pred q(A : String -> String, x, y : String) { all z : String | !p[A,x,z] x.head==C_a x.tail==y } pred test() { some A : String -> String { Rules[A] some x : String { Nil in x.A all y : String | y in x.*tail } } } run test for 10 assert no_a5 { all A : String -> String | Rules[A] => no x0 : String { let x1 = x0.tail | let x2 = x1.tail | let x3 = x2.tail | let x4 = x3.tail | let x5 = x4.tail { x0.head==C_a x1.head==C_a x2.head==C_a x3.head==C_a x4.head==C_a x5==Nil Nil in x0.A } } } check no_a5 for 10 assert uniq_A { all A1, A2 : String -> String { Rules[A1] && Rules[A2] => A1==A2 } } check uniq_A for 10
実行例
Alloy Analyzer で「Run test for 10」を実行すると、「a」「aaa」「aaaaaaa」といった文字列を表すモデルが生成される。 例えば、「aaa」の場合にはこんな感じ。
これを見ると二文字目と三文字目のaがAにマッチしているのに対して、一文字目のaはマッチしていないことがわかったりとかする。
一方、他のモデルの探索を繰り返しても「aaaaa」を表すようなモデルは生成されない。 そこで、「Check no_a5 for 10」を実行すると、「No counterexample found」となり、そのようなモデルが(多分)存在しないことが示せる。
関連
2008-05-08 [長年日記]
λ. ディスプレイ壊れた
急にデスクトップマシンのディスプレイが壊れた。 電源を入れると映るのだが数秒でフェードアウトして映らなくなる。 落ち込んでるときに嫌なことが重なるものだな……orz
ちなみに、使っていたのは、20030220#p01に買ったSotecのPC STATION SX6130Cとセットだったディスプレイで、MAG Innovision の Product No. MAG565 の Model No. 568 とかいうやつ。
2008-05-10 [長年日記]
λ. Scala勉強会@関東-1
水島さん企画のScala勉強会に参加。 企画の存在は覚えていたのだけど、参加表明が必要なことを見落としていることに前日気づく。結局、キャンセルがあったため参加することが出来た。
水島さんの発表「Scalaチュートリアル」が発表40分なのに、皆がツッコミを入れまくって2時間以上になっていてウケた。水島さん独演ショー。 水島さんの発表ではScalaがいかに節操のない言語*1かを理解することが出来、soutaroさんの発表では逆に型システムがきちんと考えられていることを窺うことが出来、興味深かった。 最近ちょっとJavaを使っていて、「これはダル過ぎる」と思っていたところなので、Scalaは使ってみたいなぁ。
帰りの電車で、宮本さんのA Scala Tutorial for Java programmers(和訳,PDF)を読んだ。
関連リンク
メモ
「/」が foldl とか、「これは酷い」と思ったw
「_+_」といった書き方はOBJ系の言語や、Agda2でも採用されている(Agda2 - ヒビルテ (2007-12-01))ので違和感なし。
……と思ったが、OBJ系言語やAgda2のやつが演算子を関数として扱うための記法なのに対して、Scalaのは任意の式に穴を空けられるのか。 そうすると、例えば _+_.toInt は ((x, y) => x+y).toInt ではなく (x, y) => x+y.toInt と解釈されるが、ラムダ式のボディになる範囲はどうやって決まるのだろうか? 「違和感なし」と書いたけど、前言撤回。やっぱり気持ち悪いかも。
「var z :Array[T] forSome { type T } = x」のとき、z(0) の型は T for Some { type T } ではなく、AnyRef になる。
水島さんのtwitterで取り上げられている implicit parameter の話は、Agda1だとimplicitな引数を明示的に与えるときには、通常の関数適用の f x とは別の f |x という記法を使うことで曖昧性を無くしていたので、Scalaだとどうしてるのかなと思って聞いてみたのでした。
- <URL:http://twitter.com/kmizu/statuses/808199043>
- <URL:http://twitter.com/kmizu/statuses/808199622>
- <URL:http://twitter.com/kmizu/statuses/808200187>
- <URL:http://twitter.com/kmizu/statuses/808200567>
implicit parameter を使った Poor Man's Type Classes 。 そういえば、Agda1での型クラスの実装も内部的にはimplicit parameterを使う形になっていた(“Overloading in Agda” by Catarina Coquand - ヒビルテ (2005-10-03))。
A Nominal Theory of Objects with Dependent Types
*1 ところで、この雰囲気はMerdを思い出すんだよなぁ。
λ. RubyKaigi2008と懇親会のチケットを購入
2008-05-11 [長年日記]
λ. 第四十回圏論勉強会
今日は圏論勉強会。 『The Haskell Programmer's Guide to the IO Monad ― Don't Panic』を読む四回目で、Section 6.3 “An alternative definition of the monad”から最後まで。 モナドの代替的な定義としての Kleisli Triple と Haskellの定義での定義、それらの等しさ。IOモナドの説明。 次回から何をやるかは未定。
母の日ということで、帰りにシュークリームを買って帰った。 クッキーっぽいやつと、五月限定のさくらんぼのやつ。
関連
λ. 新ディスプレイ
ディスプレイが壊れたので、新しいディスプレイを買ってみた。 ディスプレイのことなど何も分からないので、適当に安めだったiiyamaの20インチのやつに。¥24,800
これまでのに比べると画面が広くて綺麗だなぁ。弾幕が映える(ぉ
2008-05-12 [長年日記]
λ. 『Cygwinで日本語TeX』 by 黒木裕介
を読む。 黒木さんの作っているCygwin向けの日本語TeXパッケージの開発についてで、スクリーンショット一つとってもちゃんと考えて用意してあったのかと感心。
ちなみに、最近新しいWindowsマシンにTeXを入れるときは、いつも黒木さんのパッケージのお世話になってます。いつもありがとうございます。
2008-05-16 [長年日記]
λ. 相棒 ―劇場版―
帰りに映画館によってみた。 時間通りに行ったら20分ぐらい予告編で辟易。 内容は、どうにも犯人側の行動や戦略に合理性と一貫性が欠落しているように思えて、あまり納得のいかない終わり方だった。 本仮屋ユイカはかわいかたけど。
2008-05-22 [長年日記]
λ. オープン・スペース 2008
ちょっと用事があって東京の方まで来たので、帰りに新宿初台の ICC の オープン・スペース 2008 によってきた。目当ては佐藤雅彦+桐山孝司《計算の庭》*1。
《計算の庭》は、数字の書かれたRFIDタグ内蔵カードを持って庭の中に入り、計算式を表すゲートを通過するごとに自動的に行なわれる演算によって、数字を「73」にすることを目指すもの。 やってみたら、私の結果はこんな感じになった。
適当に手にしたカードは36で、適当に近くにあったゲートを通ったら、それが「×7」のゲートで、数字が結構大きくなってしまった。ので、「こりゃ面倒かなぁ」と思ったのだけど、そこからは案外すぐに終わってしまった。 色々と試行錯誤するのが楽しそうなので、そういう意味ではちょっと物足りなかったけど、面白かった。
他には、グレゴリー・バーサミアン《ジャグラー》*2やカールステン・ニコライ《invertone》は感覚に直接働きかけてきて、すごく刺激的。ちょっと酔いそうだけど。 それから、三上晴子+市川創太《gravicells[グラヴィセルズ]−重力と抵抗》 や インタラクティヴ年表 2008 は単純だけど良かった。
どの展示も普段使わない感覚を刺激される感じで、すごく刺激になる。 しかし、こういうのを設計するデザイナにはどんな世界が見えているんだろうね。僕らとは全く違う世界が見えているとしか思えん。
ψ 石川将也 [でもこの解答、短くていいですね。36の最短経路じゃないかな?]
2008-05-24 [長年日記]
λ. “Optimistic evaluation: an adaptive evaluation strategy for non-strict programs” by Robert Ennals and Simon Peyton Jones
Lazy programs are beautiful, but they are slow because they build many thunks. Simple measurements show that most of these thunks are unnecessary: they are in fact always evaluated, or are always cheap. In this paper we describe Optimistic Evaluation ― an evaluation strategy that exploits this observation. Optimistic Evaluation complements compile‐time analyses with run‐time experiments: it evaluates a thunk speculatively, but has an abortion mechanism to back out if it makes a bad choice. A run‐time adaption mechanism records expressions found to be unsuitable for speculative evaluation, and arranges for them to be evaluated more lazily in the future.We have implemented optimistic evaluation in the Glasgow Haskell Compiler. The results are encouraging: many programs speed up significantly (5–25%), some improve dramatically, and none go more than 15% slower.
を読んだ。
先行評価を組み合わせることで遅延評価の非効率性を避ける試みで、Eager Haskell (c.f. 20070706#p01) と同様だが、独立に行われたもの。
Eager Hasekll は常に投機的に実行することを試みていたのに対して、こいつはプロファイラを持っていて、投機的に実行した結果が無駄になっている比率が高い場合には、そのletに関しては遅延評価に戻すようになっている。
個人的に面白かったのは、chunky evaluation の実現方法に関しての、「The intuition is that the deeper the speculation stack, the less likely a new speculation is to be useful」という洞察。それから、「let x = (let y = <expensive> in y+1) in ...」という式があったときに、<expensive>を投機的に実行するコストを、yではなくxに帰する方法。
2008-05-28 [長年日記]
λ. 携帯で動画を見てみる
最近、iPod を買いかえようか悩んでいるのだけど、理由の一つは動画再生機能なので、携帯電話で動画が見れればまだ当面は買い換えずに済みそうかと思い、試してみた。
携帯電話で再生可能な形式はかなり特殊な形式のようなので、ffmpegをはじめとするツールを自分で組み合わせて変換しないといけないのかと思ったが、携帯動画変換君というツールがあり、便利だった。 MobileHackerz Knowledgebase Wikiに色々な情報が集約されているので、変換君対応機種情報から自分の携帯電話用の設定(私の場合はW43CA用の設定)を見つけてTranscoding.iniにコピペ。簡単に変換できた。
とりあえず、TheCatsters's Playlists (c.f. 圏論の講義をYouTubeで - ヒビルテ (2008-03-11)) の講義ビデオとか、お気に入りのエロ動画とかを変換して、携帯につっこんでみる。
で、再生してみて思ったのは、携帯のメディアプレイヤーとしての機能の貧弱さ。私のW43CAの場合だと、ちょっと見逃したと思っても巻き戻せないし、再生を中断して他の作業をして後で同じところから再生を再開するといったことも出来ないみたい。これだと、本当にちょっとした動画の閲覧にしか使えないなぁ。
というわけで、ちょっと代替にはならなそう。 知り合いの中にはニンテンドーDSで動画を見てる人もいるけど、こっちはどうなんだろうなぁ……
【2008-06-09追記】 上で巻き戻し出来ないと書いたが、巻き戻しと早送りは出来た。 しかも、「←」や「→」という分かりやすいキーで、説明書にも書いてあった。アホだ俺……ごめんよカシオ。 説明書を見ないのはともかくとして、何故これらのキーを試すことを思いつかなかったかというと、通常の横長の動画だと携帯を90°回転した状態で見ることになるためで、この状態だと「↑」「↓」のボタンとして意識してしまっていたため(だと思う)。
これであと残る課題は携帯動画変換君で直接変換できない動画をどうするかだよなぁ。 ところで、佐野さんによるとNokiaの携帯ではビルトインの動画の再生環境は対応フォーマットは変換しないでも大抵は再生できるそうで、Nokiaの携帯が羨ましくなった。
2008-05-29 [長年日記]
λ. OCamlでランクn多相
レコードでもliftしたい - みずぴー日記 のコメントに関する補足。
関数を受け取って、レコードの型の異なる複数のフィールドに対して適用する高階関数を書きたいという話。
型の異なるフィールドに対して適用するには、受け取る関数は [Int]→[Int]→[Int] のような型の単相的な関数ではなく、∀a. [a]→[a]→[a] のような型の多相的な関数である必要がある。で、多相的な関数を受け取る高階関数の (∀a. [a]→[a]→[a])→Record→Record→Record のような型は、二階ラムダ計算の言葉でいうと、ランク2の型になっている。
ランクの正確な定義は Type reconstruction in finite-rank fragments of the polymorphic λ-calculus (c.f. The “Curry view” and the “Church view” of polymorphic λ-calculus - ヒビルテ (2006-04-25)) あたりを参照してもらうとして、ランク2の型はHindley-Milnerの型システムの表現力を超えるので、言語によって扱いが異なっていて面白い。
Haskellの場合
GHCはランク2多相(rank-2 polymorphism)をサポートしていて、型宣言を書きさえすれば自由に使うことが出来る*1。
{-# LANGUAGE Rank2Types #-} data Record = R { x :: [Int] , y :: [Double] } lift :: (forall a. [a] -> [a] -> [a]) -> Record -> Record -> Record lift f R{ x=x1, y=y1 } R{ x=x2, y=y2 } = R{ x = f x1 x2, y = f y1 y2 } append' :: Record -> Record -> Record append' = lift (++)
ちなみに、Haskellでのランク2多相の使用例でもっとも有名なのは、STモナド(Control.Monad.STモジュール)の runST :: (forall s. ST s a) -> a で、これについては Lazy Functional State Threads で詳しく説明されている。
OCamlの場合
一方、OCamlの場合にはランクN多相に直接対応してはいない*2けど、レコードのフィールドが多相型を持つことが出来るので、多相関数をレコードに包んで受け渡すことでエンコードできる。
type some_record = {x:int list;y:float list} type op = { app : 'a. 'a list -> 'a list -> 'a list } let lift f {x=x1;y=y1} {x=x2;y=y2} = {x=f.app x1 x2; y=f.app y1 y2} let append' = lift { app = (@) }
あと、同様の例として、昔のOCaml.jpにあったチャーチ数の例がある。
- Church 数 ― OCaml.JP
- <URL:http://web.archive.org/web/20060430024445/ocaml.jp/archive/sample/firstclass.ml>
Scalaの場合
Scalaでランクn多相をエミュレート - Onion開発停滞日記(2008-05-30) で水島さんがScalaへの翻訳を書いてくれました。ありがとうございます。 あとで自分でやろうと思ってたら先を越されてしまった(^^;
SML#の場合
現在のSML#にはこういった機能はないのかな。LLDN のときの上野さんの発表「Language Update: Standard MLer から見たML 概要」の「Next generation of ML」によると Rank-n polymorphism についても「理論的には完成。実装待ち」とのことなので、そのうち実装されるのだとは思うけど。
【2009-03-14追記】 ……と書いたけど、PPL2009で上野さんに聞いたら、どうもこういったファンシーな機能は当面実装されることはなさそうな感じだった。
F#の場合 (2009-02-19追記)
いげ太さんという方が、いげ太のブログ: F# で ランク N 多相っぽく でF#の場合について書かれていた。 F#ではOCaml流の多相的なフィールドを持つレコードではなく、ジェネリックなメソッドを持つインターフェースが推奨されているらしい。
2008-05-30 [長年日記]
λ. Lockdown in sector 4
Gmail のメールをバックアップしようと、Thunderbirdを使ってIMAPで「すべてのメール」フォルダをローカルにコピーしようとしたら、途中で「Lockdown in sector 4 (Failure)」といわれてIMAPでのログインが失敗するようになってしまった。 ぐぐってみると、24時間のアカウントロックってやつか。たかだか7万通、400MBたらずのメールで……。しょぼーん。
λ. LL Future チケット購入
帰りに Lightweight Language Future のチケットを購入。 Tシャツの有無は悩んだけど、とりあえずTシャツ付のチケットにしてみた。 以前だったら確実にTシャツ無しのを選んだと思うけど、中途半端にお金があるせいで財布の紐が緩んでしまった……。酔狂だよなぁ……。
2008-05-31 [長年日記]
λ. 西鎌倉混声コーラス第6回定期演奏会
西鎌倉混声コーラスの第6回定期演奏会なるものを観てきた。
- レクイエム ニ短調 K.626 (モーツァルト) [Naxos Music Library] [Naxos Music Library (SFC用)]
- 唱歌の四季
- 朧月夜
- 茶摘
- 紅葉
- 雪
- 混声合唱曲集 鳥の歌 (10のスペイン民謡より)
- 鳥の歌
- アララ
- アラブの二人娘
- さよならの夜
λ. クラスター爆弾禁止条約 採択
これまでクラスター爆弾が果たしていた役割を、どうやって代替していくのかな。 それを十分検討する前に採択されてしまった印象があって、色々不安。
ψ とおる。 [勉強になりました。ありがとう〜。]
ψ さかい [ありがとうございます。 そういってもらえると書いた甲斐があります。]