Journal InTime

_ 末尾再帰

前もやったけど末尾再帰の最適化をRuby 1.7に実装してみた。

<URL:http://www.shugo.net/archive/ruby17-tail-recursive.diff>

末尾再帰の最適化とは、簡単にいうと、

def foo(...)
  ...
  return foo(...)
end

のような末尾再帰でスタックを食い尽くさないようにすること。

どうやって実現しているかというと、あるメソッド(A)内の最後のメソッドコール(B)では、 Aに戻って来る必要がないことを利用して、Bの前にAの呼び出し前に戻ってしまう、という 方法を使っている。上記のコードでは、return foo(...)という部分でいったんfooの呼び 出し元に戻ってから再びfooを呼ぶので、何回fooを呼んでもスタックを食い尽くすことが ないってわけ。現状ではメソッドコールのたびにsetjmp()するので効率が悪いけど、上手 くやれば改善できると思う。

ところがmake testに通らない。原因は、

def foo
  proc {
    return "hello"
  }.call
end
p foo

みたいなのが

-:3:in `call': return from proc-closure (LocalJumpError)
        from -:3

というエラーになること。 最適化でProc#callの前にfooの呼び出し元に戻るので、Procがorphan (みなしご)になっちゃうわけですね。

これは難しいなあ。 orphanなProcからreturnした時は、例外を上げる代りにcontinuationで 元のメソッドに戻ることにするとかいうのは...だめだろうな。

_ 続き

上のバグの対処法を思いついたけど、上手く動かない。 うーん、今日はPC持って帰るか。

_ かぜ

かぜをひいた。 のどの痛みと鼻水がひどい。

_ action以外のメソッドをpublicにしてはいけない

何となく、以下のaction_methodsの実装を見て気になっていたのだが、 Railsのコントローラのメソッドでpublicなものは、すべてaction として扱われてしまう(=外部から呼び出し可能になる)ようだ。

def action_methods
  @action_methods ||= (self.class.public_instance_methods - self.class.hidden_actions)
end

これって周知されてる?

気持ちはわからなくもないけど、メソッドの可視性をそのまま使ってしまうのは あまりよくないと思う。

def show
  ...
end
action_method :show

とかの方がよかったんじゃないかなあ。

まあ、でも、Railsっぽいなという気はする。 Railsを使う時は、Railsの慣習をよく知っておかないと危険かもしれない。 適当にやってても動いてしまうだけに。

自分は、

def action_methods
  return ["list", "show", ...]
end

とでもしとくかな。 public_instance_methodsのコスト *1 を免れるし。

_ image_tagと絶対URI

image_tag(というかcompute_public_auth)にhttp://hostname/path/to/fileのような 絶対URIを渡しても、相対パスとして扱われてしまうようだ。

そういうもの?

_ 松江市長・市議選

一応投票。

しかし、旧松江市の選挙区は定数34に候補者36人で、どうも盛り上がりに書ける。 個人的には、中島始候補の広報にウケた*1。 4年後は、全市で一区になるようだ。

結果は、一勝一敗。

_ Brouwerの不動点定理と直観主義論理

Conceptual Mathematicsと並行して記号論理入門を読んでいるのだが、たまたまConceptual Mathematicsの方でBrouwerの不動点定理を取り上げた章を読んでいる時に、記号論理入門の方でBrouwerの名前が出て来て面白かった。

記号論理入門によると、Brouwerは「数学において排中律を無制限に用いるのは正当でない」と主張したそうで、古典論理から排中律を除いた論理体系を直観主義論理と呼ぶそうなのだが、Conceptual MathematicsのSession 10の§4の演習では背理法を使う必要があって、このケースでは排中律(を前提とする背理法)を使ってよいのかなと疑問に思った。

ところが、改めて前の§を読み返すと、p.125に以下のような記述があった。

We need to use another principle of logic, that not (not A) implies A, to reach `every f has a fixed point.' Brouwer himself seriously questioned this rule of logic; and we will later see that there are examples of useful categories in whose `internal' logic this rule does not hold.

[Conceptual Mathematicsより引用]

日本語に翻訳すると、以下のような意味だと思う。

「すべてのfは不動点をもつ」を導くためには、論理のもう一つの原理である「not (not A) ならば A」を使う必要があります。Brouwer自身はこの論理規則に対して深刻な疑問を呈していました。後に見るように、いくつかの有用な圏の例においては、その「内部の」論理ではこの規則が成り立ちません。

読み流していたけど、Brouwerの直観主義を踏まえて敢えてこういう構成になっているんだな、とちょっと感動した。 ちなみに「not (not A) ならば A」（¬¬A→A）は、排中律「A or not A」（A∨¬A）と同値である（記号論理入門 p.57）。

追記: 後で読み返したらここはBrouwerの証明をなぞっているだけで、別にこの本独自の構成というわけではないようだ。独自なのは、§5で二つの公理を導入することで、位相空間と連続写像の詳細を説明せずに、Brouwerの定理を一般化した定理［topological spaceだけでなくsmooth space（ってなんじゃらほい）などにおいても成り立つ］を導いているところのようだが、消化しきれていないので後でもう一度読む。