日々の流転

λ. tDiary 0.9.8

色々便利になってるっぽいんで、0.9.8にしてみた。tdiary.conf.sampleの@referer_tableの正規表現の「?」がエスケープされていなくてハマッタ。

λ. 英検

日大藤沢まで受けに行ってきた。結果は×だろう。やっぱ記述問題が特に苦手。

λ. セブン

を見た。

λ. Re: 遠藤さん

そういえば、SFCがあるのは藤沢市遠藤なのですよー

ってのはおいておいて、T(f)(x,y)=(f(x),f(y)) はHaskellでのリストやツリーのFunctorと同じで、要素毎に写像を適用してるだけですよん。(といっても単なる直積なので、要素は2つしかないけど)

λ. 続merd

Makefileを修正したらコンパイルが通った。

λ. 自然言語論

一応メールで報告してみました。

それにしても、関さんにまで見られているとは……。こりゃますますうっかりした事は書けないなぁ。

λ. 『妻みぐい2 [ADULT]』

Amazonにこんなのを勧められる。お勧めの理由(の一つ)は『計算機プログラムの構造と解釈』を評価してたかららしい。ビバSICP。

λ. ALGI-13 Proceedings

数理解析研究所講究録１３１８
短期共同研究 代数・論理・幾何と情報科学
京都大学数理解析研究所
２００３年５月刊

λ. C410 封印の村 (ネタばれ注意)

負けちゃった。村側に突然死5という時点で厳しかったけど、勝ち目が全くなかったという訳ではないのに狭義狼側完全勝利……悔しい。村側の能力者は共有者しかやったことなかったので、いっちょ占い師でもやってみるかと思って、占い師を希望してみたんだけど……信頼を得るのって難しいね。極端な事例ではあるけれど、この村は大変勉強になりました。

キャラクタはモーリッツを選択。最初は仙人(道士)のRPをしようかと思ってたのだけど、ネタを用意するのが面倒になって止める。かわりに、前から一度やってみたかった旧字・旧仮名遣いでのRPに挑戦。旧字・旧仮名遣いのためのIMEの辞書で気に入ったものが見つからなかったので、入力は 旧仮名・旧字変換支援 misima を使って変換しました。それから、野嵜さんの「正かなづかひ早分り」を参考にさせて貰いました。 素晴らしいサービスと素晴らしい文章をありがとうございます。

敗因は、エピローグでも指摘されてるけど、三日目に「ペーター霊能者・ヨアヒム人狼なら、ペーターに白白は変。よって、ヨアヒム霊能者・モーリッツ占い師」という推論に到達出来なかったというのが最大のものだろうな。こんな単純な推論に考えが至らなかったのが悔しい。もっとも、モーリッツの口から言っても効果は薄いのだけど。

それと、疑問が出てきた。二日目はモーリッツだけに占われて黒判定を受けていたカタリナを放置して、突然死しそうだったアルビン吊った。これには多くの人が賛成していたのだけど、これは果たして適切な選択だったのだろうか?

これもエピローグで指摘されているけど「モーリッツが占い師ならば、残り狼の数に関わらず、翌日には狼側の霊能者は狼が全員生きている判定を出す可能性が高い」。よって、翌日になればカタリナを安全に吊れるということはなくて、2日目よりも3日目の方が「失敗したら負け」という点で、カタリナ吊りのリスクは大きくなる。また、翌日黒確定が出るのもまず期待できない。ならば、モーリッツが庇っていたアルビンと、モーリッツが黒判定を出したカタリナは別陣営と考え、アルビンの突然死と同時にカタリナを吊るというのが最大のリスクヘッジだったのではないか?

関連URL

• 人狼BBS:C C410 封印の村
• 人狼BBS まとめサイト - C410村
• 人狼BBSの事をぐだるページ:C410村, yuragiさん(ペーター)のブログ

λ. 『余は如何にしてナショナリストとなりし乎』, 福田 和也

を読んだ。福田 和也 の言う意味でならナショナリストでありたいと思った。

λ. C410村で提案した、靈能結果の報告を投票で行う案

以前に日記で投票による結果報告について書きましたが、この村では初日に突然死が大量にあったので、霊能者が投票COで同時に突然死者中の狼の人数を伝えることを二日目に提案してみました。

老人 モーリッツ 午後 6時 19分

■1. 靈能の結果報告を今日の投票で行ふといふ案を考へてみた。具體的には「突然死者に含まれる人狼數が0,1,2名ならそれぞれA,B,Cに投票」といつた感じ。檢討してみて慾しい。

羊飼い カタリナ 午後 8時 53分

■1.霊能者さんが発投票ＣＯする場合、お爺さまの案を考えてみましたわ。
今日の生存者リスト順に並べます。
羊屋老旅商年者神青妙木。狼残０なら自分の一つ後ろの人に投票。１なら１つ前、２なら２つ前。但し、今日の投票先がありますから、その方は抜きます。
ニコラスさんで説明させていただきます。０ならアルビンさんに、１ならお爺さまに、２ならオットーさんに。先頭の私と最後のトーマスさんはつなげます。私だと、０オットーさん、１トーマスさん、２リーザさん。これなら投票先誰々とした時、その人が霊能者さんだったら？という事を考えなくて済みますわ。

老人 モーリッツ 午後 10時 46分

カタリナの投票CO案は興味深いのう。カタリナとは何だか氣が合ひさうぢや。
ちなみに儂は以下のやうな別の案を考へてをつた。
「突然死者中に狼0ならジムゾン、1ならペーター、2ならモーリッツに投票。ただし、指定された投票先が自分自身の場合にはニコラスに投票」(人物名は仮のもの)

(ところで、「狼残０」ならゲームが既に終はつてゐなくちやいけないやうな……)

λ. Smullyan's drinkers' paradox を Alloy で

Paradoxes of classical predicate calculus - ヒビルテ (2007-08-28) で Smullyan's drinkers' paradox を扱った。

これは英語で書くと「In any non-empty bar, there is a person such that if she drinks, then everyone drinks」で、論理式で書くと「∃p. (drink(p) → ∀y. drink(y))」というもの。 古典一階述語論理での演算子の意味を考えれば、当たり前ではある*1のだけど一見するとパラドクスに思えてしまう。

こないだは Agda で証明したので、今度は Alloy でも試してみる。

-- 個体領域
sig Person { }
fact { #Person > 0 } -- 個体領域は空ではない

-- 述語
one sig Drinkers { ext : set Person }
pred drink(p : Person) { 
  p in Drinkers.ext
}

-- test
pred show() { }
run show for 10 Person

-- Smullyan's drinkers' paradox
assert paradox {
  some x : Person | drink[x] implies (all y : Person | drink[y])
}
check paradox for 10 Person

これを Alloy Analyzer でチェックしてあげると、ちゃんと「No counterexample found」となる。 また、ここで「fact { #Person > 0 }」を削除すると、ちゃんとPersonが一人もいない例が反例として得られる。

2010-12-23 追記

上の書き方はあまり良くなかった。

• 空でないことは、濃度演算子を使うより、someを使って表現したほうが良い。
• 部分集合はDrinkersのようなシグネチャのフィールドにしなくとも、部分集合シグネチャを使えばより直接的に表現できる。

直すと以下のようになる。

-- 個体領域
sig Person { }
fact { some Person } -- 個体領域は空ではない

-- 述語
sig Drinker in Person { }
pred drink(p : Person) { 
  p in Drinker
}

λ. 数学基礎論を巡るつぶやき

週末にtwitter上で行われていたやりとりが非常に面白く、散逸してしまうのが勿体無かったので、まとめてみた。 しかし、twitter上のやり取りを後から追いかけるのは想像以上に大変だった……

• salmonsnare (#1 #2 #3 #4 #5 #6): 基礎の公理の成り立たない集合論 (non well-founded set theory) について, これって、AFA集合論のことか。引用「いずれにしても， 数学としては，基礎の公理の成り立たない集合の理論 （つまりその理論ですでに確立している結果や将来確立されるであろう結果の総体）が数学理論として 「美しい」，あるいは，「面白い」（ものになる）かどうかが， この理論の（数学理論としての）存在意義の評価を左右することになるのだろうと思います．」　この辺の議論の流れをつかみたい。昔、こういう資料を見つけて読んでいたことがある。超集合論—circularityの論理の現在—
• h_kagami (#1 #2): Axiom of Foundation を否定した「集合論」って集合論の本質的に重要な議論が全然できなくなると思います。「超」がついてるのであれなのですが、はたして「集合論」と呼べるのかどうかは疑問に思っています。もちろん AF を否定した「集合論」の研究を否定しているわけではありません。
  • kururu_goedel (#1 #2 #3): 基礎の公理が成り立たないモデルでの集合論は、有効な局面もある(とi-landさんが言っていた)のですが、その研究には基礎の公理が成り立っているモデルからの視点が不可欠になるだろうということです。 選択公理と決定性の公理の話と同様、どちらが正しいというレベルではなくて、どちらが与えられた状況下で有効かで見ていくべきものだと思います。そして、基礎の公理はとても強力かつ害が少ないので普段は仮定するほうが自然。 渕野先生が書いていらした文章も、結局はそういう切り口だったと思います。
  • ytb_at_twt (#1): すみません、基礎の公理の件ですが「基礎の公理はとても強力かつ害が少ないので普段は仮定するほうが自然。」というのは、standardな集合論者の偏見が混じっていませんか。
  • kururu_goedel (#1 #2): 確かに言葉の選び方が良くなかったです。ごめんなさい。偏見はもちろん入っていますし、それは込みで読んでいただきたいところなのですが(たかだかtwitterだし) 私が良くないと考えているのは、「基礎の公理は不自然なので仮定するべきでない」という見方であって、「不可欠｣は勇み足ですね。要は、ZFCとZF+ADの関係みたいになればいいなと思っているだけでして。
  • ytb_at_twt (#1 #2): ついでに、「その研究には基礎の公理が成り立っているモデルからの視点が不可欠になるだろうということです。」について、極論すれば「ZFの証明は自然数論の枠組みで形式化できるから集合論には自然数論の視点が不可欠」とか言えるような気もするのですが。 F先生が「数学の基礎」という言葉で何を意図されておられるのか、私には理解できません。
  • kururu_goedel (#1 #2 #3 #4): 私自身は『数学を展開するための基礎としての集合論』みたいな言い方からは微妙に距離をおいているつもりでいます。一般向けの文章でもプロポーザルでも立ち入り過ぎないようにしています。 そういうのを云々できるほど、哲学の知識も数学全体の知識もありません。謙遜でも逃げでもなく事実として。 でも、数学の多くがZFC上で展開できて、かつZFCに特有のテクニックを使って強力な議論を展開できるから、有効な見方のひとつであることは確かだと思うのですが。私にはそれで十分です。 つーか楽しいじゃんよーZFC。ZFC抜きでgeneral topologyできないじゃん。PCF使ってDowker space作ったり、minimal walk使ってL-space作ったり出来ないじゃん。つーか、俺の飯の種なくなるじゃん。
  • ytb_at_twt (#1): ZFC楽しいよねー。便利なツールも揃ってるし、ツール自体いじって楽しいし。ついでに、「基礎の公理はADなみに面白い」ってのにも賛成。それだけだったら、何の文句もありません。楽しい学会をお過ごしください。
• masahiro_sakai (#1): 外延性の成り立たない集合論を考えることすらあるのだから、それに比べれば、基礎の公理が成り立たない集合論なんてかわいいものだと思うけどなぁ。
  • h_kagami (#1): 道具としてではなく集合論そのものを研究対象とする場合、基礎の公理を否定したものを「集合論」とは呼びにくい気がします。
• masahiro_sakai (#1 #2): 渕野先生の 基礎の公理の成り立たない集合論 (non well-founded set theory) について には概ね異論はないけど、基礎の公理の成り立たない集合論を持ち出すことが、「大砲で雀を撃つ」ようなものという感覚は私には良くわからない。 基礎の公理の成り立たない集合論を使えば話が簡単になるところで、基礎の公理の成り立つ集合論の内部で作ったモデルを使って間接的に議論するのは、むしろ回りくどくはないのだろうか。

  • ytb_at_twt (#1 #2 #3): 渕野先生は

    1. ZFCは全ての数学の基礎である
    2. 解析学など、他の理論は全てZFCの中でコーディングされ展開される
    3. ZFCで直接は扱えないストリームなどを扱うZFAも、ZFCの中で展開される
    4. ZFAは、あくまでZFCの中で展開されるサブ理論であり、「数学の基礎ではない」
    5. ZFAを「ZFCと同等に重要」というためには、ZFAを「数学の基礎」と見なす必要がある
    6. しかし、そうすると、超限帰納法による既存の集合論の証明技術がoverkillされてしまう
    7. 「大砲(ZFAの基礎理論化)で雀（ストリームetc）を撃つ」のは、益少なく、無駄である。

    という感じだと思うのですが、いかがでしょうか。

    • masahiro_sakai (#1): 「意識のモデル，ないし概念認識のモデルを考察するときに」という前提で、基礎の公理と反基礎の公理のトレードオフを考えてましたが、「ZFAの基礎理論化」が前提なら納得です。
    • ytb_at_twt (#1 #2 #3): 渕野先生の論法の問題点は、彼の議論で重要な役割を果たす「数学の基礎としての集合論」と言う言葉の意味がよく分からないと言うことです。ZFAを研究している人は「数学の基礎」を目指している訳じゃない。 単に数学の論理的分析をするための枠組みならたくさんある。各種集合論、各種型理論、逆数学、etc. 異なる理論間の数学的内容の比較の共通プラットフォームとしては圏論があり、「その意味において圏論こそ数学の基礎だ」とAwodeyが絶叫していた。 渕野先生は「数学の基礎としての集合論」って言葉で何を意図しているのか理解不能だし、ZFAのような「数学の基礎としての集合論」を目指していない理論を、そうとなり得ないという理由で攻撃するのはお門違いではないかと思います。だから私は渕野先生に反対です。
    • masahiro_sakai (#1): 『ZFAのような「数学の基礎としての集合論」を目指していない理論を、そうとなり得ないという理由で攻撃するのはお門違い』というのも同意。これを読んで、渕野先生の文章に対してどこかひっかかっていたのが、すっきりしました。
  • kururu_goedel (#1 #2 #3): そういうのは私も同意するところなんですが、元々ZFCはその中で他の理論をモデル化するのが普通の利用法なわけで、考えているZFAのモデルがZFCの中で構成されているとイメージまたは仮定しても何の害もないような。 私のようなZFCの外にはほとんど出れないような人間でも、簡単な群論の問題を解くのにそれがZFCの中にあるものかなんて考えないわけですから。 あー、ZFCの中でモデル化したZFAのモデルには何らかの制限が加わるとかいうのなら、話は別なのですが。そのあたりよく知らないので。
    • masahiro_sakai (#1): それはその通りだと思います。ただ、モデルを使って考えることは、議論の単純さとかの点で、モデル化される理論を直接使って考えることの、完全なオルタナティヴにはならないのではないかと思って、あのように書きました。
    • h_kagami (#1: 「G を群とする」と言った途端群論のモデルを考えていることになると思いますが、そんなに不便でしょうか。
      • h_kagami (#1 #2): ちょっと真面目に考えたのですが。例えば V ≠ L の場合 L を「外側から」眺める観点は非常に有用です。 例えば AFA を理論として通常の集合論をモデルと考えた場合、その逆の場合、「外側から見る」という観点でどちらが面白いかという判断は有用かも知れません。
      • h_kagami (#1): どっちが理論でどっちがその内部で作れるモデルなのかの主導権争いみたいな感じもしないではない。あ。また余計なことを。
      • ytb_at_twt (#1): 主導権を主張しているのはF先生だということをお忘れ無く。
      • h_kagami (#1 #2 #3): 主導権と書いたのは余計なことでした。ただ集合論を道具としてではなく、その内部を研究されている方が、AF の否定という言明について「そんなばかな」と思われる気持ちはよく分かります。もちろん AFA について「そんなばかな」なんて言ってません。そもそも基礎の公理がないと清楚清純萌え萌え美少女ねたが使いにくくなるではないか。
    • masahiro_sakai (#1): うーん。念頭にあったのは、例えば自然数の乗算の可換性はペアノ算術だけで証明出来るのに、ペアノ算術のモデルを持ち出して議論するといったものです。
    • h_kagami (#1): 了解しました。たしかに範疇的な公理系を考える場合と非範疇的な公理系の場合ちょっと雰囲気が違うかも知れません。さらに集合論系は独特なので。
    • masahiro_sakai (#1): 私は範疇性について全然わかってないのですが、ここでは集合論が範疇的ということでしょうか? (そういえば、ZF2ではquasi-categoricityが成り立つとかなんとか昔聞いたような……)
    • h_kagami (#1 #2 #3 #4 #5 #6): 範疇性は例えば実数論のように公理と基数が与えれたときその基数であるモデルが唯一存在する理論だったと思います。すみませんいまいち自信なしです。 なんというかある種の対象を規定するための公理という感じだと思います。数論とか実数論とか実体があるという感じで。 群論みたいなのは「群」を規定するというよりも議論の仮定というニュアンスが強いかなと。 なので群論の場合理論で考えてもモデルで考えても特に違いはなくて、逆に範疇的な理論とそのモデルというのは扱いに違いがでるのではと。 集合論に関しては難しすぎて良く分からないです。ちょっといいかげんなこと書いたかも知れません。ごめんなさい。 例えば実数の可算モデルと言われると驚きますが、群論のなんとか基数モデルと言っても別に驚かないという感じでしょうか。
• h_kagami (#1 #2): 色々な批判を受けながらも数学の基礎としての集合論もすいぶん寿命が長いと思います。 数学の基礎という点ではいずれ新しい理論に道をゆずる日が来るかも知れません。そうなったとしても集合論内部の構造研究はまだまだ続くと思います。
• h_kagami (#1): ZFC が、色々批判もあるかと思いますが、いまのところ伝統的な数学的構造とそれなり相性が良い理由はよく分かりません。
• patho_logic: (#1 #2 #3): twitter 上の「数学基礎論を巡るつぶやき」残しておけないだろうか。このまま消えてしまうのがもったいない。断片的な発言を引いて「やっぱ基礎論怪しいね」みたいなことになると困る。

その後の話。

• yoriyuki (#1 #2 #3 #4 #5 #6): http://bit.ly/KIKuL だけど　そもそも *The* Foundation とは何か、という問いを立てているみたいだけど、あまり共感しないなあ。数学というのは、「雑多な技法の寄せ集め」だと思う。集合論の公理についていえば、http://dx.doi.org/10.1016/j.apal.2008.09.010 みたいに公理の強さを精密に測定していくというのが生産的だ。ちなみに基礎の公理はあまり強くなくて、外延性公理の方が強いらしい。