日々の流転

λ. しまった。昨日はナカジ企画の花火大会をすっかり忘れてた。最近こんなのばっかで嫌になる。

λ. グローバル経済を動かす愚かな人々

だがここで、疑問を抱く人もいるかもしれない−すべての追加生産を吸収できるほど消費者需要は十分に上昇するという私の想定には根拠があるのだろうか?　もし、生産高が二倍になり、そのすべてが売られるなら、当然、全体の収入も二倍になるであろう。そうならば、なぜ消費が二倍にならないのであろうか?　すなわち、経済が単に生産量を増やしただけなのに、なぜ消費が落ち込まなければならないのか、ということである。

λ. はい、疑問を抱きます。限界効用は逓減するし、限界消費性向は通常は1より小さいし、こんなんで納得出来るわけないじゃん。でも、まてよ。遅かれ早かれ収入は消費に回ることになるはずだから、金融政策さえ………………………………やっぱ、わからーん。

λ. バイオハザード

ケシゴムがバイオハザードやってるなんて…　そんなのイメージ違うよー　えーん。

λ. Color space FAQ

ChangeLog for wl-ja.texiより

λ. Re: [I18n]mb/wc Xft API (Re: ISO 10646 Fonts and XFontSet question)

Li18nuxのダイナミックローディング用のコードってまだマージされてないんだっけ?　あれをマージすれば容量に神経質になる必要は無くなるんじゃないの?

λ. そもそもXftってXのエクステンションなんじゃないの?　なら、Xの流儀に従ってmb/wcのAPIも実装すべきでは?　依存性は増えるけど、それによってサイズが肥大するわけでも無いし。

λ. あれ、li18nux.orgに繋がらないや…

λ. 「霞が関が震えた日」

読書をして一日過ごす。今読んでるのは塩田潮の「霞が関が震えた日」という本で、ニクソンショックを扱っているのだけど、僕はこういう事件を歴史の年表に出てくる名前としてしか知らなかったのだなぁ……と感じた。

金・ドルの交換停止—。日本経済が凍りつくようなニクソン・ショックが突如日本を襲った。大蔵省を筆頭に政府官庁・日本銀行をはじめ、都市銀行、証券、商社はいかなる対応をしたのか。戦後経済史最大のナゾとされる通貨戦争の内実を徹底取材によってはじめて明らかにした講談社ノンフィクション賞受賞作品。

λ. Functional Programming with Overloading and Higher-Order Polymorphism

.

λ. EUC/SJIS/JIS/UTF-8の判断ルーチン

そういえば現在のNKF.guessはSS3をSHIFT_JISと誤認するので、それも直ると嬉しいです。とか書いてみる。

λ. GGX

全然関係ないけど、イノいーよね。

λ. Classクラス

RubyではClassクラスの継承は禁止されている。特定のクラス群を独自の方法でマーシャリングしたい場合にはどうしたら良いか?

λ. -no-undefined

こないだatkのDLLを作れなかったのは、libtoolに-no-undefinedオプションが指定されていなかったのが原因だった。configure.inとMakefile.amを見るとmingwの時は指定されるようになってるので、この辺をpangoやgtkに合わせてゴニョゴニョすれば良い。後でパッチを送ろう。

λ. お昼

ゲンキョウワンというタイ料理屋さん。

λ. PPL Summer School 2003

なんか愛知まで行くのが面倒になって、結局申し込まなかった。パラメトリシティ原理の話とか結構聴いてみたかったんですけどね。

λ. MAD PEOPLE 用の発言ポップアップスクリプト

madpeople-message-popup.user.js

本体からポップアップ機能が無くなってしまって不便なので、例によってGreasemonkeyのスクリプトとして作った。というか、人狼審問用に作ったものを数行書き換えただけだけど。

使い方

詳しくはそれぞれのブラウザ等のドキュメントを参照。 また、Wikiにあるページも参照のこと。

Firefox の場合

1. Greasemonkeyをインストール
2. madpeople-message-popup.user.jsのリンクをクリックするとダイアログが出てくるので「Install」を選択 (古いGreasemonekyの場合には、上記リンクを右クリックしてInstall User Scriptを選択)

Opera の場合

1. このスクリプトをダウンロードし、「ツール」メニューの「設定」「詳細設定」「コンテンツ」「JavaScriptオプション」「ユーザーJavascriptファイル」で指定したフォルダに置く。

Internet Explorer 6 の場合

1. TurnAboutをインストール
2. madpeople-message-popup.user.jsのリンクを右クリックして出てくるメニューの「Turnabout」「Install Script」を選択

Sleipnir 2 の場合

1. SeaHorseをインストール
2. このスクリプトをダウンロードし、[Sleipnir インストールフォルダ]\plugins\seahorse\ に置く。

他のブラウザ

ユーザージャバスクリプト的な仕組みを持たないブラウザであっても、ブックマークレットを使ってこのスクリプトを読み込むことは可能です(面倒ではありますが)。MAD PEOPLE 発言ポップアップ (bookmarklet) をブックマークして試してみてください。

古いバージョン

• madpeople-message-popup-20060902.user.js

λ. 女子高専生殺害の容疑者、バイクで逃走か

桐野夏生の『リアルワールド』を少し連想した。 どうでも良いが。

λ. Schemeのsyntax-rulesがようやく理解できた気がする

昨日のcut-seaさんのツッコミをきっかけに、Schemeのsyntax-rulesがようやく理解できた気がする。「...」が面白い。

λ. NPR (National Public Radio)

英語の学習に NPR (National Public Radio) が良いという話を聞いた。「Podcastはあるかな?」と思って見てみたら、500以上もあって、どれを聞いたら良いか迷って困る……

【2007-10-28追記】 最近は以下の二つを少し聴いている。

• WNYC's Soundcheck
• NPR: Story of the Day

λ. あろは先生を問い詰める会 (ET Seminar)

あろは先生を問い詰める会というイベントに参加。

• スライド
• ホワット・ア・ワンダフル・ワールド 東京行ってきました

これはなんと、あろはさんが7時間ぶっ続けで発表し、問い詰める気満々の聴衆からすごい勢いでツッコミと質問が入るという恐ろしいイベントだった。 ツッコミまくってたお前が言うなという気もするけど。 特に、あまり本質的でない質問や、勘違いした質問を結構してしまって、そこはちょっと反省。 そんな過酷な環境にもかかわらず、長時間にわたって忍耐強く続けてくださったあろはさんには感謝するとともに賛辞を送りたい。

こないだの論文とあわせて、ETの目指すものと現状について大体理解できた気がする。

以下はとりあえず自分がした質問を中心に簡単に、感想や聞きそびれてしまったことなども含めてメモ。

命令型の理論とか仕様とか

ホワット・ア・ワンダフル・ワールド ET Q&Aでは「仕様 (what) の概念無し」、今回のスライドでも「そもそも理論が無い (あるけど，後付け （現場の要請ドリブン）)」と書いてあった。

そこで、「命令型言語でもホーア論理とかで仕様書けるし、最近JMLとか少し流行ってるよ」と聞いたら、ここで仕様と呼んでいるものは解きたい問題を記述したもので、関数の性質とかを記述したものではないとのこと。仕様をそう定義すれば確かにそうなんだけど、うーん……。

あと、他の方から「JMLとかは仕様ではなくアサーションでは」というコメントがあった。私の理解では「アサーション」は満たすべき性質の一部を記述したもので、「仕様」は満たすべき性質の全てを記述しつくしたもの。JMLはそのどちらも記述可能。

それから、命令型言語における仕様からの合成という話では、refinement calculus みたいな古典的な話もあるので、その辺りも少し質問してみたけど、仕様の概念が違うこともあって、あまり比較対象にはされていないような感じだった。

notは無理筋?

「notの定義例」のスライドでは後で書く否定の種類の方面の話に気をとられていたけど、落ち着いて考えると、ET 版の not が Prolog 版 not の問題を解決しているのか良く分からない。 というのも、結局PrologのSLD導出アルゴリズムの手続き的性質に依存していたのが、Dルールの手続き的性質に依存するようになっただけで、今回のセミナーではあまり触れられていなかったDルールの理論的扱いがわからないと何が変わったのか分からないので。

また、リファレンスマニュアルのnotの項の「(not *s)」の説明で「notは副作用を起こします。*s中の変数が実行中に変更されると、共有するnotの外側の変数も変更されます。この変更は、結果の真偽によりません」とあるけど、これはPrologの問題よりも遥かに凶悪なような気がする。 あろはさんも「条件部の結果が本体にひきずるのは問題」「実装で解決できるかも」というようなことを言っていた。

否定の種類

「notの定義例」というスライドのところで質問したが、利点として<URL:http://assam.cims.hokudai.ac.jp/et/indexj.html>に「否定を含む問題を正しく扱える」とあったのが気になっている。 Prolog でも negation as failure については問題なく扱える*1ので、これは negation as failure ではない通常の否定(classical negation とか strong negation と呼ばれる)を扱えるといっているのだろうか。

あろはさんによると、最近、DL(Description Logics) を扱う関係で ET で真の否定を扱える理論(?)が出来たとか。 論理プログラミングの文脈だと、通常の否定を扱うためには解集合プログラミング(answer set programming, ASP)のような枠組みが必要になってくるが、これは理論的にはともかく実装技術としては問題領域を限定した技術だと思う。 広い問題領域を対象としたETに対して実装されるとしたらどのような形になるのか興味深いところ。

構成的プログラミング

前日の LL Future での Lightning Talk 「超未来言語Gallina」で「仕様を効率的に実行可能な形に等価変換していくことを実現したのがGallina(Coq)」だと断言したyoshihiro503さんと、「Coq等はルールのように分解可能性のある(単体で正当性が議論できる)コンポーネントの集合で構成されているわけでない」というあろはさんとのバトルをちょっと期待してたんだけど、特にそんなことはなかった。

それはそうと、効率に関しては確かにちょっと問題はあるのかもと思うこともある。 というのも、Coqで書ける*2のは停止性が検査機によって自動的に判定出来る関数だけで、停止性が自動判定出来ない関数定義は書けないため、効率的だけど停止性が自動判定出来ない関数を書けずに問題になる場合が本当に無いのか自信がないため。Coqで“無限オブ無限”を書いたときにもちょっと思ったんだけどね。

palpal問題

ETの論文でよく出てくるpalindromeの例がpalpal問題と呼ばれてるのね。どうでもいいが、最近やっている英語版の逆転裁判で Detective Gumshoe (糸鋸刑事) が pal という呼びかけを頻繁に使っているので、それを連想してしまって、少しツボだった。

肝になる5番目のルール rv(*x, *y), rv(*x, *z) ⇒ {=(*y, *z)}, rv(*x, *y). にみんなの質問が集中していて、その結構な部分が「証明できる」が指すことについてだった気がする。

結局、このルールを自動導出出来るようになったのが最近というのは良いのだけど、「本当に厳密に D に対して ET ルールであることが証明可能になったのは，つい最近」というのが機械による自動証明だけを指しているのか、人間による証明についても不可能だったのかがよく分からなかった。

プライオリティ

これは私の勘違いでした。済みません。

(後で書く)

特殊化システムと書き換え系

「書き換え系としては多重集合の書き換え系(+情報変数)と思ってよいのか?」と聞いたら、その通りとのこと。多重集合の書き換え系なら線形論理の証明探索を書いたりするのに便利かもと思った。

それから、情報付き変数を使って特殊化システムを拡張可能とのこと。

書き換え系という意味では、Maudeの代数的仕様記述+書き換え論理という枠組みとの比較なんかも質問してみたかったが、これは質問しそびれてしまった。

圏論による定式化?

仕様空間とプログラム空間の理論は、channel theory とか chu space とか institution とか良くあるやつに似ているので、良くあるような感じで定式化してやれば良いのではないかと。 それで何か嬉しい結果が出てくるかはわからないけど。

あろはさんの研究とか

スライドにはあまり書いていないけど、私の理解では「命令型言語のプログラムの空間からETプログラム(Dルール)の空間への埋め込みを定義して、その逆変換としてDルールから命令型言語へのコンパイルを定式化」というのを一つのアプローチとして考えていたようだだった。

ただ、プログラムの埋め込みは仕様を何らかの意味で保たなくてはならないはず*3で、その部分があまり考えられていない気がして、その辺りを質問してみた。

そして、その議論からどうもDルールで副作用のあるアトム(?)の扱いが仕様上どう扱われているのかが気になりだして、それも聞いてみた。unification が substitution を生成するのと同じ扱いで、副作用については世界の枝分かれみたいな感じで扱われるとか。 ただ、一方でDルールにはNルールと違って正当性の概念がない(?)とか、どうもあまり理論的には扱われていないようでもあった。

ネタとかどうでも良い点とか

• S式版の記法で使われているasはassertの略でprolog-kr由来
• 『仕様からの合成』と要約してしまうとLyeeと同じになってしまってアレ
• 闇世界仮説。
• 高階質問状
• 「すごいパーツをいれれば僕はすごくなるよ」

他の方の感想など

• 埒を明ける日々: ET Seminar
• LLFuture と、等価変換セミナーに行ってきた - にわとり小屋でのプログラミング日記
• 等価変換理論集中セミナー2008（at 溜池某所） - ヤドカリデンキ商会（第一倉庫）
• 2008-09-03 - 兼雑記
• とりあえず俺はProlog知らなすぎだ - soutaroにっき
• <URL:http://morihyphen.hp.infoseek.co.jp/log2/200808.html#083118>
• <URL:http://page.freett.com/shelarcy/log/2008/diary_08.html#haduki312008>
• 8月31日は問い詰める会 - YasuyukiMiuraの日記

λ. Agda2でクイックソート

LLTV後の飲み会でranhaさんが、クイックソートの停止性をAgda2の停止性チェッカに説得できないというような事を話していた(参考: 修行失敗 - Yet Another Ranha (2009-08-27))ので、Agdaさんを説得してみた。 基本的には length (filter p xs) ≦ length xs の証明 と Wellfounded induction in Agda2 で書いたのを組み合わせただけなんだけど、Agda2のライブラリの使い方を調べるのが面倒くさかったよ……

module Quicksort where

open import Data.Bool
open import Data.Nat
open import Data.List
open import Relation.Binary using (Rel)
import Induction.WellFounded as WF
open WF using (Acc; acc)
open WF _<′_ using () renaming (Acc to <-Acc)
open import Induction.Nat using (<-allAcc)

R : ∀ {A} → Rel (List A)
R {A} xs ys = length xs <′ length ys

R-allAcc : ∀ {A} xs → Acc (R {A}) xs
R-allAcc xs = f xs (<-allAcc (length xs))
  where
    f : ∀ xs → <-Acc (length xs) → Acc R xs
    f xs (acc rs) = acc (λ ys h → f ys (rs (length ys) h))

s≤′s : ∀ {m n} → (m ≤′ n) → suc m ≤′ suc n
s≤′s ≤′-refl = ≤′-refl
s≤′s (≤′-step h) = ≤′-step (s≤′s h)

length-filter
  : ∀ {A} → (f : A → Bool) → (xs : List A)
  → length (filter f xs) ≤′ length xs
length-filter f [] = ≤′-refl
length-filter f (x ∷ xs) with f x
... | true  = s≤′s (length-filter f xs)
... | false = ≤′-step (length-filter f xs)

length-filter′
  : ∀ {A} → (f : A → Bool) → (x : A) → (xs : List A)
  → length (filter f xs) <′ length (x ∷ xs)
length-filter′ f x xs = s≤′s (length-filter f xs)

quicksort′
  : ∀ {A} → (A → A → Bool) → (xs : List A)
  → ((ys : List A) → R ys xs → List A) → List A
quicksort′ _≤?_ [] f = []
quicksort′ _≤?_ (x ∷ xs) f = f ys ys-lem ++ [ x ] ++ f zs zs-lem
  where
    ys = filter (λ y → y ≤? x) xs
    zs = filter (λ y → not (y ≤? x)) xs
    ys-lem : R ys (x ∷ xs)
    ys-lem = length-filter′ (λ y → y ≤? x) x xs
    zs-lem : R zs (x ∷ xs)
    zs-lem = length-filter′ (λ y → not (y ≤? x)) x xs

quicksort : ∀ {A} → (A → A → Bool) → List A → List A
quicksort {A} _≤?_ = wfRec (λ _ → List A) (quicksort′ _≤?_)
  where open WF.All R R-allAcc

参考

• Coqで、クイックソート - にわとり小屋でのプログラミング日記(2008-03-08)