檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2012-02-28 (火)

足が速いと有利

| 13:17 | 足が速いと有利を含むブックマーク

長男:「日本代表に選ばれた宮市ってね、50メートル5秒台で走るんだって」
父親:「へー」
長男:「永井も速いよ、5秒8だったかな*1
父親:「すごいなー」
長男:「サッカーは足が速いほうが有利だからね」
父親:「そりゃサッカーだけじゃないでしょ、どんなスポーツだって足が速いと有利だろ」
長男:「ゴルフも?」
父親:「ん、ゴルフか。まー、あれは走ったりしないか」
長男:「冬のスポーツだと、カーリングはどう?」
父親:「カーリングはー、走っちゃダメだな」
長男:「あと、アーチェリーね」
父親:「ああ、動かないほうがいいね」
長男:「射撃も」
父親:「アーチェリーと同じようなもんかな」
長男:「乗馬」
父親:「馬の足が速いと有利だろ」
長男:「人は馬の上で走らない」

猫はいない

| 16:11 | 猫はいないを含むブックマーク

子供の頃(つっても高校まで)猫を何匹も飼っていました。当時、セーターに猫の白い毛が付いて嫌だなーと思っていたわけですが、今もセーターに白い毛が付いて嫌だなーと思っていますがね。

白髪の抜け毛ね。あーもう、イヤッ。

*1:ちょっと調べたところ、この二人はロッペンやクリスチャーノ・ロナウドよりも速いみたい。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20120228

2012-02-24 (金)

ワタミ従業員の過労・自殺に関して

| 16:15 | ワタミ従業員の過労・自殺に関してを含むブックマーク

飲食業じゃなくてソフトウェア関連だけど、このテの話題に対して僕が思っていることは、

から辿れるエントリーに書いてあるので、いまさら言うことはないです。それと、

ソフトウェアのインストールや更新はやっぱりメンドクサイ

| 10:58 | ソフトウェアのインストールや更新はやっぱりメンドクサイを含むブックマーク

僕はソフトウェアのインストールとか更新とかはメンドクサイので嫌い。だけど、Mercurialを1.4.3から2.1にして少しハズミがついて、IPython(http://ipython.org/*1を入れる気になりました。http://ipython.org/download.html から ipython-0.12.win32-setup.exe をダウンロードしてインストール後に起動してみると、

    hlen_b4_cell = self.readline.get_current_history_length()
AttributeError: 'module' object has no attribute 'get_current_history_length'

と言って起動失敗。

>>> dir(readline)

で調べてみると、get_history_length はあるけど、get_current_history_length はないですね。PyReadline(http://ipython.org/pyreadline.html)が古いらしい(pyreadline-1.5-win32 を使っていた)。https://launchpad.net/pyreadline/+download (最新版のソースは https://github.com/pyreadline/pyreadline)から pyreadline-1.7.1.win32.exe をダウンロードしてインストール。

これで、IPythonは動くようになりメデタシメデタシ。と思ったら、Catyが動かなくなってしまいました。ガーン。

最近のPyReadlineの使い方はどうも以前と変わったようです。PyReadlineはGNU readlineが使えない環境(主にWindows)用に準備されたものなので、以前は次のようにして使用していました。

if sys.platform == 'win32':
    import pyreadline as readline
else:
    import readline

しかし最近は、こういう場合分けは不要で、単に import readline とすればいいようです。import pyreadline とすると変なことになります。

僕の環境で言えば、import pyreadline だと Python26/Lib/site-packages/pyreadline/__init__.py(のコンパイル済みファイル)がロードされ、 import readline だと Python26/Lib/site-packages/readline.py がロードされます。以前は readline.py がなかったのでしょう(1.5に戻して確認する気はない)。

プラットフォームによる場合分けは必要なくなったのですが、readlineが存在しない環境はあり得るので、結局次のようなコードが必要です(Kuwataさんが http://return0.info/note/2011-12.html#id2011-12-17 で書いています)。

try:
    import readline
except:
    readline = None
    print '[Warning] readline module is not installed.'

# ... 

if readline is not None:
     # ...

このような修正をしてCatyは起動するようになったのですが、今度はWin32 APIを使ったクリアスクリーンが動かなくなっちゃいました。

Error cls: Col 0, Line 1
Traceback (most recent call last):
  File "./python\caty\front\console.py", line 322, in default
    r = c(None)
  File "./python\caty\core\facility\__init__.py", line 308, in __call__
    r = self._command(input)
  File "./python\caty\core\script\interpreter.py", line 91, in __call__
    return self.cmd.accept(self)
  File "./python\caty\core\command\__init__.py", line 226, in accept
    return visitor.visit_command(self)
  File "./python\caty\core\script\interpreter.py", line 102, in visit_command
    return self._exec_command(node, self._do_command)
  File "./python\caty\core\script\interpreter.py", line 148, in _exec_command
    r = exec_func(node)
  File "./python\caty\core\script\interpreter.py", line 109, in _do_command
    return args[0].execute()
  File "/cls.py", line 9, in execute
  File "./lib/win32cls.py", line 67, in clear_screen
    coord, byref(dwDummy))
ArgumentError: argument 4: <type 'exceptions.TypeError'>: wrong type

argument 4: <type 'exceptions.TypeError'>: wrong type
caty:root>

今まで動いていた次のコードがエラーしてるんですよね。いかなる因果関係なのかサッパリわかりません。ムー。

# 画面クリア

def clear_screen ():
  csbi = CONSOLE_SCREEN_BUFFER_INFO()
  coord = COORD() # 初期値 coord.X = 0, coord.Y = 0
  dwDummy = DWORD()

  hConOut = stdout_handle
  if GetConsoleScreenBufferInfo (hConOut, byref(csbi)):
    FillConsoleOutputCharacterA (hConOut, 32, 
                                 csbi.dwSize.X * csbi.dwSize.Y, 
                                 coord, byref(dwDummy))
    FillConsoleOutputAttribute (hConOut, csbi.wAttributes, 
                                csbi.dwSize.X * csbi.dwSize.Y, 
                                coord, byref(dwDummy)) # ここが 67 行目
    SetConsoleCursorPosition (hConOut, coord)

動き出したIPythonでも不思議なことが起こります。Mercurialのライブラリも入れた(つうか結果的に入った)ので、IPythonからインポートしてみると:

In [7]: import mercurial.hg

^A^0;32m^BIn [^A^1;32m^B8^A^0;32m^B]: ^A^0m^B

^A^0;32m^BIn [^A^1;32m^B8^A^0;32m^B]: ^A^0m^B

文字に直して貼りつけてますが、プロンプトとしてコントロールコードが出ているようです。どうも、ANSIエスケープシーケンスを使うモードに変わっているようです。mercurial.hg のなかでコンソールに影響する設定をしてるのでしょうかね。

複雑になったソフトウェアシステムでは、予期せぬ相互作用で不具合や奇妙な現象が生じるわけですが、もうメンドクサくて追いかける気力が湧きませんなー。

[追記]

IPythonのコンソールが壊れる原因は、どうやら、mercurial/windows.py のようだ。余分な部分を削り落とすと次のようなコード。Windowsのstdoutの不具合を修復する目的らしいが、他の所ではこれが迷惑だったりする。

# windows.py - Windows utility function implementations for Mercurial
#
#  Copyright 2005-2009 Matt Mackall <mpm@selenic.com> and others
#
# This software may be used and distributed according to the terms of the
# GNU General Public License version 2 or any later version.


import sys

class winstdout(object):
    '''stdout on windows misbehaves if sent through a pipe'''

    def __init__(self, fp):
        self.fp = fp

    def __getattr__(self, key):
        return getattr(self.fp, key)

    def close(self):
        try:
            self.fp.close()
        except IOError:
            pass

    def write(self, s):
        try:
            # This is workaround for "Not enough space" error on
            # writing large size of data to console.
            limit = 16000
            l = len(s)
            start = 0
            self.softspace = 0
            while start < l:
                end = start + limit
                self.fp.write(s[start:end])
                start = end
        except IOError, inst:
            if inst.errno != 0:
                raise
            self.close()
            raise IOError(errno.EPIPE, 'Broken pipe')

    def flush(self):
        try:
            return self.fp.flush()
        except IOError, inst:
            if inst.errno != errno.EINVAL:
                raise
            self.close()
            raise IOError(errno.EPIPE, 'Broken pipe')

sys.__stdout__ = sys.stdout = winstdout(sys.stdout)

[/追記]

[追記]クリアスクリーンの問題は事情が分からないので、OSネイティブのclsコマンドを呼び出すことでとりあえず対処。[/追記]

*1:IPythonて、「高機能なPythonシェル」だと思っていたのですが、http://ipython.org/ipython-doc/rel-0.12/parallel/index.html とかを眺めると、なんか分散コンピューティングのプラットフォームを提供したりするんですね。スゴイ。

2012-02-22 (水)

最新のMercurialにした(マヌケな話)

| 17:48 | 最新のMercurialにした(マヌケな話)を含むブックマーク

MinGWbashを使ってますがWindowsです。

$ hg --version
Mercurial Distributed SCM (version 1.4.3+20100201)

Copyright (C) 2005-2010 Matt Mackall <mpm@selenic.com> and others
This is free software; see the source for copying conditions. There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

いくら何でも古過ぎるだろう、コレ。で、Mercurialを最新にしようと思い立って、http://mercurial.selenic.com/downloads/ を眺めました。mercurial-2.1.win32-py2.6.exe をダウンロードして実行したらナニカがインストールされました。が、hgコマンドのバージョンは古いまま。いったい何がインストールされたの?

$ python
Python 2.6.5 (r265:79096, Mar 19 2010, 21:48:26) [MSC v.1500 32 bit (Intel)] on win32
Type "help", "copyright", "credits" or "license" for more information.
>>> import mercurial.hg
>>> mercurial.hg
<module 'mercurial.hg' from 'c:\Installed\Python26\lib\site-packages\mercurial\hg.pyc'>
>>>

あー、そういうことだったの。まー、これはこれでいいけど、hgコマンドは更新されてないので、Mercurial 2.1 MSI installer - x86 Windows - requires admin rights をダウンロード。実行したらナニカがインストールされました。が、hgコマンドのバージョンはまだ古いまま。ハレー?

インストーラは何も聞かず/何も言わず勝手にナニカをインストールしたので、c:/Program Files/Mercurial/ を眺めてみたら、タイムスタンプが今日なので、ここに新しいMercurialをインスールしたのでしょう、たぶん。

$ which hg
/c/Installed/Python26/Scripts/hg

$ echo $PATH | tr : $'\n' | grep -i mercurial
/c/Installed/Mercurial

パスは古いほうしか通ってない。

$ /c/Program\ Files/Mercurial/hg.exe --version
Mercurial Distributed SCM (version 2.1)
(see http://mercurial.selenic.com for more information)

Copyright (C) 2005-2012 Matt Mackall and others
This is free software; see the source for copying conditions. There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

おおー、確かに新しいバージョンがインストールされている。とりあえず alias で対処:

$ alias hg='/c/Program\ Files/Mercurial/hg.exe'

$ hg --version
Mercurial Distributed SCM (version 2.1)
(see http://mercurial.selenic.com for more information)

Copyright (C) 2005-2012 Matt Mackall and others
This is free software; see the source for copying conditions. There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

この状態で使ってみると:

$ hg parent
changeset:   540:792e2f98e04c
tag:         tip
user:        ckuwata
date:        Mon Feb 20 10:21:14 2012 +0900
summary:     Issue #420に対応


$ hg st -mard
M develop\SysSpecs\schemata\astu.casm.lit
M global\schemata\set.casm
M main\root\scripts\app-graph.caty

$ hg pull
pulling from https://m_hiyama@bitbucket.org/project_caty/dev
searching for changes
no changes found

普通に使えるね。たぶん、大丈夫でしょ。

2012-02-21 (火)

普通の日本語?

| 13:46 | 普通の日本語?を含むブックマーク

2009年08月05日「キモチカッタ」:

ウチの子達もそうなんだけど、「気持ち良かった」を「キモチカッタ」って発音する例をけっこう耳にするんだよね。僕は違和感あるんだけど、5年もすると、これが普通の日本語になったりするんかなー。

今朝のNHKニュース・天気予報のとき、女性アナウンサーが「昨日はキモチカッタです」と言っていた、少なくともそう聞こえる発音をしていた。5年を待たずして普通の日本語になったのかな>キモチカッタ。

サラダバー

| 15:14 | サラダバーを含むブックマーク

去年のことなんだけど、ふと思い出した。

サラダバーがあるレストランに行ったのだけど、生野菜の上に小さな青虫がいた。田舎で育った僕には、野菜に青虫なんてどうってことはない。でも殺すのはしのびないので、「こんなんがいたよ」と青虫をそのままスタッフに渡した。と、責任者らしき人が慌ててやって来て「ほんとうに申し訳ない、あってはならないことです」みたいな勢いで謝って、「お代をいただくわけにはまいりません! それと、お詫びにドリンクのサービスもお付けします」と。

「いやいや、こっちが恐縮しちゃうな。青虫がいるのは野菜が新鮮な証拠でしょ、気にしないで下さい」と言うと、意外にアッサリ「そうですか」と。ドリンクは出なかったし、料金も普通に払った。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20120221

2012-02-20 (月)

型推論に関わる論理の概念と用語 その6:substitutionの記法

| 08:51 | 型推論に関わる論理の概念と用語 その6:substitutionの記法を含むブックマーク

とりあえず、「型推論」を「プログラマに代わって自動的に最適(?)な型宣言/型注釈を書いてくれる機能」と捉えることにしましょう。その型推論の処理のなかで単一化と呼ばれる計算が行われます。単一化(ユニフィケーション)は、型推論に限らず、式やデータ構造のパターンマッチングとして幅広く利用できる手法です。

単一化ではsubstitutionという概念を使うのですが、これがなかなかにややこしいのです。そこで、substitutionについて説明しようと思い立ったのですが、今日は記法の紹介だけ。

シリーズ目次:

  1. その1
  2. その2
  3. その3
  4. その4
  5. その5
  6. その6
  7. 番外(型理論ってば)


まず、substitutionの訳語で悩みますね。「置換の圏から代入の圏へ」では、permutationを置換と呼んだ都合から、substitutionは代入と呼びました。実際、代入という訳語もよく使われています。僕の感覚だと、代入はメモリ領域への破壊的書き込みの感じがするのですが、それをあまり気にせずに今回は「代入」を使うことにします。

代入とは、変数の置き換え操作のことなんですが、代入の書き表し方から紹介します。この書き方(記法)がまたすごくイッパイあるんですよね。

x, yを変数としてE, Fは式だとします。式としては、例えば 2*x + y + 1 とかの算術式を思い浮かべるのが分かりやすいでしょう。E, Fには変数x, yが入ってもいいし、2 + 3 のような変数を含まない式でもいいし、x, y 以外の変数、例えばtを含んでもかまいません。

僕が一番多く見る記法は、{E/x, F/y} のようにスラッシュを使った書き方です。これはもちろん「変数xを式Eで置き換え、変数yを式Fで置き換える」という意味です。代入は一種の作用素(オペレーター)と考えて、「式 2*x + y + 1 に、代入 { (2 + 3)/x, (t + 1)/y} を作用させると 2*(2 + 3) + (t + 1) + 1 になる」のような言い方をします。

ただ、(2 + 3)/x と書くとスラッシュが割り算のように見えてしまいます。{ '2 + 3'/x, 't + 1'/y} とクォートすればいいでしょうか。でも、代入を文字列置換だと誤解されるのも困ります。
「式 '2*x + y + 1' に、代入 { '2 + 3'/x, 't + 1'/y} を作用させると '2*2 + 3 + t + 1 + 1'」
ではありません。式のテキスト表現じゃなくて、構文解析した後のAST(abstract syntax tree)のようなデータ構造を考えて、その構造に対する置換操作なんですよね。

僕が単一化についてお勉強した(したのか?)本はJ.W.ロイド(著)の『論理プログラミングの基礎』(佐藤雅彦, 森下真一 (翻訳))という本なのですが:

この本では、{x/E, y/F} という記法が使われていました。変数がスラッシュのに置かれるんですね。一方、タイガーブックだと、{x|→E, y|→F} のような矢印が使われています。

最新コンパイラ構成技法

最新コンパイラ構成技法

他に、{x := E, y := F} とか {x = E, y = F}、{x <= E, y <= F} という記法もあります。{x : E, y : F} も見たことあるような、JSONオブジェクトみたいです。ブレイス(波括弧)の代わりにブラケット(角括弧)で囲むこともあります。いずれにしても、“変数と式のペア”の集合となっています。変数も式も単なる名前やテキストではなくて、構文的なデータ構造と考えます。

で、どれを採用するべきか? 色々な書き方があることを承知の上ならどれでもいいでしょう。「置換の圏から代入の圏へ」では {x := E, y := F} を使っています。たぶん、説明では今後もこの記法を使うでしょう*1

*1:僕自身が一番よく使っているのは {E/x, F/y} という記法です。

2012-02-15 (水)

はなうた?

| 08:51 | はなうた?を含むブックマーク

次男:「今、学校の音楽で鼻歌やってる」
父親:「鼻歌? 鼻歌って言わないだろう」
次男:「なんとか」
父親:「スキャットかな?」
次男:「そんなんじゃなかった」
長男:「ハミングじゃない」
次男:「あー、それそれ、ハミング」
長男:「ハミングネオ、ふわふわー♪ って、先生に言ってみな」
次男:「うん、『かさかさー』って言おうかな、って思ったんだけど」
長男:「そしたら先生が『ふわふわー♪』と」
次男:「そうならなかったらどうすんの?」
長男:「あー、なるほど、先生がボケに反応できないときね」
次男:「それがあるでしょう」
長男:「あるね」
次男:「それとさ、先生が勝手にすべっちゃうときね」
長男:「それ困るよね」
父親:「おまいらさ、先生に何を期待してんの」

トラックバック - http://d.hatena.ne.jp/m-hiyama/20120215

2012-02-14 (火)

寒いとホントにダメェー

| 12:08 | 寒いとホントにダメェーを含むブックマーク

気温が低いだけで不調ですわ。僕はなんかもう、夏虫か爬虫類なんじゃないか、と。でも冬眠できるわけでもないし。

やたらに厚着をして外出もしないで耐え忍んでおります。喉を冷やさないようにネックウォーマーは必須。ある人から、あったかくていいと登山のときに着る下着をいただいのたすが、これは実際あったかいです。が、暖房がある所に行くと暑くて汗をかいて、それで体が冷えることもあります。下着だから脱げないし。

バイクツーリング用のグッズで、12Vバッテリーに繋ぐ伝熱ヒートジャケットてのがありますね。→ http://item.rakuten.co.jp/daikanyama-st/10002238/ 。4段階温度調整可能とな。でも、バイクじゃないとバッテリーをどうすんだ?

登山にもツーリングにも無縁な、むしろ逆な生活しているんだけどねー。ハー(ため息)。

出来の悪い演繹系に関する理論

| 18:23 | 出来の悪い演繹系に関する理論を含むブックマーク

Caty型安全性の判定系を付けようとしています。

Catyは既に動いているので、あまり大幅な変更はしたくありません。そもそも、我々のように人的リソースが極小のプロジェクトでは、一度に大きな労力をかけることは不可能なので、ボチボチ・チビチビとやっていくしかないし、それでもそれなりの効果が上がる方法しか採用できません。どうしたらボチボチ・チビチビと機能改善ができるでしょうか。

型安全性の判定系とは、プログラムの型に関する演繹系(deduction system)です。まず、この演繹系があってもなくてもシステム全体に致命的な影響を与えないことが重要です。「ないならないでも動く」ってことです。また、演繹系の出来が悪かったり機能が非力だったりしても、「それなりに使える」ことも条件になります。動かしながら、ボチボチ・チビチビ作るんだから、こういう要求になります。

上記の要求を満たすように演繹系を作っていく際に、演繹系一般に関する洞察がとても役に立ちます。ボチボチ・チビチビ作る方法を示唆してくれます。我々に必要なのは「出来の悪い演繹系に関する理論」なのですが、たいていの演繹系は完璧ではあり得ないので、通常の「演繹系の理論」が出来の悪い演繹系にも適用できます。

内容:

  1. 決定性を持たない演繹系
  2. 4値論理/3値論理を使う
  3. 良い性質と悪い性質
  4. Catyの型安全性命題
  5. ダメなプログラムを表す命題
  6. 良い、悪い、その他
  7. 判定能力をだんだんに上げる

決定性を持たない演繹系

Sがなんらかの演繹系だとして、P、Qなどは演繹系Sが扱う命題(論理式)だとします。命題Pを演繹系Sで形式的に証明できることを次のように書きます。

  • |-S P

これは、Sを外から眺めたメタな主張です。命題Pの否定(があるとしてそれ)を ¬P と書きます。演繹系Sが次の性質を持つとき、決定性を持つと呼ぶことにします。

  • どんな命題Pに対しても、|-S P または |-S ¬P 。

この決定性を「完全性」ということもありますが、モデル理論の完全性と紛らわしいので「決定性」にしました。

ゲーデルの定理によれば(「プログラマのための「ゲーデルの不完全性定理」(1)」とか参照)、ある程度の能力を持つ演繹系は決定性を持たなくなります。これは原理的な話ですが、単に演繹系(の実装)の出来が悪くて決定性を持たないことはいくらでもあります。例えば、原理的には決定可能(十分に単純)な体系なのに、そのソフトウェア実装が手抜きであった、てなことです。

演繹系Sを、命題(のデータ)を引数に渡されて計算結果として真偽値を返す関数と考えましょう。すると、Sが決定性を持つことは:

  • どんな命題(のデータ)Pに対しても、S(P) = true または S(¬P) = true 。

S(¬P) が必ず S(P) の値の否定となることを仮定すれば、次のように言い換えられます。

  • どんな命題(のデータ)Pに対しても、S(P) = true または S(P) = false 。

Sが決定性を持たないときは、次のようになります。

  • S(P) = true でもなく S(P) = false でもない命題(のデータ)Pが存在する。

上のようなPは決定不能な命題となります。演繹系が「決定性を持たない」とは、当該演繹系のなかに決定不能な命題が存在することです。原理的に決定不能な状況だけでなく、Sの出来が悪いせいでもかまいません。むしろ、ここで問題にしたいのはSの出来の悪さ=能力不足です。

4値論理/3値論理を使う

「S(P) = true でもなく S(P) = false でもない」とはどういうことでしょうか。ソフトウェア的に考えると、Sの計算が無限走行をして結果を出さないことです。停止しないので、trueもfalseもありません。無限走行を、⊥(ボトム)という記号で象徴的に表します。⊥を使うと、S(P) の結果は「trueまたはfalseまたは⊥」の3値となります。

実用上は無限走行されると困ります。途中であきらめたことを表す値indefを導入します。S(P) = indef とは、「計算はちゃんと停止したが、trueかfalseかの決定はできなかった」ということです。{true, false, indef, ⊥} の4値真偽値の計算は次の記事で述べています。

演繹系を実現するソフトウェアは、⊥(無限走行)じゃなくてindefを返すように頑張ります、いや頑張らないようにします。頑張らないで早めにあきらめてindefを返せば、無限走行を避けられます。

手違いで無限走行や例外発生があるかもしれませんが、原則的には {true, false, indef} の3値で真偽値計算できるとしましょう。つまり、演繹系を実現するソフトウェアがまともに動いてくれれば、{true, false, indef} のどれかの値が返るとします。

良い性質と悪い性質

我々が実際に行いたいことは、プログラムコードを見て実行時の型安全性(type safeness)を判断することです。ソフトウェアの性質をソフトウェアに判断させたいわけです。演繹系に証明させる命題は、p(小文字ピー)を対象とするプログラムコードとして IsSafe(p) のような形です。

3値の結果を出す判定系を使う場合は、indefの可能性があるので、より精密な結果を得るために複数の命題を組み合わせるのが有効です。その一番単純(だが、割と強力)なケースは、良い性質と悪い性質の2つの命題を組み合わせることです。IsGood(p) と IsBad(p) の2つの命題を使うわけです。具体的にどんな命題を IsGood、IsBad として選ぶかは状況次第です。

一般論をしていても分かりにくいと思うので、Catyの型安全性の判定系で説明をします。

Catyの型安全性命題

Catyは、基本となるコマンドを組み合わせてスクリプトを作り、そのスクリプトを実行させるシステムです。

コマンドとは、1入力1出力の関数のことです。基本となるコマンドは型宣言を持ちます。f:: A->B という形の型宣言は、「コマンドfの入力の型がAで、出力の型がB」という意味です。型はデータの集合を意味するので「型=集合」と考えてかまいません。以下では、型と集合を区別しません。

fとgがコマンドのとき、その結合(composition)はパイプ記号を使って f | g と書きます。3つのコマンド f, g, h のこの順での結合なら f | g | h です。ラムダ式で書くなら、(f | g | h) ≡ λx.(h(g(f(x)))) です。ここで記号「≡」は、左右は違う記法だが同じ意味だ、ということです。実引数を渡す“適用”もパイプ記号です。

  • (a | f | g | h) ≡ (λx.(h(g(f(x)))))(a)

ラムダ式よりずっとスッキリ書けるでしょ :-)

f:: A->B 、g:: C->D だとして、パイプ結合 f | g が型安全とは B⊆C のことです。パイプ記号ごとに集合の不等式(包含関係式)を書いて、すべてのパイプ記号にわたって論理ANDをとれば、それが型安全性を主張する命題になります。つまり、型安全性の命題は、集合に関する連立不等式系の形になります。

h:: E->F だとして、f | g | h の型安全性は、最初のパイプ記号から B⊆C、2番目のパイプ記号から D⊆E です。寄せ集めて (B⊆C ∧ D⊆E)、あるいは連立不等式系の形にして {B⊆C, D⊆E} となります。型変数を含まない場合だけを考えれば、これらは原理的には真偽を決定できる命題です。

ダメなプログラムを表す命題

プログラムpが p ≡ (f | g | h) であり、コマンド f, g, h の型宣言が先の通りだとすると、「pが良いプログラム」であることは次のように表せます。

  • IsGood(p) ≡ (B⊆C ∧ D⊆E)

内容的には、2つのパイプ記号の位置で型安全だという主張です(IsSafeと同じ)。

さて、では「pが悪いプログラム」であることはどう表せるでしょうか? ここで考えている型安全性は、パイプ記号の位置での集合の包含関係に基づくので、悪いプログラムとは、パイプ記号の位置でデータがサッパリ繋がらないプログラムです。

  • 最初のパイプ記号の位置でデータがサッパリ繋がらない ≡ (B∩C = 0)
  • 二番目のパイプ記号の位置でデータがサッパリ繋がらない ≡ (D∩E = 0)

ここで、0は空集合を意味します。

どちらか一方のパイプが繋がらないと、全体としてデータフロー(制御フローでもある)は脱線するので、「pが悪い」という条件は次のように書けます。

  • IsBad(p) ≡ (B∩C = 0 ∨ D∩E = 0)

良い、悪い、その他

先に進む前に注意を; IsGoo(p)∧IsBad(p)、つまり良いプログラムであると同時に悪いプログラムであるpは存在するのでしょうか? これはあります。f:: A→0、g:: C->D のとき、p ≡ (f | g) に対しては IsGood(p) と IsBad(p) が同時に成立します。このケースでは、fが無限走行したり例外を投げたりするので、入出力の情報だけでは判断ができません。矛盾しているというよりは、判断に別な情報が必要なのです。

念のために、IsReallyGood, IsReallyBad を定義しておきましょう。

  • IsReallyGood(p) ≡ (IsGood(p) ∧ ¬IsBad(p))
  • IsReallyBad(p) ≡ (IsBad(p) ∧ ¬IsGood(p))

IsReallyGoodとIsReallyBadのもとになるIsGood、IsBadは、真偽(trueまたはfalse)以外にindef(ワカラン、アキラメタ)も返す可能性があるとします。三値の真偽値の組み合わせを考えると、IsReallyGoodとIsReallyBadの可能性は次のようになります。

B↓G→ true false indef
true - 悪い -
false 良い ワカラン ワカラン
indef - ワカラン サッパリワカラン

良いプログラムは型安全性(集合の包含関係)の観点からは安心して実行できます(その他の問題は含むかも知れませんが)。悪いプログラムは実行しても常に失敗するので、絶対に実行しちゃいけません。その他はハッキリしません。

判定能力をだんだんに上げる

プログラム(を表すデータ)pを与えられて、IsReallyGood(p)とIsReallyBad(p)を計算する判定系を考えましょう。この判定系が、常にどんなプログラムpに対しても IsReallyGood(p) = indef、IsReallyBad(p) = indef と出力したらまったくの役立たずです。でも、そんな役立たずな判定系から出発して、少しでも機能を追加すると、少しだけ「良いプログラム/悪いプログラム」を識別できるようになります。だんだん判定能力を上げていくと、今まで「ワカラン」と判定されていたものが「良い/悪い」と判定されるようになるでしょう。

いくら頑張っても「ワカラン」が残っても、まーそれはそれでいいのです。型安全だと判定されても、実行時型チェックが省けるとも限りません(型宣言の間違いの可能性がある)。まったくワカランから少しワカルようになるだけでも価値があると思います。そして、継続的な改善/パワーアップができる枠組みが重要だとも思うわけです。

出来の悪い演繹系に関するモデル論の話もあるのですが、それはまた別の機会に。

MattMatt 2012/02/28 08:14 ああ,なんかこれは,すごく物理っぽいですねぇ!

どこがといわれると困るのですが…現実のプログラムの挙動に合わせて精度の良い記述を求めていくあたりでしょうかね….

m-hiyamam-hiyama 2012/02/28 11:16 Mattさん、
> ああ,なんかこれは,すごく物理っぽいですねぇ!
そうですか。まー、物理もソフトウェアも、現象を相手にして、少しずつ正しい方向に進んでいくのは同じかも。

2012-02-09 (木)

Catyと型推論

| 16:18 | Catyと型推論を含むブックマーク

Catyは、トラブルの原因になりそうなことは、事前になるべく取り除こうという方針で作っています。

データのバリデーションは当然の事として、ハイパーリンクがちゃんと繋がることを保証しよう(ハイパーバリデーション)とか、リクエスト処理の途中で失敗しても被害を抑えるためにトランザクションをしっかりやろうとか、テストが負担にならない環境を作ろうとか、文書と実装の乖離をなくすために、自動描画や自動文書化のメカニズムを入れようとか、そんなことです。

当然に、リクエスト処理が“正しく”行われることも、できるだけ実行前に保証したいわけです。とは言っても「正しさ」とは何であるかの定義は難しいし、仮に定義が出来てもそれを完璧に保証するのは困難です。せめて型安全性くらいは保証したい、というのが我々の希望です。

最近、僕が論理と型推論の記事を書き始めたり、Kuwataさんも型システムに関するノートを書いたりしているのは、Catyに型安全性の判定系を付けるための準備みたいなものです。

型安全性の判定系は、その作業の一環としていわゆる「型推論」も行います。スクリプトコードを解析して、型の観点(型に注目するだけ)からそのコードを実行していいかどうかを調べます。「どうすれば型安全性の判定ができるか」は随分と前から(だいたいは)分かっていました。そもそも、型推論機能は、Catyプロジェクトの一番最初から予定されていた機能です。

予定はしてても手が回らないという事情は常にあるのですが、それよりネックになっていたのは、一箇所どうしても分からない事があったことです。「型安全かどうか?」にYES/NOで答えられても、実行時にチェックすべき型が決まらないのです。解がないから決まらないのではなくて、妥当な解がイッパイあり過ぎてどれを選んでいいか分からない、という状況でした。

型安全性が静的に分かるなら実行時型チェックは不要ではないか? と思うでしょ。原理的には不要なんです。が、型に関する演繹をするとき、公理に相当する型宣言、例えば、foo :: string -> integer; はプログラマやアプリケーション設計者の自己申告なんです。開発中は(あるいは運用中でも)、自己申告と演繹に基づいたい名目上の安全性と実際の挙動に食い違いがあるかもしれません。そこで、静的に型安全と判定されても実行時型チェクを併用します。実行時チェック以外でも、型変数の具体化がないと困る箇所があります。

そのような型の具体化が決まらない問題があったのですが、比較的最近、どうやらうまくいきそうな気がしてきました。コロンブスの卵というか、僕に思い込みがあったようです。実は、苦し紛れにやってみた強引な方法がマトモな結果を出すので「えーーっ、こんなんで良かったん?」という状態なんですけどね。

ともかく、アルゴリズムはだいたい出来ていたし、引っかかっていた点は解決したみたい(たぶん)なので、自己流じゃない標準的な用語と記法で書き下そうと思い始めたのが1月末で、調べてみたら「標準的な用語と記法」と呼べるものはないし、山のような同義語/類義語でウンザリした、と ←今ココ。

それはそうと、以前、Catyの処理をCatyScriptで書いたことがあります(「REPL方式のWeb処理」とそこからのリンク先)。型推論の一部である単一化(ユニフィケーション)は、今のCatyScriptで書けそうです。実用にはなりませんが、説明には好都合です。CatyScriptのちょっと不便(非力)な部分をKuwataさんが修正してくれたので、単一化を書いてみようと思っています。

[追記 date="翌日"] いろいろと制限付きかつ手抜きですが、単一化を書いてみました。

面倒な事は省いてやってないからだとも言えますが、割と簡単に書けましたね。[/追記]

2012-02-07 (火)

型推論に関わる論理の概念と用語 その5:型付けの簡単な例から型判断へ

| 17:01 | 型推論に関わる論理の概念と用語 その5:型付けの簡単な例から型判断へを含むブックマーク

このシリーズの「その2」で不平不満を言い、「その3」で実例を挙げたことですが、型推論に関わる用語法は混乱を招くものです。論理をある程度知っているが型推論の用語を知らない人と、型推論に詳しいが普通の論理に馴染みがない人が話をしたら、ほとんど話が通じないでしょう。外国語にようにまったく通じないならまだいいのですが、お互いに自分の知識で解釈しようとしたら、とんでもないカオスになるでしょう。

プログラミング言語の常識からの類推も通用しません。「型宣言」なら知っていても、型注釈や型コンテキストと言われたら何のことかわかりません。多相型という言葉にしても、オブジェクト指向の人々が持っている多相のイメージとは(無関係とは言わないにしても)かけ離れているでしょう。

そんな事情でして、「型推論」の「推論」がそもそも論理で言う「推論」とは違ったりしています。論理で推論というと、演繹系の推論規則、またはその推論規則を適用して証明のステップを進める行為です。型演繹系内で行われる(論理の意味の)推論や証明は、型推論でなくて型付け(typing)と呼んでいるようです。今日は、型付けの簡単な例を調べてみます。

内容:

  1. ラムダ式を型付けする規則
  2. 型付け規則を使ってみる
  3. 型理論/型推論の言葉では

シリーズ目次:

  1. その1
  2. その2
  3. その3
  4. その4
  5. その5
  6. その6
  7. 番外(型理論ってば)

ラムダ式を型付けする規則

カリー/ハワード対応の一番簡単な例は、「タプルを持つ型付きラムダ計算」と「含意と連言を持つ命題論理」の対応です。この対応を復習しながら、ラムダ式(ラムダ項)の型付けを説明します。

まず、A、Bなどは命題として、以下の(論理の意味の)推論規則(推論図)を考えましょう。

  A   A⊃B
 ----------
    B


  A    B
 --------
   A∧B

A、Bなどは集合だと解釈してみます。集合は、Sets-as-Typesの立場なら型だと言えます。論理の含意記号「⊃」を関数集合を作る演算子「->」に置き換え、論理の連言(AND)記号「∧」を直積集合を作る演算子「×」に置き換えてみます。

  A   A->B
 ----------
    B


  A    B
 --------
   A×B

A、Bなどの集合(=型)の左側に、値(集合の要素)を表す項を添えてみます。

  s:A   t:(A->B)
 ---------------
    t(s):B


  s:A    t:B
 -------------
  [s, t]:A×B

ここで、t(s) は関数適用、[s, t]はタプルの構成です。

項と型に関する推論規則(推論図)を型付け規則(typing rule)と呼びます。型付け規則は、論理の意味の推論規則ですが、型推論規則とは(混乱が生じるので)呼ばないようです。

型付け規則を使ってみる

項の構文は「その4」で述べたJavaScript風構文とします。JavaScript風なので、タプルは [x, y] の形で書いて、配列(array)と呼びます。

lengthは配列の長さを求める関数、sumは数値(number)の足し算だとして、sum(length(x), 1) の型を求めてみましょう。足し算を「+」じゃなくて「sum」と書いたのは、関数形式のほうが扱いやすいのと、記号「+」はオーバーロードされていることが多くて厄介だからです。

もういきなり(論理の意味の)推論図を積み重ねた証明図を出してしまいますね。

x: array   length: array->number
--------------------------------
      length(x): number          1: number
     -------------------------------------
           [length(x), 1]: number×number   sum: number×number -> number
          ----------------------------------------------------------------
                          sum(length(x), 1): number

この証明図の一番下は結論である型命題 sum(length(x), 1): number です。上端になっている命題はいくつかあります。

  1. x: array
  2. length: array->number
  3. 1: number
  4. sum: number×number -> number

上記の証明図は自然演繹風です。自然演繹風の証明を外から眺めて、「こんな証明ができたよ」というメタな言明を書いてみると:

  • x: array, length: array->number, 1: number, sum: number×number -> number |- sum(length(x), 1): number

ここで、ターンスタイル記号「|-」はメタな言明を構成する記号で、左側の命題群を仮定すると右側の命題を証明できる、という意味です。

自然演繹風の証明に関するメタな言明を再び形式化したものがシーケントだと解釈できます(そう思ってもいい、という程度)。そのことは、「シーケント計算と例外処理コード」でも書きました。

上のメタな言明を、シーケントらしく矢印を「⇒」として書き換えれば以下のようです。

  • x: array, length: array->number, 1: number, sum: number×number -> number ⇒ sum(length(x), 1): number

型付け規則をシーケント計算の形に書き換えれば、型命題に関するシーケント計算の体系ができます。

型理論/型推論の言葉では

型理論/型推論では、なぜか「シーケント」という言葉は使いません。型判断(typing judgement)、型ステートメント(typing statement)、型表明(typing assertion)*1などと呼ばれます。シーケントの矢印も「⇒」や「→」ではなくて、ターンスタイルをそのまま使うのが習慣のようです。しかしメタ記号なのではなくて、シーケント計算風の演繹系のなかの記号です。

これから先、型理論/型推論におけるシーケントを型判断と呼ぶことにします。型判断は次の形をしています。

  • 型命題1, 型命題2, ..., 型命題n |- 型命題

形の上では直観主義論理のシーケントと同じです。

型判断の左右辺に出現する型命題は、「名前 : 型」という形の基本型命題です。これはまた、名前に対する型割り当て(type assignment)ともみなせます。名前に対する型割り当てを型環境型コンテキストとか呼ぶので、型判断(シーケント)の左辺を型環境、型コンテキストとも呼ぶわけです。

一方、型判断の左辺は演繹の仮定としての意味もあるので、型仮定(type assumuption)とか型仮説(type hypothesis)といった呼称も使われるのでしょう。

というわけで、同義語・類義語が生じるにはそれなりの事情と経緯があるとは言えるのですが、… …、やっぱりイヤになる。

*1:シーケントの成分である型命題を型表明と呼んでいる例もあります。

MagicantMagicant 2012/02/08 08:25 型付け規則は導出規則、証明木は導出木とも言いますね。

m-hiyamam-hiyama 2012/02/08 11:20 Magicantさん、
> 型付け規則は導出規則、証明木は導出木とも言いますね。
そうですね。「証明」とは言わないで「導出」と呼ぶ習慣みたい。
「推論」に別な意味を持たせちゃっているので「推論規則」とは呼べないのでしょうが、
「証明」を避けている理由はよく分かりません。

2012-02-03 (金)

おつかれさま

| 18:44 | おつかれさまを含むブックマーク

電話をかけると「はい、おつかれさまです」。朝、某オフィスを訪問するといきなり「檜山さん、どうもおつかれさまです」。朝からそんなに疲れてないよ、と思ってしまいます。

僕の感覚では、ひと仕事終えて実際に疲れているのをねぎらう、って言うか、まーそこまで文字通りじゃなくても、開口一番、会っていきなりの「おつかれさま」は違和感あるのですが、皆さんいかがでしょう。

そういえば最近、女子高生達が別れ際に「おつかれさん」と挨拶してるのを目撃しました。夕方の別れ際だから状況としては自然だけど、女子高生ってところがナンカね、「さよなら」とか「じゃーねー」ではなくて「おつかれさん」ですか。学校でひと仕事終えてきたって感覚なのかな。あるいは、「おつかれさま」は極めて汎用的な挨拶の地位を獲得しているのか。

hiroki_fhiroki_f 2012/02/05 23:09 >女子高生達が別れ際に「おつかれさん」と挨拶

女学生は、「ごきげんよう」と挨拶するものだと思っていました。時代は変わったのですね。

http://ja.wikipedia.org/wiki/%E5%A5%B3%E6%80%A7%E8%AA%9E

ごきげんよう 【挨拶】 かつての女学校などで使われていた挨拶。出会った時、別れる時共用である。

m-hiyamam-hiyama 2012/02/06 08:58 hiroki_fさん、
> 女学生は、「ごきげんよう」と挨拶するものだと思っていました。時代は変わったのですね。
えーっ?
僕のほうがはるかに長く生きていて、同県出身のはずだけど、
僕は「ごきげんよう」聞いたことないなー。
宇女高生あたりは言っていた?

YJSZKYJSZK 2012/02/06 12:10 こんにちは。YJSZKと申します。

> > 女学生は、「ごきげんよう」と挨拶するもの…
> えーっ?

神保町とか三番町あたりの女子中学生・高校生ですと、現在でも「ごきげんよー」という挨拶をしてますね。

m-hiyamam-hiyama 2012/02/06 18:54 YJSZKさん、
> 神保町とか三番町あたりの女子中学生・高校生ですと、現在でも「ごきげんよー」という挨拶をしてますね。
そうなんですか。僕が育った田舎やご近所では「ごきげんよう」聞いたことないです。
「おつかれさん」よりいいと思います。

shiroshiro 2012/02/06 19:32 学生時代に劇団関係で出入りしていた女子大も(その大学の在学生間では)「ごきげんよう」がオフィシャルな挨拶だったような。
とはいえ芝居関係者は別れの挨拶はいつも「おつかれさま」、出会いの挨拶は何時でも「おはようございます」ですけど。
檜山さんの目撃した女子高生は演劇部員だった、とか?

m-hiyamam-hiyama 2012/02/07 10:58 shiroさん、
> 檜山さんの目撃した女子高生は演劇部員だった、とか?
演劇部かどうかはわかりませんが、夕刻だったので部活からの帰りだったかもしれません。
部活なら「おつかれさん」で解散も普通かな。

hiroki_fhiroki_f 2012/02/07 15:20 >僕は「ごきげんよう」聞いたことないなー。
>宇女高生あたりは言っていた?

言ってないかも…。でも、そうであってほしいです。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20120203

2012-02-02 (木)

型推論に関わる論理の概念と用語 その4:JavaScript風の擬似言語

| 18:17 | 型推論に関わる論理の概念と用語 その4:JavaScript風の擬似言語を含むブックマーク

与えられた項(term)に型付け(typing)することは、型に関わる基本的行為ですが、なにかしら項の書き方(構文)を決めておかないと例を出せません。普通はラムダ項が使われるのですが、もっと馴染みがある構文を定義しておきましょう。以下で、項(term)と式(expression)は同じ意味で使います(使い分けの基準はありません)。

内容:

  1. ラムダ項をJavaScript風に書く
  2. let式
  3. 型let式

シリーズ目次:

  1. その1
  2. その2
  3. その3
  4. その4
  5. その5
  6. その6
  7. 番外(型理論ってば)

ラムダ項をJavaScript風に書く

ラムダ計算の説明にJavaScriptは好都合です(「JavaScriptで学ぶ・プログラマのためのラムダ計算」を参照)。λ(x, y).(x + y) を function (x, y){return (x + y);} と書けます。だけど、return がいかにも邪魔ですね(「returnも嫌いな理由」も参照)。returnは書かなくてもいいことにしましょう。つまり、function (x, y){x + y} でいい、と。これならもう、ほとんどラムダ項そのもの。

関数の引数と戻り値の型を次の形で宣言できるとします。

  • function (x:integer, y:integer):integer {x + y}

これは型付きラムダ項に対応します。ただし、型宣言は必須ではなくて、あってもなくてもいいとします。

引数変数だけでなく、どこに出現した変数にも型を添えていいとします。例えば、

  • function (x, y):integer {x:integer + y:integer}

出現位置のその場で型宣言をするようなものです。このような形での、変数への型情報付与を型注釈(type annotation)と言います。最初に出した、引数と戻り値の型宣言も型注釈とみなして差し支えありません。

let式

変数を束縛しておいてから式を評価することを表すためにlet式がよく使われます。次の形を使います。

  • let <変数束縛> in <式>

JavaScript風構文でもlet式を使っていいとします。

  • let {var x=2; var y=3} in {x + y}

この例では、x + y は 2 + 3 となり、全体の値は5です。すべての変数が束縛される必要はありません。

  • let {var x=2} in {x + y}

これだと、x + y が 2 + y になりますが、それ以上は評価できません。

  • let {var y=3} in {function (x) {x + y}}

これは、function (x) {x + 3} が値となります。

  • let {var x=2} in {(let {var y=3} in {function (x) {x + y}})(x)}

少し複雑ですが、注意深く順番に見ていけば、次と同じことがわかると思います。

  • (function (x) {x + 3})(2)

次はどうでしょうか? 考えてみてください。

  • let {var x=2} in {let {var y=3} in {let {var f = function (x) {x + y}} in {f(x)}}}

型let式

let式は、変数に値を束縛します。値には関数も含まれます(let {var f = function (x) {x + y}} がその例)。式の評価のための環境を整えていることになります。一方、式の型を知りたいときは、型付け(typing)の環境が必要です。それは、変数や関数の戻り値に型注釈を付けることになります。

型注釈を付けるための専用の構文、例えば lettype {var x:integer; var t:boolean} を導入してもいいのですが、めんどうだからletをそのまま使ってしまいましょう。

  • let {var x:integer; var t:boolean} in {function (y:integer) {if (t) {x} else {y}}}

function (y:integer) {if (t) {x} else {y}} だけだと、yの型しかわかりませんが、外側のletにおいて、x:integer; var t:boolean と型注釈(型宣言)されているので、x, y, tの型がハッキリとわかります。

let内では、変数の型注釈と値の束縛を一緒にやってもいいとします。

  • let {var x:integer=2; var t:boolean} in {function (y:integer) {if (t) {x} else {y}}}

if (t) {x} else {y} のような式だけだと、変数の型も値も不明です。let式によって、型情報や値情報を準備してあげることができます。すべての情報を明示的に与えなくても、与えられた情報をもとに計算や推論ができます。できるだけ少ない型注釈から、式やその部分式の型を決定することが、「型推論」のひとつの解釈です。

2012-02-01 (水)

喫茶店とは何か

| 18:14 | 喫茶店とは何かを含むブックマーク

長男:「俺、喫茶店行ってみたいな」
父親:「一緒にスターバックス行ってるじゃん」
長男:「スターバックスは喫茶店と違うよ」
父親:「じゃ、どんなんが喫茶店なんだ?」
長男:「えーとね、大人の人がタバコ吸ってるの」
父親:「禁煙じゃないってことね」
長男:「そう、それでコーヒー以外に食べ物がある」
父親:「スターバックスだって、スコーンとかサンドイッチとか売ってるぞ」
長男:「そうじゃなくて、ピラフとかスパゲッティとか」
父親:「あー、ランチセットとかね」
長男:「そうそう、スパゲッティの具はソーセージ」

確かに、昭和の「喫茶店」ってそんなイメージだな。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20120201