2001-07-16
λ. 記号処理プログラミングでミニプロの発表をした。名簿を見ると、Lispのコンパイラを作った人とかもいるみたいでレベルが高い。もっとも、その人は欠席してて発表を聴くことは出来なかったんだけどね。
λ. 昼食
は学食で、アサリとイカのスパゲッティにコーンスープ。しかし、このコーンスープの薄さといったら…
2002-07-16
λ. 台風去来。雨がすごい。こういう雨は好き。でも、昼ごろには止んでしまった。どうせならば一日中降っていれば良かったのに。
λ. 情報数学Ⅱ
「Horn節」が一瞬「Hom節」に見えた。疲れてるな。この授業も今日で終りだけど、難しかったのは、やっぱ確率/統計の話だったよ。それに比べれば、情報理論や論理の話は簡単すぎた。
λ. Content-Type: application/xhtml+xml
そういえば、Mozillaはtext/htmlだとMathMLとSVGをレンダリングしてくれなくて、仕方なくapplication/xhtml+xmlにした事もあったなぁ……
λ. スケジューリング
referential transparency が保証されているとスケジューリングがやりやすいというのは理解できるけど、実際どれくらい効果があるのだろう。どっかに定量的な評価がないものか。
λ. Re: 独り勝ち慶応に陰り？
大学コンサルティング会社「ベガ」の後藤健夫氏も「慶応ＳＦＣはコンピューターと語学が売り物だったが、今ではどこの大学でもやっている。ＳＦＣのイメージバブルがはじけ、受験生離れが加速した」。
いわゆるコンピュータが売り物のひとつではあったけど，環境があるのと学生が使いこなせるのとは別の話．SFC にいる人は皆コンピュータの知識があって云々とか思われがちだけど，中には電子メイルさえ使えない人もいる．
さすがに電子メールすら使えない人はいない……と信じたい脳。というか、メールで提出の課題って少なくないと思うのだが、そういう人って一体どうやって卒業(した|する)のだろう。
よくSFCはコンピューターと語学が注目されるらしいけど、 履修できる授業に学年の縛りが原則的に無い事や、 1年でも研究室に所属できる事の方が印象的だったなぁ (他の大学の事は知らないので比較できないけど)。 語学やコンピュータよりもこういうのを売りにすれば良いのにとは時々思うのだけど、 きっと難しいのだろうなぁ。
まあ、別に学校名に期待してるわけでもないので慶應凋落も全然構わないけど、 せめて口にだして恥ずかしくない大学くらいではあって欲しいと思う。
まぁ，環境が整ってるといっても，最近まで SS 5 だか SS 10 だかで X 起動させて，Netscape でほげふげとかいう環境がメインだったよね．かなりキツイと思うけど．
この手の環境が保守的になるのは、まあ仕方がないんじゃないかとも思う。とはいえ、国際化パッチすら当たっていないfvwmが標準のウィンドウマネージャだったのには唖然としたね。
ちなみに、今年からは GNOME + Sawfish だったり
2004-07-16
λ. Call For Participation: Haskell Marathon
もちろん参加します。
λ. Amazon.co.jp
注文した商品の個別の発送可能時期は「通常24時間以内に発送 」から「通常2〜3日以内に発送 」で、「商品 まもなく発送されます」にもなっているのに、配送予定日が「08/16 - 09/ 1」ってどういうことよ。ファッキン。
2005-07-16
λ. 人狼審問 : (625)憎しみの村
ここ2週間ほど参加していました。初の生存勝利なのでとても嬉しいです。エピローグに無事入れたときは緊張がほぐれたからか手が震えていました。
ケネス(hanasuiさん)が独り言でいいことを言っていたので引用。
占い師同士の論戦はＮＧだな。 論戦の勝者は真偽じゃなくて、 経験の有無で決まる。
- 関連リンク
2008-07-16
![[お菓子の写真]](./images/20080716_0.jpg)
λ. 3 not problem
x,y,zの3入力, x',y',z'の3出力を持つブラックボックスがある. 入出力の関係は
- x' = not x
- y' = not y
- z' = not z
である. ブラックボックスには, andとorは好きなだけ使われているが, notは2つしかないことが分かっている. 内部はどうなっているか.
ささださんのだいありー(2008-07-15)と、 3 not の問題 - まめめも(2008-07-16)経由で。 例によってAlloyで解こうとしたら、Alloy Analyer のバグを踏んだっぽい(追記: どうもバグではなく仕様だったっぽい)。 あと、昔Otter関係で聞いたことのある話だなと思ったら、<URL:http://www-unix.mcs.anl.gov/AR/otter/examples33/program/two_inv.in> にあった。
λ. Alloy で 3 not problem を解く
以下のような感じで書いたのだけど、Alloy Analyzer にかけたところ、残念ながら数時間程度では解けない感じだった。Otterでやっているように、真理値表を8bit整数で表してビットごとのandやorで操作できると、もうちょっと効率よくなりそうなんだけど、今のAlloyにはそれらのビット演算はないのだった。ビットシフトはあるのに……(涙
/*
The 2-inverter puzzle.
The problem is to build a combinational circuit with 3 inputs
and 3 outputs, such that the outputs negate the inputs; we can
use as many AND and OR gates as we wish, but at most 2 NOT gates.
*/
abstract sig Bool {}
one sig True, False extends Bool {}
abstract sig Node {
t : set (Bool -> Bool -> Bool)
}
sig Not extends Node {
i : Node
}
abstract sig Op2 extends Node {
i1 : Node,
i2 : Node,
}
sig And, Or extends Op2 {}
one sig X,Y,Z extends Node {}
pred v[n : Node, a : Bool, b : Bool, c : Bool] {
(a->b->c) in n.t
}
fact {
no n : Node | n in n.^(i + i1 + i2)
all a,b,c : Bool {
v[X,a,b,c] <=> (a=True)
v[Y,a,b,c] <=> (b=True)
v[Z,a,b,c] <=> (c=True)
all n : Not | v[n,a,b,c] <=> !v[n.i,a,b,c]
all n : And | v[n,a,b,c] <=> (v[n.i1,a,b,c] && v[n.i2,a,b,c])
all n : Or | v[n,a,b,c] <=> (v[n.i1,a,b,c] || v[n.i2,a,b,c])
}
}
pred show() {}
run show for 10
pred two_inv {
some n1,n2,n3 : Node {
all a,b,c : Bool {
v[n1,a,b,c] <=> !v[X,a,b,c]
v[n2,a,b,c] <=> !v[Y,a,b,c]
v[n3,a,b,c] <=> !v[Z,a,b,c]
}
}
}
run two_inv for 25 Node, exactly 2 Not
2012-07-16
λ. ICFP Programming Contest 2012 “Lambda Lifter”
連休中は ICFP Programming Contest 2012 を割と頑張ってた。 いつものメンバーのTeamSampouで参加(使用言語はHaskell)。 今回は仕様も簡単でとっつきやすくて良かった。が、結局今年も大したことはできなかったけれど。
今回は昨年の田中さんたちを真似て、githubのプライベートレポジトリを使ってみた。(コンテスト終わったので、公開済み)
概要
採掘ロボのプログラムを書く問題で、2次元のマップが与えられていて、穴を掘ったりして地中にあるラムダをすべて回収して、ゴールに移動するのが目的。ただし、障害物として岩があって、下が安定しない岩はある規則にしたがって下に落ちたり転がったりして、岩の下にいると潰されて壊れたり。岩の下を掘ると岩は不安定になるし、あと岩を押して動かしたりもできる。 問題文を読んで(& そこで使われているレトロなドット絵を見て)、ディグダグと倉庫番を連想。といっても、どっちもちゃんと覚えていないので、どれくらい似てるのかは良くわからんけど。
戦略
色々考えていたことを、忘れないうちにメモしておくく。
最初に考えたこと
最初に漠然と考えたこと
- スタート地点と各ラムダとゴールの間の距離を(貪欲法なりなんなりで)近似計算
- 巡回セールスマン問題を解いて回る順番を決める
- その上で岩に潰されたりしないよう経路を局所的に調整
ただ、サンプルのマップをみると、結構パズル的要素が強く、局所的な調整では調整しきれないだろうなぁという印象だったので、断念。
- 次に考えたのは、岩を動かしてパズルを解くのが倉庫番に似ていて、倉庫番はPSPACE完全で、同じくPSPACE完全な QBF satisfiability のソルバ(QBFソルバ)を使って解けないかというもの。ただ、ググってみてもQBFでパズルを解いたりとかいう情報はあまりなかったので、断念。
実装した戦略
- ランダム
- ランダムは制限時間までランダムなプレイをひたすら生成して、一番スコアの良かったものを返す
- 本命ではなく、あくまでチームメイト向けのアルゴリズムの書き方のサンプルというつもりだったので、あまりやる気なかった。
- とりあえず1ステップ先読みはして、1ステップ後に壊れるやつは選ばないように
- 幅優先
- 部分タスクではなく全体を幅優先で探索するやつ。当然だけど、メモリを食い尽くして死ぬ。
- これもサンプル的に書いたつもり。あと、後で部分タスクを解く部品として再利用するつもりだったけど、結局使わずじまい。
- 深さ優先で一番近いラムダに向かうやつ
- これもサンプル＆後の再利用向けに書いたけど、結局使わず仕舞い。
- モンテカルロ木探索的なもの。
- 割と本命だったんだけど、うろ覚えで書いたら、うまくいかず。
モンテカルロ木探索的なものを書くのに時間がかかってしまって、その割にうまくいかず、結局ランダムなやつが一番成績が良かったので、それを投稿。 なんか最近こういうパターンが多い気が……
ただし、時間切れ直後にトランポリンへの移動をすべて枝刈りしてしまっているというアホなバグが発覚…… orz
実装したかったこと
実装したかったけど、できなかったこと。 実装しようと思っていた順。
- 複数アルゴリズムのポートフォリオ
- AI/CSP的アプローチ、プランニング
- conflict analysis と nogood の学習
- うまくいった手筋の記憶と再利用。うまくいった手筋の「事前条件」を解析しておいて、盤面がそれを満たすならそれを優先的に試すなど
- 最初のタスクの集合は、スタートと各ラムダとリフトの間の移動としておいて、あとはconflict analysisの結果から、タスクを追加
- SAT(やPBO)で有界モデル検査(Bounded Model Checking; BMC)
- conflict analysis とか学習とかしだすと、自分で書くよりもSATソルバの内部に実装されているものを活用した方が速いのではという発想。SATソルバ速いし。
- ただ、「各ステップの各セルが各種類」という風に変数をとると、共通の原因であってもステップが違うと違う補題になってしまって、学習結果の再利用が効かなそう。エンコードの工夫をしないといけないかも。(良く知らないんだけど、SatplanみたいなSATベースのプランナーは、その辺りを考慮したエンコーディングをするのかな？)
- 完全なソルバを使うことしか考えてなかったけど、今考えるとwalksatやGSATみたいな不完全なソルバを使う手もあったかも。
- GA等のメタヒューリスティクス
- 詳しくないので自分には難しいだろうと思い断念してた。
反省?
今回のは、少なくとも以下の5人くらいで分業できると良かったのかなぁと思った。
- シミュレーターの改良(高速化と新仕様の取り込み)をする人
- 盤面の評価関数やスコアの上界値計算を書く人
- 部品としての探索アルゴリズムを書く人
- 部品を利用した上位の戦略を書く人
- 人手で問題を解いて、色々考えたり、同時にシミュレーターのバグを見つける人
アホなバグの件に関して思ったこと:
- バグの箇所は最初に書いたっきりずっと使ってなくて、仕様変更への追従漏れしてて、後半に使いだしたため。こういう使ってないコードはいっそ消すかコメントアウトするかしておいた方が、変更漏れしたまま使ってしまう危険を避けられるのかなぁ。
- シミュレーターに関してはHUnitを使った簡単なテストをしてたんだけど、問題のあった箇所はシミュレーターでは使っていなかった箇所だった。また、探索アルゴリズムについては、最初のころに書いていたのはサンプルくらいのつもりだったので、テストを用意していなかったし、終盤は逆にテストを書いてる余裕がなくなってしまっていた。
