2016-08-19

Windows 10 導入作業

Windows 10を導入する上でやったこと

ディスプレイの色調整

液晶の白が青かぶりしている感じだったので、ディスプレイの詳細設定から色設定を行う。

開発者向け機能

更新とセキュリティから、開発者向け機能に関する設定を行う

PackageManagement

ソフトウェア開発に使う各種ツール群をコマンドラインからインストール

Git for Windows

PackageManagement+chocolateyで入れるとデフォルトで改行コードの変換が行われる設定になるのでgit config --global core.autocrlf=falseしておく。

Visual Studio Code

{
  "editor.tabSize": 2,
  "editor.renderWhitespace": true,
  "files.eol": "\n",
  "terminal.integrated.shell.windows": "C:\\Windows\\System32\\WindowsPowerShell\\v1.0\\powershell.exe"
}

2016-07-17

Suica専用自販機に見る形骸化した記号の話

哲学

Suica専用自販機。
どんどん進めていけばいいし、
通常の自販機を流用するのも全然いい。

たださ、
なんでコイン投入口跡に小銭のイラストを残したの？
飲み物買おうとした外国人、英語の説明ないから、お金入れようと四苦八苦してたぞ。 pic.twitter.com/qIja6ba6Bx
— いし@名誉駅長35ヶ月目 (@mk_ishi) 2016年7月15日

あと、Suica専用自販機のコイン投入口の上の点字、
たぶん"コイン"って書いてある。
視覚障害者のことを考えたら、コインが投入できないここに、コインって点字を残さないでしょ。https://t.co/PKCv57C7U7 pic.twitter.com/6ceHmw1wgp
— いし@名誉駅長35ヶ月目 (@mk_ishi) 2016年7月15日

あの酷い、残額を見せる気のない自動改札機を改良もせずに展開してるJR東日本に期待する方が悪いとは思ってるけど、
訪日外国人や視覚障害者にたいしての配慮がいかないのはさすがに放置できない。
— いし@名誉駅長35ヶ月目 (@mk_ishi) 2016年7月15日

この話を見た時、これはまさに「形骸化した記号」のよい例だろうと思った。ナンセンスな「電子署名」の話よりも、それが形骸であることがずっと分かりやすい。

普段から自販機を使っている大多数の日本人にとって、それがコイン投入口だということを認知するためにコインの絵や点字は必要ではなく、無意識に見過ごされた記号であったのだろう。だから、実際に困る人が現れるまでは、誰も気づくはずがなかった。

それで、教訓として得るべきなのはなんだろうか。マイノリティーへの配慮を充実させること？まあ、それはそうだろう。多様性を持つ利用者全般に対して不都合のないデザインであるか、よくテストを行うべきだと言える。アクセシビリティのガイドラインを守り、マイノリティーを尊重し、適切なテストを行った後にプロダクトを出すのが理想だ。問いたいのは、理想を実現させるにはどうすればよいのかということだ。

あらゆるマイノリティーに対してアクセシビリティ上の困難がないかテストをするには多大なコストが掛かる。それは必要なコストだ、と頭で分かるとしても、感情が付いてこない。マジョリティーはマイノリティーに対する意識を高めなければならないのだけれども、それはアクセシビリティのガイドラインを頭に叩き込むだけでは成しようがない。必要なのは、ルールの遵守というよりも、記号を多様な観点から見ることができる柔軟さだ。

記号の不完全さへの意識を高めるのに、笑いは重要な役割を果たしうる。私たちは記号を信用し、時に記号に裏切られる。記号の解釈には文化による差異があり、それによって起こる勘違いは、記号が引き起こす悲喜劇だ。記号はコミュニケーションのなかだちだけど、それが勘違いの種であり、常に不完全さを孕むことを認めよう。未知の存在との交流は常に勘違いの連続だ。私たちは記号と、記号が引き起こす勘違いを互いに笑いながら、少しずつ乗り越えていくしかない。異文化交流とは、寛容性を前提としなければ成し得ないと思う。

2016-07-17

東京メトロの行先案内の多言語化で全言語にルビが付いていて賢いという話（だけど限界もある）

日本語

東京メトロの多言語化戦略、全部の言語にふりがなが付いていて賢い
— Ryusei Yamaguchi (@mandel59) 2016年7月15日

全部の言語にふりがながあるから、ハングル表示の時に日本人が読めないというクレームを無効化している、神対応か
— Ryusei Yamaguchi (@mandel59) 2016年7月15日

ドラえもんの絵の広告で見ただけでインプリメンテーションは確認していないが、絵だけで神デザインとわかる
— Ryusei Yamaguchi (@mandel59) 2016年7月15日

ちなみにこれね。全言語にふりがな。 pic.twitter.com/C6kmxVG6eQ
— Ryusei Yamaguchi (@mandel59) 2016年7月15日

ルビ（振り仮名）が振ってあると、すごく日本っぽい感じがする。ハングル一色の画面を見れば、異形の文字を見慣れない人には忌避感を与え、ここは日本だぞと文句を付けたくもなるっていう人が出てくるんだろうけれども、ハングルに振り仮名するだけで、そういう人にとっても、なんだ日本語じゃないかと思えてくるのではないか。たぶん。まあ、それでも文句を付ける人は付けるんだろうけれども。

ルビは、昔から漢字と仮名を併用してきたからこそ生まれた、日本独特の組版文化だと言える。もちろん、発音を併記するのは中国語学習用のテキストとかでもやることではあるのだけれども、日本語のようにルビを常用する文化は他にないだろう。漢字と仮名という複数のチャンネルを使って情報を流すことで、字義と音価、あるいは意味と意味が新しい形で結びつく。そのことが、言葉を新しい視点から眺めることを教えてくれる。

ルビの欠点として、ルビは小さい。視力に自信がない人は、やっぱり平仮名の大表示も欲しいって思うだろう。そして、ルビを振ると画面が煩雑になる。大きな表示スペースがないと難しい。万人にとって良い画面を設計するのはほぼ不可能なことで、どうしたって切り捨てが生じてしまう。液晶ディスプレイによる時分割表示は、多言語対応の万能薬ではない。

そもそも、公共のディスプレイに表示しようとするから、万人が読める表記という難題を解かなければならないのであって、一番いいのは、個々人に最適化された案内表示がなされることだろう。スマートフォンに表示する分には、他人の目を気にすることなく、自分の都合のよい表示方法に設定できるはずだ。案内情報を局所的に配信する仕組みは絶対に必要だと思うのだけれども、誰か真剣に取り組んでくれないだろうか。

2016-06-04

花押の件について判決文を読んでみたけどよく分からなかった話

哲学

www.jiji.com

今回の裁判の要旨は「いわゆる花押を書くことは，民法９６８条１項の押印の要件を満たさない」ということですが、その理由を抜き出してみます。

　３　原審は，次のとおり判断して，本件遺言書による遺言を有効とし，同遺言により被上告人は本件土地の遺贈を受けたとして，被上告人の請求を認容すべきものとした。
　花押は，文書の作成の真正を担保する役割を担い，印章としての役割も認められており，花押を用いることによって遺言者の同一性及び真意の確保が妨げられるとはいえない。そのような花押の一般的な役割に，ａ家及びＡによる花押の使用状況や本件遺言書におけるＡの花押の形状等を合わせ考えると，Ａによる花押をもって押印として足りると解したとしても，本件遺言書におけるＡの真意の確保に欠けるとはいえない。したがって，本件遺言書におけるＡの花押は，民法９６８条１項の押印の要件を満たす。
　４　しかしながら，原審の上記判断は是認することができない。その理由は，次のとおりである。
　花押を書くことは，印章による押印とは異なるから，民法９６８条１項の押印の要件を満たすものであると直ちにいうことはできない。
　そして，民法９６８条１項が，自筆証書遺言の方式として，遺言の全文，日付及び氏名の自書のほかに，押印をも要するとした趣旨は，遺言の全文等の自書とあいまって遺言者の同一性及び真意を確保するとともに，重要な文書については作成者が署名した上その名下に押印することによって文書の作成を完結させるという我が国の慣行ないし法意識に照らして文書の完成を担保することにあると解されるところ（最高裁昭和６２年（オ）第１１３７号平成元年２月１６日第一小法廷判決・民集４３巻２号４５頁参照），我が国において，印章による押印に代えて花押を書くことによって文書を完成させるという慣行ないし法意識が存するものとは認め難い。
　以上によれば，花押を書くことは，印章による押印と同視することはできず，民法９６８条１項の押印の要件を満たさないというべきである。
http://www.courts.go.jp/app/hanrei_jp/detail2?id=85930

読みづらいので、箇条書きにして原審の判断と最高裁の判断を整理してみます。

原審の判断:

(1.) 花押は，文書の作成の真正を担保する役割を担い，印章としての役割も認められており，花押を用いることによって遺言者の同一性及び真意の確保が妨げられるとはいえない
(2.) そのような花押の一般的な役割に，ａ家及びＡによる花押の使用状況や本件遺言書におけるＡの花押の形状等を合わせ考えると，Ａによる花押をもって押印として足りると解したとしても，本件遺言書におけるＡの真意の確保に欠けるとはいえない
(結論1.) したがって，本件遺言書におけるＡの花押は，民法９６８条１項の押印の要件を満たす

原審では押印の要件をどのように考えていたのかが抜けているので、これだけでは妥当な論証にはなっていません。原審の判決文を確認する必要がありそうです。

最高裁の判断:

(3.) 花押を書くことは，印章による押印とは異なる
(4.) (3.)から，〔花押を書くことは，〕民法９６８条１項の押印の要件を満たすものであると直ちにいうことはできない
(5.) 民法９６８条１項が，自筆証書遺言の方式として，遺言の全文，日付及び氏名の自書のほかに，押印をも要するとした趣旨は，(5-1.)とともに，(5-2.)にあると解される
- (5-1.) 遺言の全文等の自書とあいまって遺言者の同一性及び真意を確保する〔こと〕
- (5-2.) 重要な文書については作成者が署名した上その名下に押印することによって文書の作成を完結させるという我が国の慣行ないし法意識に照らして文書の完成を担保すること
(6.) 我が国において，印章による押印に代えて花押を書くことによって文書を完成させるという慣行ないし法意識が存するものとは認め難い
(結論2.) 花押を書くことは，……民法９６８条１項の押印の要件を満たさないというべきである

この論証は妥当な論証ですが、結論を導くのに必要なのは(5.)の〈(5-1.)と(5-2.)をともに満たす⇔押印の要件を満たす〉という趣旨の命題と(6.)の〈花押を書くことは(5-2.)を満たさない〉という趣旨の命題だけです。(3.)と(4.)は、それが否定されると結論も否定されるような命題です。

論証自体は妥当ですが、そこに挙げられている前提(5.), (6.)は妥当なのでしょうか。

(5.) の主張のために「最高裁昭和６２年（オ）第１１３７号平成元年２月１６日第一小法廷判決」が参照されていますが、この裁判の要旨は「自筆遺言証書における押印は、指印をもつて足りる」ということです。こちらも、その理由を抜き出してみます。

　自筆証書によつて遺言をするには、遺言者が遺言の全文、日附及び氏名を自書した上、押印することを要するが（民法九六八条一項）、右にいう押印としては、遺言者が印章に代えて拇指その他の指頭に墨、朱肉等をつけて押捺すること（以下「指印」という。）をもつて足りるものと解するのが相当である。けだし、同条項が自筆証書遺言の方式として自書のほか押印を要するとした趣旨は、遺言の全文等の自書とあいまつて遺言者の同一性及び真意を確保するとともに、重要な文書については作成者が署名した上その名下に押印することによつて文書の作成を完結させるという我が国の慣行ないし法意識に照らして文書の完成を担保することにあると解されるところ、右押印について指印をもつて足りると解したとしても、遺言者が遺言の全文、日附、氏名を自書する自筆証書遺言において遺言者の真意の確保に欠けるとはいえないし、いわゆる実印による押印が要件とされていない文書については、通常、文書作成者の指印があれば印章による押印があるのと同等の意義を認めている我が国の慣行ないし法意識に照らすと、文書の完成を担保する機能においても欠けるところがないばかりでなく、必要以上に遺言の方式を厳格に解するときは、かえつて遺言者の真意の実現を阻害するおそれがあるものというべきだからである。もつとも、指印については、通常、押印者の死亡後は対照すべき印影がないために、遺言者本人の指印であるか否かが争われても、これを印影の対照によつて確認することはできないが、もともと自筆証書遺言に使用すべき印章には何らの制限もないのであるから、印章による押印であつても、印影の対照のみによつては遺言者本人の押印であることを確認しえない場合があるのであり、印影の対照以外の方法によつて本人の押印であることを立証しうる場合は少なくないと考えられるから、対照すべき印影のないことは前記解釈の妨げとなるものではない。そうすると、自筆証書遺言の方式として要求される押印は拇印をもつて足りるとした原審の判断は正当として是認することができ、原判決に所論の違法はない。論旨は、採用することができない。
http://www.courts.go.jp/app/hanrei_jp/detail2?id=52210

平成元年の判決の判断:

(結論3.) ……押印としては、遺言者が印章に代えて拇指その他の指頭に墨、朱肉等をつけて押捺すること（以下「指印」という。）をもつて足りるものと解するのが相当である
(7.) 同条項が自筆証書遺言の方式として自書のほか押印を要するとした趣旨は、(7-1.)とともに、(7-2.)にあると解される
- (7-1.) 遺言の全文等の自書とあいまつて遺言者の同一性及び真意を確保する〔こと〕
- (7-2.) 重要な文書については作成者が署名した上その名下に押印することによつて文書の作成を完結させるという我が国の慣行ないし法意識に照らして文書の完成を担保すること
(8.) 右押印について指印をもつて足りると解したとしても、遺言者が遺言の全文、日附、氏名を自書する自筆証書遺言において遺言者の真意の確保に欠けるとはいえない
(9.) いわゆる実印による押印が要件とされていない文書については、通常、文書作成者の指印があれば印章による押印があるのと同等の意義を認めている我が国の慣行ないし法意識に照らすと、文書の完成を担保する機能においても欠けるところがない
(10.) (9.)ばかりでなく、必要以上に遺言の方式を厳格に解するときは、かえつて遺言者の真意の実現を阻害するおそれがあるものというべき〔である〕

(5.)は(7.)を参照していて、ほとんど同じ表現であることがわかります。(7.)の〈(7-1.)と(7-2.)をともに満たす⇔押印の要件を満たす〉という趣旨の命題は、(8.)の〈指印は(7-1.)を満たす〉、(9.)の〈指印は(7-2.)を満たす〉という趣旨の命題と合わせて、(結論3.)を妥当に導くための前提になっています。

(7.)が指印が印章の代わりになることを主張する際に考えられた前提であるのに対し、それを今回の判決の(5.)は逆に使われていて、花押が印章の代わりにならないことを主張するための前提になっていますが、主張(5.)自体は妥当で「押印の要件」つまり押印であると認められる必要十分条件になっていると思われます。そうすると、問題になるのは(6.)です。

(6.)は単に原審における前提(1.)の「印章としての役割も認められており，」を否認しているだけのように見えます。（原審の判決文は確認できていないので、原審で認められた「印章としての役割」が具体的にどのような役割を指しているのかははっきりしませんけれども。）そして、その前提にさらなる理由は与えられていません。

結局、判決文を読んで分かったのは、最高裁判所は「我が国において，印章による押印に代えて花押を書くことによって文書を完成させるという慣行ないし法意識が存するものとは認め難い」という判断を行ったが、その判断には全く理由が与えられていないということでした。なぜ、こんなよく分からない判決文が許されているんでしょうか。「印章による押印に代えて花押を書くことによって文書を完成させるという慣行ないし法意識が存する」かどうかについて、十分審議が尽くされたのでしょうか。審議するまでもなく自明だという認識なんでしょうか。そこら辺が、よく分かりませんでした。

リファレンス

平成27(受)118 遺言書真正確認等，求償金等請求事件平成28年6月3日最高裁判所第二小法廷判決 http://www.courts.go.jp/app/hanrei_jp/detail2?id=85930
昭和62(オ)1137 遺言無効確認請求事件平成元年2月16日最高裁判所第一小法廷判決 http://www.courts.go.jp/app/hanrei_jp/detail2?id=52210

2016-05-23

シンタックス・ハイライト機能はHaxeに対応してほしいです。

お題「シンタックス・ハイライト機能で対応してほしい言語」

Haxeに対応してほしいです。

class Test {
    static function main() {
        trace("Haxe is great!");
    }
}

HaxeはActionScript風のシンタックスを持ちながらも、JavaScriptやC#, PHPなど多数のターゲットに対してコードをトランスパイルすることができる言語です。

Flashとの互換性を持つOpenFLというフレームワークを抱えていたり、言語のオリジナル開発者がゲームデベロッパーで性能を重視した言語であるという面も関係して、ポストFlash時代におけるゲーム開発プラットフォームとして採用事例が多数存在しています。

また、複数ターゲットに出力可能であることから、クライアント側とサーバー側で共通のコードを利用することが可能だという点も魅力です。

2016-05-14

文脈付き構成的意味論を構成的意味論に変換する

プログラミング哲学数学

mandel59.hateblo.jp

ここでは, 自然数の集合 ${\bf N}$ に0を含めることとする。

記法 $\left ( a_k \right )_{k=m}^{n}$ は $\left (a_m, a_{m+1}, \cdots, a_{n-2}, a_{n-1} \right )$ を表す。 $m = n$ の時は $\left ( \right )$ を表す。
記法 $\bigwedge_{k = m}^{n} p_k$ は $p_m \wedge p_{m+1} \wedge \cdots \wedge p_{n-2} \wedge p_{n-1}$ を表す。 $m = n$ の時は $\top$ （真理値の真）を表す。

形式言語

形式言語 $L = \langle F, | \bullet | \rangle$ は関手集合 $F$ , 関手の項数 $| \bullet | : F \rightarrow {\bf N}$ からなる組である。

式

形式言語 $L = \langle F, | \bullet | \rangle$ の式集合 $E(L)$ を, つぎの帰納的定義によって定める:

$f \in F \land \left ( \bigwedge_{k = 0}^{|f|} t_k \in E(L) \right ) \Rightarrow f(t_k)_{k=0}^{|f|} \in E(L)$ .

これは, 次のようなことを含意している:

が項数の関手であり, が式であるとき, は式である。
- 特に, $f$ が項数 $0$ の関手であるとき, $f()$ は式である。
$t$ が式であるとき, ある自然数 $n$ , ある項数 $n$ の関手 $f$ , ある式 $t_0, \cdots, t_{n-1}$ が存在し, $t = f(t_0, \cdots, t_{n-1})$ .

構成的意味論

構成的意味論 $\Sigma = \langle L, M, I \rangle$ は形式言語 $L = \langle F, | \bullet | \rangle$ , 意味集合 $M$ , 解釈 $I : f \in F \mapsto g \in [ M^{|f|} \rightarrow M ]$ からなる組である。

このとき $\Sigma$ のもとの式の意味 $\Sigma \unicode{x27e6} \bullet \unicode{x27e7} : E(L) \rightarrow M$ を, つぎの帰納的定義によって定める。

$\Sigma \unicode{x27e6} f(t_k)_{k=0}^{|f|} \unicode{x27e7} = I(f) \left ( \langle \Sigma \unicode{x27e6} t_k \unicode{x27e7} \rangle_{k=0}^{|f|} \right )$

文脈付き構成的意味論

文脈付き構成的意味論 $\Sigma_\star = \langle L, C, V, I_\star \rangle$ は形式言語 $L = \langle F, | \bullet | \rangle$ , 文脈集合 $C$ , 値集合 $V$ , 解釈 $I_\star : f \in F \mapsto g \in [ [ C \rightarrow V ]^{|f|} \rightarrow [ C \rightarrow V ] ]$ からなる組である。

このとき $\Sigma_\star$ のもとの式の意味 $\Sigma_\star \unicode{x27e6} \bullet \unicode{x27e7} : E(L) \rightarrow [ C \rightarrow V ] \$ を, つぎの帰納的定義によって定める。

$\Sigma_\star \unicode{x27e6} f(t_k)_{k=0}^{|f|} \unicode{x27e7} = I_\star(f) \left ( \langle \Sigma_\star \unicode{x27e6} t_k \unicode{x27e7} \rangle_{k=0}^{|f|} \right )$

文脈 $c \in C$ のもとの式 $e$ の値は $\Sigma_\star \unicode{x27e6} e \unicode{x27e7} (c) \$ になる。

文脈付き構成的意味論を構成的意味論に変換する

文脈付き構成的意味論 $\Sigma_\star = \langle L, C, V, I_\star\rangle$ から自明な構成的意味論 $\Sigma ' _\star = \langle L, [ C \rightarrow V ], I_\star \rangle$ を構成できる。

2016-05-11

プログラム意味論の分かりやすい紹介

プログラミング哲学

巷に膾炙しているプログラム意味論の説明は、正直言って何を言っているのか、部外者にはよく分からないように感じられる。プログラムの意味を論じる「プログラム意味論」の意味がよくわからないというのは本末転倒だろう。ここでは、プログラム意味論を分かりやすく紹介したい。

プログラムの意味

プログラム意味論とは、プログラムの意味に関する理論だ。

そもそも「意味」とはなんだろうか。「意味」の意味を知るために、デジタル大辞泉で調べてみよう。

１言葉が示す内容。また、言葉がある物事を示すこと。「単語の―を調べる」「愛を―するギリシャ語」
２ある表現・行為によって示され、あるいはそこに含み隠されている内容。また、表現・行為がある内容を示すこと。「慰労の―で一席設ける」「―ありげな行動」「沈黙は賛成を―する」
３価値。重要性。「―のある集会」「全員が参加しなければ―がない」
いみ【意味】の意味 - goo国語辞書

「意味」の語義が3つ示されているが、要約すると、ひとつめは「言葉が示す物事」、ふたつめは「行為が示す物事」、みっつめは「行為が持つ価値」だ。この3つの「意味」の意味は無関係なものではなく、共通した構造が存在している。それは、何か言葉や行為という表に見えている表現は、その裏にある物事や価値に繋がっているという構造だ。

たとえば、店で「ビールあり〼」という看板を見たとする。ビールの実物を見ずとも、その店には実際にビールが用意されていて、店はそのビールを売る意図があって、自分はそれを注文して飲むことができるという場面を想像できる。その想像された場面や、その場面の持っている価値が、「ビールあり〼」の意味だと言える。

プログラムの意味も同様だ。プログラムの意味とは、そのプログラムによって実現される物事や場面のことだと言える*1。例えばalert(1)というJavaScriptのプログラムは、実行するとダイアログ・ボックスで“1”を表示する。すなわち、alert(1)の意味は「ダイアログ・ボックスで“1”を表示する」という場面だ。

プログラムの意味は、そのプログラムを動かしてみれば分かるように思うかもしれないが、プログラムを動かすにもコストやリスクが存在する場合がある。誤作動を起こすプログラムを実際に動かしてしまえば、重大な事故を引き起こすかもしれない。それを避けるためには、プログラムを動かすことなく、その意味を知る必要があるのだ。

優れたプログラマーが頭の中で考えたプログラムを一発で動かしてしまうのも、プログラムの意味を体得しているからだと言える。しかし、プログラムの意味を個人の経験によって身に付けるのは時間がかかるだけではなく、その厳密さにも限界がある。見慣れない種類のプログラムがどのように動くかは、経験からでは分からないのだ。そういう場合でも、プログラム意味論でプログラムの表現と物事の間にある関係を詳細に学ぶことで、プログラムの意味を正確に把握できるようになるだろう。

形式的意味論

意味論は表現と物事の対応を論じるものではあるけれど、現実の物事はすごく複雑で、それをありのままに考えて厳密に論じるのはとても難しい。そこで、普通は物事を抽象化した上で、厳密に考えることになる。*2物事を抽象化した上で、数学や論理学を使って厳密に論じられる意味論が、形式的意味論だ。形式的意味論には操作的意味論、表示的意味論、公理的意味論といった大別がある。

操作的意味論は、表現を操作する規則や抽象機械を使ってプログラムの意味を考える。この意味論では表現の操作過程や抽象機械の動作が、表現の意味となる。この意味論は、現実のコンピューターの動作に一番近い形で表現された意味論で、プログラムに対して、機械がどれほどの計算資源を使い、どのように動作するのかを厳密に議論するのに適した表現だと言える。その一方で、操作的意味論が扱った規則以外の方法でプログラムを処理することについては考慮しないので、プログラムの読みやすさや編集しやすさを議論するには適していないだろう。

表示的意味論は、表現から物事への写像（表示）を使ってプログラムの意味を考える。この意味論においては、表現からの写像が定義できる好きな領域を意味としてよい。この手法は、言語の意味を数理論理学や言語哲学と同様の手法を用いて考えており、プログラムを読み書き・編集するときの性質を分析するのに向いている。例えばプログラミング言語が「構成性」という性質を持っていることが意味論から分かるので、その性質を利用したプログラムの最適化を行う、といったことに使える。

公理的意味論は、表現と物事の間に成り立つ関係（仕様）を使ってプログラムの意味を考える。この意味論においては、仕様を公理として証明できる物事が、表現の意味となる。この意味論では、仕様にないプログラムの具体的な動き方は分からないが、プログラムの「停止性」のような抽象度のより高い性質を証明するのに向いている。

リファレンス

【PDF】 Computer Science 203 Programming Languages Axiomatic Semantics

*1:「実行結果」と言ってしまえば済むように思うが、サーバーのように継続的に実行され続けるプログラムや、ギャンブル・ゲームのように非決定的な振る舞いをするプログラムもあるわけで、そのようなプログラムの意味も考えようとすると、単に「実行結果」と言うだけでは済まない。

*2:ここで「厳密に論じる」と言っているのは、他人に自分の論理を説明できる形で、論理的に論じるということだ。論じる問題が複雑になると、関係しあう事柄の組み合わせが爆発的に増えるせいで、論理を構成するのが極端に難しくなってしまう。だから、抽象化を行うことで一度に考える事柄を減らし、問題を厳密に論じきれる大きさにする必要がある。

2016-05-05

プログラミングと哲学

哲学プログラミング

プログラミングと哲学の間には深い関係がある。プログラミングが昔ながらの哲学と単純に対応するというわけではないけれども、だからといって全くの無関係というわけでもない。その理由として、プログラミングの方法論のひとつに、世界を分析し、それを記述するという方法でプログラムを書くという考えがあることが挙げられる。

それはまさにオブジェクト指向の理念である、と考える人は、プログラミングのことも哲学のこともよく知らない。世界の様子を記述するという性質はオブジェクト指向の専売特許などではなく、平叙型プログラミング*1に共通して見られる考えだ。すなわち、関数型プログラミングや論理型プログラミングもまた、世界の様子を記述する側面を持っている。

「世界を分析して記述する方法」というのは、古来哲学が対象としてきたことのひとつだ。それなら、哲学なんてプログラミングと関係ないとするほうが、伝統に則らない考えだというべきだろう。分かりやすい例として、論理型プログラミングと分析哲学の関係を挙げる。論理型プログラミングの記法は記号論理学に由来するが、遡ればフレーゲの「概念記法」にたどり着く。フレーゲは一方で分析哲学の祖ともされるが、フレーゲの分析哲学とは、概念記法の背景にある考えを記述したものに他ならない。

あなたが論理学や論理型プログラミング言語を使っている時、あなたはその背景にある「世界の分析方法」をも、気づかないうちに体得している。そういう無意識のうちに使っている考え方を、哲学者は積極的に言語化してくれているのだ。分析哲学を知らなくても論理学を使えるかもしれないが、分析哲学を知ることで論理学自体をよりよく知ることができる。

プログラミングと哲学を結びつけて考えるというのは、古臭い考えを無批判に受け入れるということでもなければ、突飛なこじつけをするというものでもない。むしろその反対だ。自分が無意識に使っている概念があることを既存の哲学を通して自覚することで、プログラミングをより深く理解し、批判的に接することができるようにする。古い哲学が自分の考え方を完全に説明していると思われなければ、新しく考えを付け足していく。そういう営みを意識的に行うことが、プログラミングと哲学を結びつけて考える意義だろうと思う。

*1:declarative programming. 定訳は「宣言型プログラミング」だが、言語学では「命令文 imperative sentence」「平叙文 declarative sentence」と言うのだから、当然「命令型プログラミング imperative programming」に対して「平叙型プログラミング」と訳すべきだ。

2016-04-06

Referential Transparencyの代わりに使える概念案

プログラミング哲学

Referential Transparencyという概念が指すものは漠然としているので、もっと意味が明瞭で使いやすい用語を定義し、色々な言語の性質を記述してみる。

前提として

式は原子式か複合式である。
複合式は関手（functor）と項（argument）から構成される。

〈純粋性〉: 「式の意味」と「式の値」は同義である。
〈原子確定性〉: 原子式の意味は原子式自身とその原子式の文脈から決定される。
〈構成性〉: 複合式の意味は関手および項の意味から決定される。
〈弱構成性〉: 複合式の意味は関手、項の意味および式の文脈から決定される。
〈文脈構成性〉: 複合式の項の文脈は、その複合式の文脈と関手から決定される。
〈文脈弱構成性〉: 複合式の項の文脈は、その複合式の文脈、関手および他の項の意味から決定される。
〈確定性〉: 式と式の文脈から部分式の意味が決定される。
〈文脈確定性〉: 式と式の文脈から部分式の文脈が決定される。
〈文脈同一性〉: 部分式は式全体と同じ文脈を持つ。
〈同値置換可能性〉: 部分式を、その式と同値の別の部分式に置き換えても、式全体は同じ意味を持つ。

関手がすべて全関数である数式は〈原子確定性〉〈構成性〉〈文脈同一性〉を持つので、〈確定性〉がある。たとえば、 $\{ a \mapsto 2, b \mapsto 3 \}$ という文脈において、式 $a + b$ は確定した値 $5$ を持つ。また、同じ変数は、ひとつの式の中では常に同じ値を指す。
C言語においては普通「式の値」でなく、副作用を含めた「式の動作」が「式の意味」だと考えるので、C言語は〈純粋性〉を持たないと言える。
Haskellにおいては普通「式の値」が「式の意味」だと考えるので、Haskellは〈純粋性〉を持つと言える。
関手がすべて全関数である数式に非再帰的なlet式を加えても〈原子確定性〉〈弱構成性〉〈文脈弱構成性〉〈確定性〉は保たれる。

（〈弱構成性〉は、レカナティの「語用論的構成性」と同様の概念か。 http://www.wakate-forum.org/data/tankyu/42/42_09_takaya.pdf）

2016-04-01

Referential Transparencyについて取り急ぎ

プログラミング哲学

Wikipedia日本語版に

参照透過性（さんしょうとうかせい、英: Referential transparency）は、計算機言語の概念の一種で、文脈によらず式の値はその構成要素（例えば変数や関数）によってのみ定まるということを言う。
https://ja.wikipedia.org/w/index.php?title=%E5%8F%82%E7%85%A7%E9%80%8F%E9%81%8E%E6%80%A7&oldid=46720534

とあるが、これは誤り。「文脈によらず式の値はその構成要素によってのみ定まる」という性質は、参照透過性ではなく構成性 (compositionality) と言う。

In mathematics, semantics, and philosophy of language, the principle of compositionality is the principle that the meaning of a complex expression is determined by the meanings of its constituent expressions and the rules used to combine them.
https://en.wikipedia.org/w/index.php?title=Principle_of_compositionality&oldid=646872914

The meaning of a complex expression is determined by its structure and the meanings of its constituents.
http://plato.stanford.edu/entries/compositionality/

参照透過性は、英語版 Wikipediaによれば次の性質だ。

An expression is said to be referentially transparent if it can be replaced with its value without changing the behavior of a program (in other words, yielding a program that has the same effects and output on the same input).
ある式は、その式をその式の値に置き換えてもプログラムの動作が変わらないとき（いいかえれば、同じ入力に対して同じ作用と出力を持つプログラムになるとき）、参照透過であるという。
https://en.wikipedia.org/w/index.php?title=Referential_transparency&oldid=709215227

（この定義が正しいとは限らないが、日本語版の説明と食い違っていることは明らかだ。）

問題をややこしくするのは、式 (expression)、意味 (meaning) 、表現 (representation)、正規形 (regular form)、表示 (denotation)、参照 (reference)、値 (value)、動作 (behavior) といった用語が、文脈によってそれぞれ同義になったりならなかったりして、混同されるというところだ。それについては別に整理してまとめることにする。

2016-03-19

ナンセンスな「電子署名」と、「失われた魔法」の話

哲学

今日の帰り道に、携帯電話会社の店舗に寄って、支払い方法をクレジットカード払いに変更してきた。身分証明証とクレジットカードを提示し、支払い方法を変更するんだけど、最後にタブレットを差し出され、指で画面への「署名」を求められた。これは変だ。その場で理由も特に聞かないまま、とりあえず日付と名前を書いて「署名」したんだけど、もったいないことをした。もし登大遊だったら、きっとツッコミを入れている。

以前、「ハンコは、ハンコが本人と書類を紐付けることと、複製（偽造）が不可能であることによって意味を持つ」というハンコの意味論の話を書いた。同じ話が、そのまま署名にもなりたつ。

mandel59.hateblo.jp

タブレット画面に指で書く「署名」には、どんな意味があるんだろう。家に帰ってから、発行された「【情報変更】申込内容確認書」をよく確認してみると、「（契約者様ご署名欄）上記内容につきまして、確認の上契約致しました。」と書いてあって、その下にタブレットに書いた「署名」が一緒に印刷されていた。でも、タブレット画面に書く時には「上記内容」はまだ印刷もされていないんだし、「署名」が確認になっているわけがない。

タブレットに契約内容が表示されていたというわけでもない。まあ、たとえ画面に契約内容が表示されていたとしても、画面に表示されている内容とその後に印刷されている内容が同じという保証はないわけで、確認にならない。（タブレットの裏で動いているプログラムまで確認できるなら話は別だけど。）

まあ、世の中には既に「シュリンクラップ契約」とか「クリックオン契約」だとか、あるいはコンビニで画面にタッチさせて行う「本人確認」みたいな、いい加減な方法で溢れているんだけど、タブレットによる「電子署名」もその系譜のひとつなんだろう。

この「電子署名」は、ナンセンスだ。そういうナンセンスなはずの契約が、それでも機能しているのは、直接人間と人間が対面し、常識的なコミュニケーションを行っている中で行われている契約だからだ。タブレットに署名をする行為から実質的な意味が欠落していても、店員も客も嘘をつかず誠実で常識的な人間どうしのコミュニケーションが行われている。その場に関係した人間が、互いに互いを信用し、ハンコや署名などなくとも、人間自体への信頼によって、契約が成立している。そう、人間という情報メディアが信頼できる存在であるのなら、他のメディアで信用を担保する必要もない。意味もない「署名」も、人間がそれに意味のあることを信じていて、常識的なコミュニケーションに必要だという理由で、形骸化したまま使われ続ける。これは、「失われた魔法」と言うべきだろう。

考えてみると、この国では人間に対して求められる信頼性が高すぎる。日本では、人間自身が工業製品と同列に高品質高信頼が求められる存在であり、道徳的な人間と高度な職人芸が礼賛され、あらゆる社会の構成要素が理想を実現されているからこそ、優れた社会なのであると信じられている。これは、馬鹿げている。人間の品質に重きを置きすぎた結果として現実に起こっているのは、人間以外のシステムの脆弱化と、「壊れた人間」の疎外だ。

人間以外のシステムが壊れていても、全体の機能は損なわれないから放置される。そして、人間自体が壊れても、それを補完する他のシステムが壊れているのだから、壊れた人間をシステムから排除し、健全な人間に置換するしかない。

魔法の失われた、形骸化したシステムが社会に蔓延している。壊れたシステムの上で、人間がメディアとなって、かろうじて社会は成り立っている。壊れた人間は疎外される。システムの不全性を指摘するには、人間の不全性を大前提とするが、この社会では壊れた人間は排除されるのが大前提だ。私はシステムの不全性を知っているが、社会常識が、壊れた人間を導入する私の理性を排除する！

2016-03-04

Failures of Japanese dolls emoji 🎎

emoji

3rd March is hina-matsuri (雛祭り; Doll's Day) in Japan. There is an emoji for hina-matsuri: 🎎 JAPANESE DOLLS. I'm satisfied with the JAPANESE DOLLS emoji which Google ships, but some vendors unfortunately ship uncomfortable emoji for it. Let me explain.

If you were going to draw new emoji for JAPANESE DOLLS, you would search for images of JAPANESE DOLLS with Google Images. Please try it: https://www.google.co.jp/search?q=JAPANESE+DOLLS&tbm=isch

You'll see some kind of Japanese dolls, but most of them are NOT for hina-matsuri. The set of dolls for hina-matsuri, called dairi-bina (内裏雛; imperial dolls), is like this:
f:id:mandel59:20110301160724j:plain
https://commons.wikimedia.org/wiki/File:HinaDolls-Emperor-Empress-topplatform2011.jpg

Now, here is a Google's Japanese Dolls. (Emoji images in this article are via http://emojipedia.org/japanese-dolls/)
f:id:mandel59:20160304034233p:plain

Google's emoji grasps the point of dairi-bina very well. The emperor wears a crown and a scepter, and the empress wears a hair ornament and a fan. They are put on colorful tatami. Their faces are white as most of traditional japanese dolls have white skin.

How about other vendors' emoji? This is Apple's one:
f:id:mandel59:20160304035243p:plain

They don't have a scepter nor a fan, and their dress are weired. It looks not good, but barely recognizable as dairi-bina.

This is the Japanese Dolls emoji in Twitter:
f:id:mandel59:20160304034757p:plain

Why the right doll wears a ribbon? The emoji lacks important features of dairi-bina. The designer might not see a real dairi-bina but only Apple's one and the result of Google Images.

If you want to make a new emoji font, please look at the real object rather than emoji by other vendors, and know cultures emoji related to. Thanks.

UPDATE: Although Google's one is the most typical image of dairi-bina, it is not the sole correct form. There are many variations of dairi-bina. There are also stand-up one, origami one, and even Mickey and Minnie Mouse's one! If you would like to see more images of dolls for hina-matsuri, search for them with this link to Google Images: https://www.google.co.jp/search?q=%E9%9B%9B%E4%BA%BA%E5%BD%A2&tbm=isch

2016-03-01

プログラミングにおける〈式〉の考察まとめ

index プログラミング哲学

mandel59.hateblo.jp
mandel59.hateblo.jp

2016-02-22

RustでFizzBuzz まとめ

プログラミング index

Rust 0.1 (2012-01-26): プログラミング言語 Rust - M59の記録
Rust 0.4 (2012-11-16): Rust 0.4 - Ryusei’s Notes (a.k.a. M59のブログ)
Rust 0.7 (2013-07-06): Rust 0.7 - Ryusei’s Notes (a.k.a. M59のブログ)
Rust 0.9 (2014-01-15): Rust 0.9 - Ryusei’s Notes (a.k.a. M59のブログ)
Rust 0.10 (2014-04-04): Rust 0.10でFizzBuzz - Ryusei’s Notes (a.k.a. M59のブログ)
Rust 0.13 dev (2014-12-16): RustでFizzBuzz - Ryusei’s Notes (a.k.a. M59のブログ)
Rust 0.13 dev (2015-01-03): RustでFizzBuzz - Ryusei’s Notes (a.k.a. M59のブログ)
Rust 1.6 Stable (2016-02-22): Rust StableでFizzBuzz - Ryusei’s Notes (a.k.a. M59のブログ)

2016-02-22

Rust StableでFizzBuzz

プログラミング

前回: RustでFizzBuzz - Ryusei’s Notes (a.k.a. M59のブログ)

安定版がリリースされてからは特段試してなかったことに気づいたので、今更ながら安定版で動くFizzBuzzを載せておく。

fn main() {
    use std::thread::spawn;
    use std::sync::mpsc::channel;
    use std::borrow::Cow;

    let n = 100;
    let (tx, rx) = channel();
    for i in 0 .. n {
        let tx = tx.clone();
        spawn(move || {
            let i = i + 1;
            let b = match (i % 3, i % 5) {
                (0, 0) => Cow::Borrowed("FizzBuzz"),
               	(0, _) => Cow::Borrowed("Fizz"),
                (_, 0) => Cow::Borrowed("Buzz"),
                _      => Cow::Owned(i.to_string())
            };
            tx.send((i, b)).unwrap();
        });
    }

    let mut res = Vec::new();
    for _ in 0 .. n {
        res.push(rx.recv().unwrap());
    }

    res.sort_by(|t, u| (&t.0).cmp(&u.0));
    for t in res.iter() {
        println!("{}", t.1);
    }
}