はからはな (2008/12/16)

2008/12/15

はからめ飼って11年。初めて花が咲きそうである。

何だか季節外れにどんどん枝葉が伸びて来て、 こいつ一体どうなっとるんじゃ、と思ってたわけですが、 今日見たらつぼみがあった。 つまり葉から芽、芽から花である。

コツは冬の間、夜はあまり明るくないところに置く事だってさ。 最近は、夕食後は6帖の和室にひっこんでコタツムリとなっている。 そのため、はからめが置いてある居間(10帖くらい)はまっ暗なのである。 6帖なら、人間が二人居るだけで、けっこう暖かい。 というか集合住宅は自分で暖房をほとんどつけなくても暖かいな。 まえの家は、朝起きたら4度とか6度とかだったもんな。気温が。

鳥の貯食？それとも子供か？ 葉っぱや苔で隠そうとした形跡もあり、しかしここはすぐに人間に見付かる場所であり、 いまいちよく判らない。

それから、妻が調子が悪いので俺がパンを焼いてみた。 わっはは。変な形。 でもこのパンは、国産小麦の天然酵母なんだーぜー。 うまく焼くのは超絶にムズいんだーぜー。 先週末、喋りすぎた。 おかげで喉がむちゃくちゃ痛いんだーぜー。 むしろ風邪ひいたかも。 というかむしろ疲れた。 午前中薫製、午後講演ってのはどうなんだ、人として。

妻が発注したパル式のDVDを見れるプレーヤが届いた。 ビミョーにテレビ台に収まらない寸法だった。そこで台を改造した。

台の上に乗っているテレビは重いので、横の板を耐力壁として 天板を支える構造だったのだが、 これでは天板の半分の厚さが釘に乗った分だけでテレビの重さを支えている事になり、 脆弱である。 しかしモノが収まらないのではしょうがない。

かいせつ

先日の講演資料ですが話を聞いてないと何だか解らないページもありますので、 それを補完する解説記事を書いておきます。 これが薮蛇にならなければよいのですが。

• 17貢: どちらも再帰画像。しかも右は balanced binary tree になっているという。 つまり再帰の視覚的表現だが、こういう画像にグっとくるような人に 計算科学適性があるのではないか、という話です。 右の画を元にした Droste Effect という用語があります。 有界な領域に可算無限の構造が再帰的に入っている事により引きおこされる 様々な視覚的効果の事です。 18は自己言及の 視覚的表現。GEBは ゲデル エシャ バハ ていう本がありましたね、むかし。 私は読んでませんが。
• 24貢: 証明つけときます。

  決定不能命題とは、命題も、その否定命題も定理にならない命題の事です。 ですから、gの決定不能性を証明するには、g と ~g の両方が 定理にならない事を無矛盾性を仮定して証明します。まず g から。 gが定理なのでgに証明があり、したがって B(g) も証明可能であり、 すなわちB(g)も定理。gは ~B(g) と同じ命題なので ~B(g) も定理。 つまりB(g)と~B(g) の両方が定理。 これはシステムの無矛盾性に反するので、システムが無矛盾ならgは定理ではない。 ~g については普通の矛盾を可算無限に拡張したω矛盾という概念を用いて 証明します。 これは通称「ゲーデルの第一不完全性」といわれる性質です。 次は第二不完全性で、こちらのほうが通俗的には有名かもしれません。

  こちらの証明は、無矛盾性が定理になれば、システムは矛盾する、 という筋道でおこないます。対偶をとれば、無矛盾なシステムでは 無矛盾性は証明できない、となりますね。無理に一般化すれば、 「俺は正直だ」とか言う奴はウソつき、という事になりますか。

  無矛盾性が定理になる、というのを記号で書きましょう (矛盾(恒偽命題)をここでは nil と表記しましょうか)。 nil が証明される事はない、 というのを記号で書けばいい。nil が証明される、は B(nil) なので その否定は ~B(nil) ですな。 B(g)が定理だとすると B(g)= ~g より ~g が定理になり、 ~g が証明可能ということなので B(~g) も定理になります。 B(g) と B(~g) が揃ったので B(nil) であり、仮定に反するので ~B(g) は定理になります。 という事は g=~B(g) より g も定理になります。 gが定理つまり証明可能なので B(g) も定理になり、したがって ~g が定理になり ~B(nil) から出発して矛盾にたどりつきました。証明おわり

  以上の証明のなかで、やはり気になるポイントは B がホントにあるのか、 という点と、その B に対して不動点となる g が都合よくあるのか、 というところでしょう。 B の存在は Church の弟子である S. C. Kleene が証明しているらしいので、 その権威にタテつくよりもそのまま使うのが賢明ですよね。 それで、 g の存在のほうを、 やはり Church の学生である H. Curry の不動点演算子にやってもらう、 というのがこの企画の趣旨です。

  しかし Church の学生が Curry と Kleene ってそれ、どんだけ濃ゆい 研究室やねん。眩がするわ。

• 26貢: Yが任意の貢の不動点を生成する高階関数であるのを 確かめてみる、というのは Introduction to Lambda Calculus ftp://ftp.cs.ru.nl/pub/CompMath.Found/lambda.pdf の12ページあたりをみてください。 俺が講演でやったよりも、だいぶかっこいい計算で証明してあります。
• 29貢: ここにでてくるYは適用順評価(applicative order evaluation) 版の不動点演算子です。 適用順評価と正規順評価の違いはたとえば SICP の 1.1.5 を見て下さい、 ってこれ、授業の第一回めくらいの場所ですよ。 最初の授業でこの話が出て来るってそれ、どんだけ濃ゆいクラスやねん。 それ、いくらなんでもムズいでしょう。人として。

細かい話としては untyped lambda calculus には矛盾があるので どうこうみたいな事になりがちですが、 まぁそのへんは大目にみてください。 矛盾があるかないかは、あんまり細かい話ではありませんがね。ははは

2008/12/16

最近よくオオタカを見るな．今日も森の上を飛んでいるのを見た。

田舎の人はオオタカが居たって全く判らないのな。 というか、どんな鳥なのかすら見当つかないみたいで。 2mくらいあって、犬とか持って飛んで行く、くらいの認識ですわ。 それイヌワシだって。 というかイヌワシもさすがに犬持って飛ばないって。 というか普通の人は「鳥は鳥」ですけどね。

それでオオタカだけど、 カラスくらいの大きさって言うとえらいガッカリするのな。

巨大な椿。花が咲きほこっており、ものすごい数のメジロが常に居る。