日々の流転

λ. Script-Fuがマルチバイト文字を扱う関数を提供していない件

どうもうまい説明が思いつかず保留してたけど、いつまでもこうしてたって仕方がないので、ようやくbugzillaに登録した。#67808。パッチを付けようかと思ったのけど、どうも僕には綺麗に解決するのは無理そうだから、やめた。

というのも、最初はScript-Fuの文字列の内部表現をワイドキャラクター(1.2ではwchar_t*で、1.3ではgunichar*)にしようかと思ったのだけど、それだとファイル名を文字列型で表せない可能性があることに気付いてこの方針は諦めた。だって互換性を考えたらそんな変更が通るとは思えないし……　かといって明示的にワイド文字列に変換したり、あるいはマルチバイト文字列のままで頑張るというのも、気が進まなかったし……

λ. 今年の抱負

どうせなのでネガティブに書いてみる。

• 欲望を実現するために全力を尽くす。
• そのためには躊躇しない。後悔しない。
• そのためには他人を省みない。むしろ積極的に犠牲に。

λ. Ruby/Gtk

Gtk::BINDING_VERSIONが[0,2,5]のままだったので、patch managerに登録してみた。[ #498502 ]

--- ruby-gnome/gtk/src/rbgtkconst.c~	Thu Oct  4 11:13:40 2001
+++ ruby-gnome/gtk/src/rbgtkconst.c	Wed Jan  2 20:58:24 2002
@@ -15,7 +15,7 @@
 
 #define RBGTK_MAJOR_VERSION 0
 #define RBGTK_MINOR_VERSION 2
-#define RBGTK_MICRO_VERSION 5
+#define RBGTK_MICRO_VERSION 6
 
 /*
  * constants

λ. それから、Win32でシンボルがexportされるようにgtk.defを用意して……と思ったんだけど、"Fatal error: Call to a member function on a non-object in common/tracker/ArtifactFile.class on line 106"とか急に言われてファイルの添付に失敗したので焦った。ひょっとしてPatch以外のファイルを添付しちゃいけなかったのかな?　どうもSourceForgeの使い方って良く分からない。あと、本当はシンボルをexportするだけじゃなくてrbgtk.hもいじらなくちゃいけないんだけど、そんなこんなで憂鬱なので今日はパス。[ #498549 ]

λ. chkURLBuffer

main.cのchkURLBufferでhttpのパターンに「;」が含まれないのは具合が悪いので、とりあえず以下のパッチを当てて使ってみる事にする。本当はRFC1738あたりをちゃんと確認しなくちゃいけなさそうだけど……

--- w3m/main.c~	Fri Dec 28 03:23:00 2001
+++ w3m/main.c	Thu Jan  3 01:38:12 2002
@@ -4147,9 +4147,9 @@
 chkURLBuffer(Buffer *buf)
 {
     static char *url_like_pat[] = {
-	"http://[a-zA-Z0-9][a-zA-Z0-9:%\\-\\./?=~_\\&+@#,\\$]*[a-zA-Z0-9_/=]",
+	"http://[a-zA-Z0-9][a-zA-Z0-9:%\\-\\./?=~_\\&+@#,\\$;]*[a-zA-Z0-9_/=]",
 #ifdef USE_SSL
-	"https://[a-zA-Z0-9][a-zA-Z0-9:%\\-\\./?=~_\\&+@#,\\$]*[a-zA-Z0-9_/=]",
+	"https://[a-zA-Z0-9][a-zA-Z0-9:%\\-\\./?=~_\\&+@#,\\$;]*[a-zA-Z0-9_/=]",
 #endif				/* USE_SSL */
 #ifdef USE_GOPHER
 	"gopher://[a-zA-Z0-9][a-zA-Z0-9:%\\-\\./_]*",
@@ -4161,9 +4161,9 @@
 #endif				/* USE_NNTP */
 	"mailto:[^<> 	][^<> 	]*@[a-zA-Z0-9][a-zA-Z0-9\\-\\._]*[a-zA-Z0-9]",
 #ifdef INET6
-	"http://[a-zA-Z0-9:%\\-\\./_@]*\\[[a-fA-F0-9:][a-fA-F0-9:\\.]*\\][a-zA-Z0-9:%\\-\\./?=~_\\&+@#,\\$]*",
+	"http://[a-zA-Z0-9:%\\-\\./_@]*\\[[a-fA-F0-9:][a-fA-F0-9:\\.]*\\][a-zA-Z0-9:%\\-\\./?=~_\\&+@#,\\$;]*",
 #ifdef USE_SSL
-	"https://[a-zA-Z0-9:%\\-\\./_@]*\\[[a-fA-F0-9:][a-fA-F0-9:\\.]*\\][a-zA-Z0-9:%\\-\\./?=~_\\&+@#,\\$]*",
+	"https://[a-zA-Z0-9:%\\-\\./_@]*\\[[a-fA-F0-9:][a-fA-F0-9:\\.]*\\][a-zA-Z0-9:%\\-\\./?=~_\\&+@#,\\$;]*",
 #endif				/* USE_SSL */
 	"ftp://[a-zA-Z0-9:%\\-\\./_@]*\\[[a-fA-F0-9:][a-fA-F0-9:\\.]*\\][a-zA-Z0-9:%\\-\\./=_+@#,\\$]*",
 #endif				/* INET6 */

λ. 最小不動点と最大不動点

A Categorical Programming Lanuage の論文では

left object nat with pr is
  zero: 1 -> nat
  succ: nat -> nat
end object

に対応するright objectとして

right object conat with copr is
  pred: conat -> coprod(1,conat)
end object

を定義していた。ここでnatは NatF(X)=1+X の最小不動点に、 conatはNatFの最大不動点になってる。 対称性は、natの定義を以下のようにcoprodを用いたものに書き換えると 明らかでしょう。

left object nat with pr is
  α: coprod(1,nat) -> nat
end object

論文には(何故か)取りあげられていないのですが、 さらに同様にして、

left object list(X) with prl is
  nil:  1 -> list
  cons: prod(X,list) -> list
end object

に対応するright objectとして

right object colist(X) with coprl is
  α: colist -> coprod(1,prod(X,colist))
end object

が定義できるはずだ(しかし、natural transformation αの良い名前が思いつかなひ)。 listが有限のリストを、inflistが無限のリストを表わしているのに対して、 こいつは有限と無限の両方のリストを表わすはず。 listとinflistからの埋め込みはそれぞれ

• list2colist = coprl(prl(in1, in2.prod(I, case(nil, cons))))
• inflist2colist = coprl(in2.pair(head,tail))

となる。

λ. Haskellとの関係

ところで、Haskellのリストがlist,inflist,colistのどれに対応するかを考えると、Haskellのリストは有限のリストも無限のリストも共に表わすことが出来るので、明らかにcolistに対応するはず。

代数的データ型の意味はfunctorの最小不動点として与えられるとよく言われるが、Haskell等のlazyな言語ではそのlazynessのために最大不動点になっているように思える。

λ. あけましておめでとうございます。

本年も是非よろしくお願いします。

最近更新が滞ってましたが、ぼちぼち再開してきます。

λ. 初詣

成田山, 金龍山浅草寺, 柴又帝釈天へツアーで行ってきた。えっ? 全部お寺なのに何が初詣だって? ノン、ノン、ノン、モナミ。成田山には巫女さんがいたのですよ。どう見てもバイトの人とはいえ、巫女さんがいるのだから、初詣で全然問題ないのですよ。ええ!! (以下略)

……とりあえず神仏習合バンザイって事で。

λ. newtype/datatype (was efficiency)

そうか、単純に pointed CPO だけじゃだめなのか。なるほどねぇ。Haskellのデータ型の意味についてちょっとナイーブに考えすぎてたな。それから、「undefined :: a->b」と「λx.undefined :: a->b」が異なっているという話で、Topology via Logic に以下のように書かれていたのを思い出した。

However, we get something more interesting if we try to solve

  D = [D→D]⊥

This has been studied by Abramsky [87,90], and also, following him, by Ong [88], in connection with the lazy λ-calculus. The effect of the lifting is to make a distinction between ⊥, a completely divergent object, and λx.⊥, which is known to be a function but which diverges whenever it is applied to an argument.
Computationally, this corresponds to not trying to evaluate a function beyond the λ until application time, and is the way things are generally done in practice.

---

• S.ABRAMSKY
  • [87] Domain Theory and the Logic of Observable Properties, PhD Thesis, Queen Mary College, University of London, 1987.
  • [90] "A domain equation for bisimulation", Information and Computation, 1990.
• C-H L. ONG
  • [88] The Lazy λ-Calculus: An Investigation into the Foundations of Functional Programming, PhD Thesis, Imperial College, University of London, 1988.

ちょっとこれらの論文を読んでみたくなった。『A domain equation for bisimulation』はPSファイルが見つかったのでまずこれを読んでみよっかな。

関連エントリ

• newtypeはHaskellの仕様に不要では?

λ. 小泉首相の靖国神社参拝

少し前に『「いつ参拝しても批判されるなら、公約通りに断行した方が潔い」(首相周辺)との判断に傾きつつある』という記事を読んで、今年は終戦記念日に参拝してくれるんだろうと期待してたので、元旦の参拝にはビックリした。元旦に参拝するのも悪くはないと思うけど、年一回参拝という公約を考えると、今年も終戦記念日には参拝しないんだろうなぁ。はぁ(ため息)

λ. 新年会

いつものメンバーでカンフーハッスル観て、La Pausa でご飯食べて、ダーツ投げて、マリオカートして、以下略。

λ. カンフーハッスル

正直「少林サッカー」の方が面白かった。

λ. 「友人のいない自作改造マリオ」

ニコニコ動画の友人のいない自作改造マリオpart1のシリーズの動画にはまる。 後になると飽きてくるし、最初の方が面白いな。 って、こんなことしている場合じゃないのに……

λ. 『iPod touch/iPhoneを楽しく使うためのハッキング』 武藤 佳恭

naoeの日記 (2008-11-17) より。 iPod touch も iPhone も特に買う予定はないのだけど、直江さんが「日本語でOtterに関して述べられている初めての本のような気がする」と書いていたので、買ってみた。

Otterに関しては、iPodへの入れ方と、「正直者と嘘つき」と「組み合わせ回路の難問題」(参考: Otter で 3 not problem を解く - ヒビルテ(2008-07-18))を解かせる例が載っているだけで、使い方のちゃんとした説明等は載っていなかったので、ちょっと残念*1。

全体としては、「それはちょっと……」と思う記述も結構とある*2が、iPod touch/iPhone で遊ぶためのとっかかりとしては良さそう。 iPod touch/iPhone、ちょっとだけ欲しくなってきた。

λ. TAS　スーパーマリオカート　150ｃｃ全カップ　21:27.02

ちょっwww　これはひどいチート。

λ. 新年会

.

λ. 2016年の目標

2015年の振り返りを踏まえて、2016年の目標を幾つか。

• SMT-COMP 参加
• MOOCの受講 x3
• 発表 x2
• 勉強会やイベント参加頻度を増やす
• プログラミングコンテストとかセキュリティとかはまあボチボチと
• 語学はコツコツと
• どっか海外旅行
• ランニング 400km
• フルマラソン