2011-11-25

パズル的な問題を知識論理で書いてみた

論理

こんな問題見かけました。

2≦m≦n なる自然数(m,n)に対し，Aはm*nの値のみを知っている，Bはm+nの値のみを知っている．A「m+nの値は分からない」B「君がそう言うことは分かっていた」A「まだm+nの値は分からない」B「m+nは14未満だ」A「mとnが分かった」B「私も分かった」さてm,nは？
http://twitter.com/#!/kakenman/status/139943992283496448

こういうのを一度きちんと知識論理使って書いてみたかったのでやってみた。

$W_0 = \{ (m, n) | 2 \leq m \leq n \}$
$(m, n) R_A (m', n')$ iff $mn = m'n'$
$(m, n) R_B (m', n')$ iff $m+n = m'+n'$

として， $W \subset W_0, x \in W$ に対して $x ||\hspace{-5}- !_A$ を「 $x R_A y, y \in W$ ならば $x=y$ 」であることと定義しましょう。 $!_B$ も同様に定義します。このとき

$W_1 = \{ x \in W_0 | W_0, x ||\hspace{-5}- K_B \neg !_A \}$

とすると，これは A「m+nの値は分からない」B「君がそう言うことは分かっていた」のやりとりが発生しうる (m, n) の全体となります。以下同様に

$W_2 = \{ x \in W_1 | W_1, x ||\hspace{-5}- \neg !_A \}$
$W_3 = \{ (m, n) \in W_2 | m + n < 14 \}$
$W_4 = \{ x \in W_3 | W_3, x ||\hspace{-5}- !_A \}$
$W_5 = \{ x \in W_4 | W_4, x ||\hspace{-5}- !_B \}$

がそれぞれ A「まだm+nの値は分からない」B「m+nは14未満だ」A「mとnが分かった」B「私も分かった」に対応して，最終的に $W_5$ に入っているものが解となります。

たぶん。

2011-10-27

MLG meeting

近況雑記

MLG meeting に参加していたので，感想みたいなもの。

前から思っていたことではあるけど，もっといろんな本や論文を読んで，論理のいろんな見え方を知りたい。多値論理と直観主義論理とか，僕が知らないだけで，もっと密接に関係しているんじゃないか，とか思った。

多値論理については，単にそういうものが存在するという事実とか，形式的な定義だけは本を読んでなんとなく知っていたりするけど，それだけじゃあまり意味がないんだと思う。もっと気持ちの部分まで自分なりに理解しておきたい。そうすることで視野が広がりそう。

2011-10-02

GCJ Japan 2011 予選

programming contest GCJ

参加しました。夕方までバイトしてたので空き時間に問題だけ見て，終わってからコード書きました。

A は，カットの回数が少ないのでシミュレーションでできるんだろうと思ったらできました。けどちょっとめんどくさかったです。こういう手続きを書くのは苦手なので，まず紙に擬似コード書いてからと思ったんですが，紙にうっかり OCaml のコードを書いてしまったので OCaml で実装することになりました。space separated list of integers な入力の読み方がしばらくわからなくて困りました。

B は問題文全体の雰囲気から DP かなあと思ったけど実際に問題文読んでみたらそうでもない感じで，じゃあなんとなく LP だろうかと思ったりしつつ放置しました。他の問題を解いた後でよく考えてみたら貪欲でできるみたいです。日付の後ろのほうから満足度が大きいものを取っていきます。実装終わらなかったのですけど，たぶん。

C は少し考えてもよくわからなかったので，これはたぶん人の手ではなく宇宙の神秘により解けるんだろうと予想して，とりあえず bruteforce しました。そうするとやっぱり規則性がありそうなので，たぶんそういうことなんだろうと思って submit したら通りました。

2011-09-11

skk-comp + auto-complete のようなもの

emacs customize

skk の補完機能，補完候補一覧が出てほしいなと思っていて，探したけどみつからなかったのでなんとなくそれっぽく書いてみた。

(defun mylib-ac-source-skk-comp-candidates ()
  (when skk-henkan-mode
    (skk-comp-get-all-candidates (buffer-substring-no-properties
                                  skk-henkan-start-point (point))
                                 nil skk-completion-prog-list)))
(add-to-list 'ac-trigger-commands 'skk-insert)
(defvar ac-source-skk-comp
  '((candidates . mylib-ac-source-skk-comp-candidates)
    (prefix . "▽\\(.+\\)")))
(setq-default ac-sources (cons 'ac-source-skk-comp ac-sources))

2011-08-04

suspend/hibernate から復帰後にマウスポインタ消える

Linux

という現象が起きていたので直し方を探しました。

/etc/pm/sleep.d/99mousecursorworkaround (ファイル名は先頭の 99 以外は適当) に

#!/bin/sh

case "${1}" in
  hibernate)
    #nothing
    ;;
  resume|thaw)
    chvt 1
    chvt 7
    ;;
esac

みたいなのを置いて chmod +x してやるとよいらしいです。どこかに転がってたのほとんどそのままですが。

復帰後に modprobe appletouch してもよいみたいなんですけど sleep.d の下に置くとうまくいきませんでした。99 だとタイミングが早すぎるとかだろうか，よくわからないのですが。

2011-07-31

Ubuntu 10.04 で stumpWM の続き

Linux stumpWM

http://d.hatena.ne.jp/lkozima/20110212/1297478453 に書いたやり方だと /usr/bin/stumpwm を書き換えてたんだけど，そんなことしなくてもよかったのでしない版。

/usr/share/xsessions/stumpwm.desktop を

[Desktop Entry]
Name=StumpWM
Comment=This session logs you into stumpWM
Exec=env LISP=sbcl stumpwm
Icon=
Type=Application

のようにすると，それだけでよいらしいです。Exec のところを直しました。環境変数 LISP に使う処理系を入れておくとそれが優先されます。

2011-07-26

Ubuntu インストール後にとりあえず入れたものたち

memo ubuntu

新しい PC に Ubuntu インストールしてからとりあえず使えるようになるまでに入れたものメモ。

lv: なんか常用してるけど入ってなかったので。
stumpwm: ウィンドウマネージャ。clisp と sbcl が黙ってても一緒にインストールされました。
emacs23: これがないといろいろなことができない人です。
emacs23-el: よくソースを見たくなるので。
ddskk: ないと日本語の入力に困る人です。
libnotify-bin: たまに emacs から notify-send を呼びます。
cl-clx-sbcl: clisp が cl-ppcre のロード中にこけるので stumpwm を sbcl で使おうとしたら要求されました。
ccrypt: ファイルの暗号化をします。emacs 経由で使ってます。