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

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
ところで、アーカイブってけっこう便利ですよ。タクソノミーも作成中。今は疲れるので作っていません。

2016-06-20 (月)

JavaScript界隈は日本語がお好き?

| 15:52 | JavaScript界隈は日本語がお好き?を含むブックマーク

JavaScriptのSVGライブラリを探していたら、bonsaiというライブラリが見つかりました。

ロゴもこんな(↓)ですから、これは「盆栽」ですね。

Kendo UIというUIライブラリもあるようです。

Kendo UIのオンライン・プレイグラウンドとして、「剣道 道場」というのがあります。

dojoといえば、prototype.jsとjQueryのはざまの時期に出現したUIライブリのひとつにDojo Toolkitってのがありましたよね。あれも「道場」なんじゃないの。今はどうしてるのか? と思ったら、開発は続いているようです。

Dojo Toolkit、YUI(Yahoo! User Interface)と並んでExt JSってのもありましたが、Ext JSを作っていた会社はSencha。

https://www.sencha.com/

ロゴは:

「煎茶」ですね。

海外でも広く知られている日本語と言えば「忍者」ですよね。jQueryのジョン・レシグは忍者の本書いています。

Ninjustu(忍術)をNinjitsuと書くこともありますから、Node.jsを扱っている会社のNodejitsuって「Node術」なのかな?

なんか、日本語が好きなんだね。

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

2016-06-13 (月)

Isabelle小ネタ:min-plus半環

| 11:32 | Isabelle小ネタ:min-plus半環を含むブックマーク

Isabelleをいじっているあいだ(=飽きるまで ^^;)は、ダイアリーにIsabelleの話が入るでしょう。今日は小ネタ。

ハイコンテキストな定数・記号の解釈」とかで話題にしたmin-plus半環をIsabelleで書いてみました。あの記事では、通常の演算子記号「+」「*」をオーバーロードする話でしたが、今回はエキゾチックな演算子記号「¥oplus」「¥odot」を使います -- 「零の概念とmax-plus半環の紹介」の説明と同じ記号法になります。

とりあえず書いてみたのは:[追記]コメント内の to proof は to prove ですね。テキストならすぐ修正するけど、画像だから面倒だ、直さない。[/追記]

セオリー記述をお見せするのにスクリーンショット貼り付けるのが、もうナントモ複雑な気分ですが、生のソースコード・テキストじゃ読むの辛いし。(一応、最後にテキストも貼っておきます。)

min-plus半環の台集合は非負実数の集合ですが、realやdoubleがIsabelleに(少なくともMainセオリーには)入ってなかったのでintを台にしました。¥oplus¥odotの定義は見りゃわかると思います。生ソースで ¥oplus は \<oplus>、¥odotは \<odot> で、TeXと同じ記号名です。([追記 date="2016-06-20"]Realというセオリーをインポートすると実数が使えますね。[/追記]

Isabelleについて: 証明支援系は何を目指し、どこへ向かうのか」でも触れたように、Isabelleのソースファイルは7ビットASCIIエンコーディングで*1、演算子記号に対する生のUnicode文字は入っていません。参考までに、「¥oplus」と「¥odot」のUnicodeコードポイントは:

min-plus半環が実際に半環の公理の満たすことを一部だけ示しています。この程度の定理なら自動証明でいけます。

「min-plus半環は半環である」という主張をIsabelleのなかでキッチリ示すには、半環を型クラスとして定義して、具体的に与えたmin-plus半環が型クラスのインスタンスになることを証明すれば良さそうです。「Coqで半環:アンバンドル方式の例として」でやったような、代数構造の階層的構成もたぶん型クラスで出来るでしょう。

ソースコードのテキスト:

[追記]間違いも画像と同じまま。簡単に直せるけど直さない。[/追記]

theory MinPlus
imports "Main"
begin

section \<open>Definition of MinPlus sum and product\<close>

fun minplus_sum :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "\<oplus>" 60)
where 
 "minplus_sum x y = min x y" 

fun minplus_prod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "\<odot>" 70)
where
 "minplus_prod x y = x + y"

section \<open>Some MinPlus expressions and evaluated values\<close>

value "1 \<oplus> 1" (* is 1*)
value "1 \<odot> 1" (* is 2 *)
value "10 \<oplus> 3\<odot>5" (* is 8*)

section \<open>Theorems (insufficient)\<close>

theorem sum_assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
apply(auto) (* We do not need to proof by hand. *)
done

theorem sum_comm: "x \<oplus> y = y \<oplus> x"
apply(auto)
done

theorem dist_l: "x\<odot>(y \<oplus> z) = x\<odot>y \<oplus> x\<odot>z"
apply(auto)
done

*1:HTML4までのデフォルトエンコーディングはISO-8859-1で、これは日本人には迷惑な話だったりします。Unicode対応しないのなら、7ビットASCIIのほうがいっそ清々しいですが、UTF-8でいいから対応してよ。

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

2016-06-09 (木)

Isabelleについて: 証明支援系は何を目指し、どこへ向かうのか

| 09:46 | Isabelleについて: 証明支援系は何を目指し、どこへ向かうのかを含むブックマーク

昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelleシステムを紹介しましょう。客観的な紹介ではなくて、僕の雑駁な印象記です。

内容:

  1. Isabelleの独自な世界
  2. Isabelleの未来

Isabelleの独自な世界

Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」より:

PIDE構想は、Isabelleプロジェクト/コミュニティを世の趨勢とは離れた孤立化へと導くのか、それとも、時代がPIDEの先進性にいずれ追いつき、PIDEがスタンダードな証明支援系UIとなるのか? なかなかに興味深いですな。

Isabelleが世の趨勢と離れるのか? という話をしてますが、有り体に言えば、もともとIsabelleは独特の文化を持った癖の強い処理系で、利用者は特殊な人々です。証明支援系を使いたくても、Isabelleを避ける人はいるでしょう。僕自身、Isabelleは「ダメだこりゃ」と思った1人です。

2005年の夏に、証明支援系を動かしたくなったことがあるのですが、そのとき僕が選んだのは Poly/ML + Isabelle ではなくて、 Moscow ML + HOL でした。当時のメモが残っています*1

Isabelleの何がそんなに嫌だったのかというと、余りにも不格好で気持ち悪い構文です。例えば、SML(Standard ML言語)で次のように書ける関数定義が、

fun conc [] ys = ys
  | conc (x :: xs) ys =  x :: (conc xs ys);

Isabelleでは次のように書きます。

fun conc :: "'a list => 'a list => 'a list"
where
  "conc [] ys = ys"
| "conc (x # xs) ys = x # (conc xs ys)"

Isabelleには外部構文(outer syntax)と内部構文(inner syntax)の区別があり、内部構文は引用符のなかに書きます。それがまるで文字列に見えてしまい、sh(シェル)スクリプトでevalを使っているような気持ち悪さです。「これは生理的に耐えられない」と思いました*2

今でも外部構文/内部構文の区別はそのままで、ソースコード気持ち悪さはパワーアップしています。

とあるIsabelleソースの一部*3 :

    from \<open>\<exists>!y. ?R m y\<close>
    obtain y where y: "?R m y"
      and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'" by blast
    show "\<exists>!z. ?R (succ m) z"

TeXコントロールシークエンス/XMLタグのような書き方は、特殊文字を表現するマークアップです。もはや、ソースコードを直接目視することやテキストエディタでの入力は考えてないようです。Isabelle/jEditで見れば:

そして、特殊文字の入力はシンボルパレットからどうぞ。

プログラミング言語APLでは、専用のキーボードや印字装置が必要だった、という話がありますが、IsabelleはAPL的方向に進んでいるようです。現代では、専用ハードウェアは不要で、ソフトウェアで入出力(編集と表示)をサポートできます。そのソフトウェアがIsabelle/jEditというわけです。

Isabelleのチュートリアルなどで、サンプルコードとして次のようなテキストが載っていたりします。

面食らいますよね。「いやっ、擬似コードじゃなくて、実際のソースコードサンプルを載せてくれよ」と。これが、実際のソースコードサンプルなんですよね。ただし、Isabelle/jEditじゃないと入出力(編集と表示)が出来ませんけど。

Isabelleの未来

「いったいどこへ向かう気なんだよ? Isabelle」、「それが正しい方向なのかい? Isabelle」と問いたくなります。

汎用の編集系Emacsや広く普及したSML処理系SML/NJを切り捨てたことは、より独自な閉じた世界へと向かっている印象を受けます。

しかし、ウェンツェルの意図はそうじゃないようです。むしろ逆で、証明支援系をより広い用途でより多くの人々に使って欲しい、だから古臭くて低機能なEmacsやSML/NJとは決別した、ということみたい。

ウェンツェルの2010年のスライド(のPDF)を見ると、PIDEという言葉こそ使っていませんが、この時点で既にIsabelle/jEditのアイディアは確立されていたことが分かります。

このスライドの冒頭には、次の2つの目標が掲げられています。

  1. 我々の証明エンジンをそこら辺にいる人々に使ってもらおう。(Make our provers accessible to many more people out there.)
  2. 証明エンジンのフロントエンドを作るのをうんと簡単にしよう。(Make building front-ends for provers really easy.)

証明エンジン/フロントエンドの用途のひとつとして、例えば教育が想定されています。

PIDEアーキテクチャは、Isabelleに限らず、他の証明支援系のUI構築にも使えるものです。実際ウェンツェルは、頼まれもしないのに(たぶん)、CoqのPIDEフロントエンドを試作したりしています。

現状のCoqのフロントエンドは、証明コマンド(タクティク)を実行して証明状態を遷移させていくものです。つまり、対話的スクリプティング環境なんです。これに対してPIDEのフロントエンドは、スクリプティング環境ではなくてドキュメント作成編集環境です。

「証明スクリプトから証明ドキュメントへ」 -- PIDEのキャッチフレーズのひとつです。動作記述である証明スクリプトでは、人がそれを読んで理解するのは困難です。宣言的で人が読める証明、それがウェンツェルの言う証明ドキュメント(proof document)です。

と、ここ数年のウェンツェルの主張を追ってみると、Isabelleの世界を広げようと尽力しているのが分かります。証明支援系の利用が広がらないネックは、「難読な証明記述言語と貧弱なユーザーインターフェースだ」との認識のもと、Isar(Isabelleの宣言的証明記述言語)とIsabelle/jEditにより障壁を取り除く戦略のようです。

この戦略が功を奏するのか? 僕には予測できません。が、このような戦略と方向性の文脈のなかで、11年前に抱いた悪印象はだいぶ緩和されました。広がりゆく(であろう)Isabelleの世界にちょいと入り込んでみようかな。


独白的余談:「ソースコードはプレーンテキストで書くべきで、プレーンテキストとして十分に読みやすくあるべき」だと僕は思っています。けど、プレーンテキストで見たときに気持ち悪いIsabelleコードは、Isabelle/jEditが綺麗に見せてくれたほうが助かります。引用符は見せないでくれ、型変数 'a もイタリックのaにしてくれ。

*1:結局このときは、MoscowML+HOLがビルド出来ず、Prolog処理系で推論計算しました。

*2[追記]今見たら、HOLでもけっこう引用符を使ってますね。|- や [ ] を使うと引用符を省けるので「多少はマシ」という判断だったのでしょう、覚えてないけど。[/追記]

*3:~~/HOL/ex/Abstract_NAT.thy lemma Rec_functional: 50行目

shiroshiro 2016/06/09 20:37 イマドキなら、Unicode使えばテキストオンリーでもそこそこ書けそうな感じはします。それはプレーンテキストなのかと言われると、ソースに日本語コメント混ぜるのにさえ最近まで躊躇してた世代としてはうーん、となるのですが、アメリカ人が日本語顔文字をばりばり使うネイティブUnicode世代だと実はそれほど抵抗は無いのかもしれません。

(最近では自分も、論文のアルゴリズムを書いてみる時などはギリシャ文字など抵抗なく使うようになりました。論文読み解きながらの入力ではタイプの手間はそれほど大きくありませんし。)

m-hiyamam-hiyama 2016/06/10 09:52 shiroさん、
僕はUnicodeも含めてプレーンテキストだと思ってますが、Isabelleの人達は、Unicodeはレンダリングの手段であっても、生のUnicode文字をソースに入れる発想はないみたいです。
そのへんは保守的。ASCII文化。
キーワードレベルでUnicodを使う言語が登場すると時代が変わるかもですね。
id := ∀α.λx:α.x とか書けて、ASCIIによる代替表現はC/C++のトライグラフのような扱い。

chiguri_schiguri_s 2016/06/10 11:58 jEditでの入力ではテキスト入力時にコマンドのように打つことで記号を出せますね。てっきり出来ている物もUnicodeテキストだと思っていたのですが、中身までコマンド風文字列だったとは。
AgdaはUnicodeでの記法をサポートし、むしろそっちを使って記述をすることが多いです。中身もUnicodeの記述になります。

m-hiyamam-hiyama 2016/06/10 14:35 chiguri_sさん、
> 中身までコマンド風文字列だったとは。
このへんのバランス感覚がなーんかオカシイ印象を受けます。
> 中身もUnicodeの記述になります。
それが普通ですよね。今のIsabella/jEditはUTF-8でさえ読めません。
記号の入出力にアプリケーション(Isabella/jEdit)が頑張るって発想も違和感あります。
かな漢字変換FEPの文化がない欧米だと、そうなっちゃうのかな。

nshinchan01nshinchan01 2016/06/19 00:33 思わずツイートするくらい笑わせてもらいましたw

2016-06-08 (水)

Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった

| 09:56 | Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなったを含むブックマーク

以前、証明支援系Coqの記事を書いたことがあります。今日話題にしたいIsabelle(イザベル)は、Coqのライバルと目される証明支援系です。最初のリリースが1986年ですから、実に30年間に渡って開発が続けられています(Coqもほぼ同時期にスタートしています)。十分に枯れた処理系でありながら、現在でも開発は活発で、新しい地平に向けて果敢な挑戦も試みられています。特に、ユーザーインターフェースの改善に熱心で、現在のGUIフロントエンドであるIsabelle/jEditには、驚くべき機能(の卵)が実装されています。

内容:

継続的チェッキング

理屈や背景は後回しにして、「継続的チェッキング」を簡単な実例で紹介します。

Isabelleは証明支援系ですが、プログラミング言語Standard ML(以下、SMLと略記)のコードエディタとしても使えます。7文字からなるSMLの式 val n=3 を、IsabelleシステムのGUIフロントエンドであるIsabelle/jEditで入力してみます。

赤いブロックがカーソル(キャレット)です。入力した式の評価結果が左側の出力パネルに表示されています。これだけ見ると、コンソールからSML処理系(Poly/MLといいます)を実行し、「コマンドラインとして入力して、コンソール出力を見る」(↓)のと同じように思えます。

いやいや、違うんです。ぜんぜっん違うのです。Isabelle/jEditは、コンソールによるRead-Eval-Printループとは、まったく違う対話的環境なんですよ。式の入力過程を1文字ずつ見ていきましょう。まず、'v'を入力したところ。

'v'だけではSMLの式になってないので、構文エラーが報告されています。それ以降も1文字入力するたびに、出力がめまぐるしく変わります。

そして、意味のある式 val n=3 が入力された瞬間に型推論と評価がされます。最初にお見せした画像の状況ですね(↓)。

「1文字入力ごとにテキストをインタプリタに渡してるだけじゃん」 -- まー、やっていることはそうなんですが、エディタとインタプリタ*1のあいだは、それ専用に設計された非同期プロトコルで通信して、コマンドラインごとの解析・評価ではなくて、ソースドキュメント全体での整合性が常に監視されています。

それを見るために、次の状態から始めましょう。

この状態で、カーソルを最初の行に移動して編集をします。すると:

関数値も再計算されています。関数の定義のほうを変更すると:

やはり、計算結果の値が変わりますね。

構文的/意味的エラーがあるかどうかをモニターするために、別パネルを出しておく必要はありません。証明ドキュメント内であれば、エディタの編集エリアの端っこ(ガター領域)にエラーのマーカーが出て、エラーメッセージはポップアップされます。

今の例は、SMLの小さなプログラム断片に対する継続的チェッキング(continuous checking)でしたが、Isabelle/jEditでは、大規模な証明ドキュメントに対しても、全体の整合性を常に監視し続けます*2。これは重い処理になり得るので、チェックの要求と応答は非同期的にやり取りされます。また、マルチコアCPUのネイティブスレッドを活用した並行処理によりチェックの高速化を図っています。

ウェンツェルのPIDE構想

Isabelleプロジェクトはロレンス・ポールソン(Lawrence Paulson)によって創始されましたが、現在、プロジェクトを牽引している中心人物はマカーリオス・ウェンツェル(Makarius Wenzel)です。

ウェンツェルは、証明支援系のユーザーインターフェースの革新を推し進めています。宣言的な証明ドキュメントに対する良好な編集GUIと、非同期/並列/継続的なチェッカーを緊密に連携させようとしているのです。その方式はPIDE(Prover IDE)と呼ばれています。PIDEの発音は次のようらしいですね。

PIDEはソフトウェア・アーキテクチャ/フレームワークの名ですが、形がそれほどハッキリしているわけではなく、ウェンツェルの思想/構想だと言ったほうが適切でしょう。

この構想を実現するために、証明支援系ユーザーインターフェースの“大将”であるProofGeneral/Emacsと袂〈たもと〉を分かち、一番メジャーなSML処理系であるStandard ML of New Jerseyとも縁を切っています。

NEWS of Isabelle2015:

* Support for Proof General and Isar TTY loop has been discontinued.

http://sketis.net/2016/isabelle-no-longer-supports-smlnj :

17-Feb-2016 marks the historic day when support for SML/NJ was removed from the Isabelle code base, ...

ProofGeneralの方式は、PIDE構想とは根本的に相容れないし、Standard ML of New JerseyはPIDEのための性能要求を満たせない、ということらしいです。

PIDE構想は、Isabelleプロジェクト/コミュニティを世の趨勢とは離れた孤立化へと導くのか、それとも、時代がPIDEの先進性にいずれ追いつき、PIDEがスタンダードな証明支援系UIとなるのか? なかなかに興味深いですな。

*1:最近の言語処理系では、インタプリタかコンパイラかハッキリしないものや分類しても意味がないものがあります。とりあえずここでは、SMLの「インタプリタ」と呼んでおきます。

*2:腕力だけで全体を調べるのは無理があるので、ユーザーが見てないところはサボるなどの工夫はされています。

2016-05-31 (火)

ストリング図とストリンググラフ、何が違う?

| 09:28 | ストリング図とストリンググラフ、何が違う?を含むブックマーク

絵算(お絵描き計算、pictorial/graphical/diagrammatic calculation)で使われる絵はストリング図(string diagram)と呼ばれます。とある文書でストリンググラフ(string graph)という言葉を見たんですよね。ストリング図の同意語だろう、と思ってました。

しかし、ストリンググラフの定義のなかで"node vertex"なんて奇妙な概念が出てきて、「はぁ、なにそれ?」 -- 少し調べてみました。

内容:

  1. ストリンググラフの起源と参考文献
  2. ストリング図を幾何学的に眺める
  3. ストリング図の組み合わせ的な表現

ストリンググラフの起源と参考文献

ストリンググラフは、ディクソン/ダンカン/キッシンジャーの次の論文で導入された概念です。

  • Title: Open Graphs and Computational Reasoning (2010)
  • Authors: Lucas Dixon, Ross Duncan, Aleks Kissinger
  • http://arxiv.org/abs/1007.3794
  • Pages: 12 pages

ただし、この論文では「ストリンググラフ」という言葉を使っていません。オープングラフ、あるいは単にグラフと呼んでいます。後からストリンググラフという呼び名を付けたようです。

ストリンググラフを主題的に詳細に扱った論文として、キッシンジャー(Aleks Kissinger)の学位論文とメリー(Alexander Merry)の学位論文があります。

どちらも長大で読む気になりません(僕は)。キッシンジャー、メリー、それとソロヴィヨフ(Matvey Soloviev)の次の論文なら短いです。

  • Title: Pattern graph rewrite systems (v3 2014)
  • Authors: Aleks Kissinger, Alex Merry, Matvey Soloviev
  • URL: http://arxiv.org/abs/1204.6695
  • Pages: 13 pages

ストリンググラフの理論は、証明支援系Quantomaticの実装のために開発された、という側面があるので、Quantomaticサイトも眺めておくといいかも知れません。(でも、Quantomaticについて知らなくても、ストリンググラフの理解に差し障りは無いです。)

ストリング図を幾何学的に眺める

ストリング図は、モノイド圏や高次圏のための計算手段ですが、ストリング図自体を研究対象とすることもあります。そのときの方向性として、とりあえず次の2つがあるでしょう(他の方向もあるかも、ですが)。

  1. ストリング図を図形とみて、位相的/幾何学的に調べる。
  2. 計算機によってストリング図を処理することを目指して、組み合わせ的に調べる。

最初に、幾何学的に調べるときの概略を例を出して説明します。

とあるモノイド圏のなかの射 f:X¥otimesY→Z と g:Z→W の結合(合成) f;g:X¥otimesY→W をストリング図で描くと次のようになるでしょう。描画方向は旗で示してます、上から下、左から右です(少しナナメってるけど^^;)。

射f, gをボックスで描くのは見やすくするためで、射は0次元の点で、対象が1次元の線です。次元に忠実に描くと:

この図形は平面に描いてあるとします。すると、X, Y, Z, Wは、閉区間 [0, 1] と同相な図形なので、なめらかな埋め込み写像 x, y, z, w:[0, 1]→R2 で定義できます。射を表す0次元セルは、x(1) = y(1) = z(0) がfの点、z(1) = w(0) がgの点、となります。

外の空間(キャンバス)であるR2をアプリオリには考えないなら、[0. 1] と同相な境界付き1次元多様体を境界で貼り合わせた複体(複合的な図形)を考えて、後から必要に応じてユークリッド空間や球面に埋め込むことになります

Globularでは、高次元のストリング図を考えますが、そのような図形は、1次元とは限らない境界/角付き多様体達を、境界/角で貼り合わせた複体と考えられます。

このような見方でストリング図(サーフェイス図)を扱う方法は次を参照:

ストリング図の組み合わせ的な表現

ここから先は、高次元のストリング図(サーフェイス図)ではなくて、1次元の(本来の)ストリング図を考えます。

コンピュータは、概念的な図形(1次元多様体の貼り合わせ)をそのまま認識はできません。離散的・組み合わせ的なデジタルデータにしてあげないとコンピュータは処理できません。

グラフ理論の意味でのグラフは、コンピュータで扱った実績が十分にあるので、ストリング図をグラフで表現しましょう。パッと見では、ストリング図は既にグラフになっているように思えます。でも、実は、ストリング図とグラフは、けっこう違っているのです。

この違いを明らかにするために、グラフ理論の用語としては頂点(vertex)と(edge)を採用し、ストリング図の点と線は、ノードワイヤーと呼びます。頂点=ノード、辺=ワイヤー なーんて単純なワケじゃないのです。

前節で例に挙げたストリング図を、ボックスをオダンゴにして再度描きます。

オダンゴをグラフの頂点(vertex)と考えるのは、まーいいでしょう。では、ワイヤーは辺(有向辺)でしょうか? 辺ならば、始頂点(source vertex)と終頂点(target vertex)を持たなくてはなりません。しかし、X, Yは始頂点を持ちませんし、Wは終頂点を持ちません。グラフとみなすには、ワイヤーの端点に頂点を追加する必要があります。ワイヤーの端点である頂点は、境界頂点(boundary vertex)と呼ばれます。入力側を進入境界(incoming boundary)、出力側は退出境界(outgoing boundary)と呼ぶこともあります。

射f, gの結合のときに、fの退出境界頂点とgの進入境界頂点を繋ぐことになりますが、繋いだ“跡”を残しておくと次のような図になります。

ワイヤー上にノードではない頂点が存在します。つまり、「ノードである頂点」と「ワイヤーの一部である頂点」ができます。前者をノード頂点(node vertex)、後者をワイヤー頂点(wire vertex)と呼びます。"node vertex"という奇妙な言葉は、こうして生まれたわけです。

ストリンググラフとは、今述べたような事情を考慮して、ストリング図を表現するためのグラフ構造です。頂点には、ノード頂点、進入境界頂点、退出境界頂点、ワイヤー(内部)頂点などの別があります。頂点に種類を設けることにより、ストリング図をグラフとしてエンコード出来ます。ストリング図 → ストリンググラフ のエンコードは、http://arxiv.org/pdf/1504.02716.pdf にあった次の図が分かりやすいですね(描画方向は下から上、左から右)。

絵算=ストリング図による計算を、ストリンググラフのグラフ書き換えにより実現できそうなことは何となく予想が付きます。そうなれば、コンピュータに絵算させることが出来るはずです。実際、色々な工夫やアルゴリズムが提案され、その一部はQuantomaticGlobularに実装されています。しかし、コンピュータ絵算はまだこれからの話です。

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

2016-05-30 (月)

次は誰?

| 16:15 | 次は誰?を含むブックマーク

歌詞で何やら騒動になったこの曲(2016年4月13日発売)

ディアナ・アグロンばっかり話題になりましたが、対比されているのは何故かアインシュタイン

少し後の2016年4月27日発売のこっちはシュレディンガー

次は誰かな、ファインマンあたり?

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

2016-05-27 (金)

圏論学習ソフト FQL++ 入門

| 09:59 | 圏論学習ソフト FQL++ 入門を含むブックマーク

関手データモデル/圏論データベース: その後の発展と現状 (2016)」 にて:

FQL IDEがサポートする4つの言語のなかで、位置付けがハッキリしないカワイソウなFQL++ですが、圏論の学習にはとても有用」という特徴があります。これだけを切り出して圏論学習ツールにして欲しいくらいです。FQL++に関しては、いずれ別な記事で語りたいと思っています。

FQL++について語ります。2013年の記事「圏と関手をできるだけ簡単に書き下す方法」の内容を、FQL++で書いてみます。

内容:

  1. FQL IDEのインストールと実行
  2. 圏を記述してみる
  3. FQL++の構文
  4. 無限圏の扱い
  5. 関手の記述
  6. FQL++と圏論

FQL IDEのインストールと実行

FQL IDEは、http://categoricaldata.net/fql.html からダウンロードできます。Javaのjarファイルfql.jarと、各プラットフォームごとのインストーラー(fql.dmg, fql.exe, fql.rpm, fql.deb)が用意されています。インストーラーにはJava8のランタイムが同梱されているので、事前にJava8をインストールする必要はありません。

Java8の実行環境が既にあるのなら、jarファイルだけでいいでしょう。そうでないならインストーラーをダウンロードして実行するのがお手軽です*1

jarファイルやインストーラーのファイル名にバージョンは埋め込まれていません。インストールしたソフトウェアを起動して[About]ダイアログを開いてもバージョン情報が出ないようです。インストールされたディレクトリのapp/CatDataIDE.cfgにバージョン情報が書いてありました、1.0です。

app.name=CatDataIDE
app.mainjar=fql.jar
app.version=1.0

Webページの説明では"FQL IDE"という呼称が使われていますが、ソフトウェア自体は"CatDataIDE"という名前のようです。

FQL IDEの起動方法は、プラットフォームやインストール方法により違いますが、起動してしまえば、プラットフォームに依存しないGUI操作となります。洗練されたGUIとは言いがたいですが、シンプルかつオーソドックスなので難しいことはないでしょう。

メニューのLoad Example:から、色々なサンプルを眺めると、FQL IDEがサポートする言語の雰囲気が分かるでしょう。各言語のマニュアルは次にあります。

圏を記述してみる

圏と関手をできるだけ簡単に書き下す方法」において、次のようなグラフで表される圏を、

次のような構文で記述することを提案しました。

category Foo {
 f: A -> B,
 g: B -> C,
 h: A -> C
}

この例を、FQL++で記述してみます。FQL IDEを起動して、[File]-[New FQL++]で新しいタブを作って、そこに次のように書きます。(デフォルトのタブはFQL構文なのでダメです。)

category Foo = {
 objects A, B, C;
 arrows
  f: A -> B,
  g: B -> C,
  h: A -> C;
 equations;
}

[Run]ボタンを押すと、FQL IDE内部に圏が生成されて、4種の形式: Schema, Graph, Table, Text で閲覧できるようになります。このなかでSchema形式は、圏の宣言(上記のソースコード)を可視化したグラフで、次のようになります。冒頭に挙げたGraphVizのグラフと、内容的には同じものです。

FQL++の構文

前節の例から分かるように、FQL++の構文は、「圏と関手をできるだけ簡単に書き下す方法」で僕が使っていた擬似構文と酷似しています。違いは、僕がキータイプ数を節約して出来るだけ短く書けることに拘ったのに対して、FQL++は冗長さを気にしてない点でしょうか。

FQL++の圏の定義には、objects, arrows, equations の3つのパートがあり、それぞれキーワードで始まりセミコロンで終わります。中身が空であってもパートを省略することはできません。したがって、一番短い圏の記述は次のようになります。

category EmptyCat = {
 objects;
 arrows;
 equations;
}

equationsの部分には、パス同値関係(path equivalence relations)を書きます。パス同値関係については、「圏と関手をできるだけ簡単に書き下す方法」や「衝撃的なデータベース理論・関手的データモデル 入門」で説明しています。また、パス同値関係を記述するためのパス記法に関しては「関手データモデル入門 3:とても便利なスピヴァック流パス記法」で述べています。

圏と関手をできるだけ簡単に書き下す方法」に出した、パス同値関係を含む例:

category Foo {
 f: A -> B,
 g: B -> C,
 h: A -> C

 where f;g = h
}

これをFQL++で書くと次のようです。

category Foo = {
 objects A, B, C;
 arrows
  f: A -> B,
  g: B -> C,
  h: A -> C;
 equations A.f.g = A.h;
}

もうひとつの例:

category Iso {
 f: A -> B,
 g: B -> A

 where
  f;g = A,
  g;f = B
}

これは、

category Iso = {
 objects A, B;
 arrows
  f: A -> B,
  g: B -> A;
 equations
  A.f.g = A,
  B.g.f = B;
}

この圏IsoをFQL IDEでGraph表示すると次のようになります。

無限圏の扱い

圏と関手をできるだけ簡単に書き下す方法」の2番目の例は次です。

category Bar {
 u: A -> X,
 v: X -> B,
 g: B -> B,

 C,
 Y
}

これをFQL++に翻訳すると:

category Bar = {
 objects A, B, C, X, Y;
 arrows
  u: A -> X,
  v: X -> B,
  g: B -> B;
 equations;
}

[Run]するとエラーになってしまいます。

Error in category Bar: Category is infinite (contains self-loop and no equations)

圏を生成するグラフに自己ループ辺があるので、g, g;g, g;g;g, ... などの無限個の射が生じます。自己ループ辺に限らずサイクルを持つグラフからは無限圏が生成されます。FQL++では、無限個の射を持つ圏が扱えません。パス同値関係を入れて“有限化”します。例えば、g;g = g という関係を入れると有限化されます。

category Bar = {
 objects A, B, C, X, Y;
 arrows
  u: A -> X,
  v: X -> B,
  g: B -> B;
 equations
  B.g.g = B.g;
}

有限個の射の全体は、Table表示やText表示で確認できます。次はText表示による射の列挙です。

arrows (11):
        A.u : A -> X
        A.u.v : A -> B
        A : A -> A
        B : B -> B
        C : C -> C
        B.g : B -> B
        X : X -> X
        Y : Y -> Y
        A.u.v.g : A -> B
        X.v : X -> B
        X.v.g : X -> B

関手の記述

次に関手を記述してみましょう。「圏と関手をできるだけ簡単に書き下す方法」の例は次のものでした。

category Foo {
 f: A -> B,
 g: B -> C,
 h: A -> C

 where f;g = h
}

category Bar {
 u: A -> X,
 v: X -> B,
 g: B -> B,

 C,
 Y
}

functor F: Foo -> Bar {
 C > B,
 f > u;v
}

この関手は、次の図で表すことができます。

僕が使っていた擬似構文における関手の記述ルールは:

  1. 同じ名前の対象は、デフォルトで対応付ける。明示的に対応を記述すればオーバーライドされる。
  2. 同じ名前の射は、デフォルトで対応付ける。明示的に対応を記述すればオーバーライドされる。
  3. パス同値関係の保存から必然的に導かれる(推論できる)対応は書かなくてもよい。

FQL++では、記述の省略はしない方針なので、すべて明示的に書き下します。上記の例は、次のように翻訳できます。ただし、圏Barを有限化するために、B.g.g = B.g を加えています。

category Foo = {
 objects A, B, C;
 arrows
  f: A -> B,
  g: B -> C,
  h: A -> C;
 equations
  A.f.g = A.h;
}

category Bar = {
 objects A, B, C, X, Y;
 arrows
  u: A -> X,
  v: X -> B,
  g: B -> B;
 equations
  B.g.g = B.g;
}

functor F = {
 objects
  A -> A,
  B -> B,
  C -> B;
 arrows
  f -> A.u.v,
  g -> B.g,
  h -> A.u.v.g;
} : Foo -> Bar

この関手 F:Foo→Bar は次のようにFQL IDEで図示されます。

圏Barの対象C, Yがやたらに離れちゃってるなー。射の対応関係も図ではよく分からない。Text表示の列挙を見たほうがいいでしょう。

On objects:
        A -> A
        B -> B
        C -> B

On arrows:
        B.g -> B.g
        A -> A
        B -> B
        C -> B
        A.f -> A.u.v
        A.h -> A.u.v.g

FQL++と圏論

FQL++はFQLの後継言語でした。FQLがSQLデータベースとの親和性を考慮した言語仕様だったのに対して、FQL++は、純粋に圏論的な概念、すなわち圏、関手、自然変換を記述することを目的とした言語です。データベースに特化した機能がなくても、圏論的な記述能力があれば大丈夫だろう、という目論見だったのでしょう。

しかし、圏、関手、自然変換だけで全てを記述することは、現実的には無理があったようです。現時点では、FQL IDEの主力言語はOPLに移っています。それでも、圏論的な概念の記述を目的とした言語FQL++は、圏論の学習には好都合で、教育的意義は大いにあります。

今回は基本的な圏と関手の記述だけを紹介しましたが、FQL++は、圏的コンビネータによるプログラミングやモナドとクライスリ圏(双対的にコモナドと余クライスリ圏)などもサポートしています。関手データモデル/圏論データベースの分野に限らず、一般的な圏論のトピックも扱えるソフトウェアだと思いますよ。

*1:最新版はjarでしか提供されないようです。一方、インストーラーがあるバージョンは安定版と考えられるので、通常の利用ではインストーラーからのインストールでいいと思います。

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

2016-05-23 (月)

猫と子供

| 11:40 | 猫と子供を含むブックマーク

これ、中国語だし、「もと動画から許可とってる?」とか思ったりもするのですが、「猫と赤ちゃん」の可愛さは無敵ですね。

D

この動画(↑)では、みんな(猫たち)赤ちゃんに気を使ってますね、爪を立てないようにしたり。でも、いつでも子供にやさしいとは限らないようです。

D

ところで、最初の動画の1分20秒辺りから、ミスタードーナツのポン・デ・ライオンだ。ミスタードーナツには何かと世話になりました、なつかしい。

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

2016-05-19 (木)

水素水広告

| 11:36 | 水素水広告を含むブックマーク

いらすとやさんの「水素水のイラスト」

これは笑えます。けど、笑ってくれない人もいそうで、それがちょっと怖いです。

このイラストのページの広告には(たぶん、ほとんどの場合)水素水の広告が出ます。それがまた可笑しかったりします。「スポンサードリンク」が「スポンサー・ドリンク」に見えて、さらに笑える。

僕は、ケラケラ笑いながら、ドリンクならぬリンクをクリックしてしまったんですよ。すると、その後水素水の広告に追い回されるハメに。

Googleの広告はすぐに拒否できます。が、Yahooプロモーション広告のほうは、アンケートに「興味ない」と答えてもすぐには止まらないようです。しばらくして、水素水広告は出なくなりました。

正確に言うと「人間向けの水素水広告」は出なくなりました。今は、「犬用の水素水」の広告が出てます。

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

2016-05-16 (月)

C/C++の思わぬ落とし穴(まーた、ハマっちまったぜ)

| 09:23 | C/C++の思わぬ落とし穴(まーた、ハマっちまったぜ)を含むブックマーク

上記の記事で、Shift_JIS(CP932)のコメントにまつわるトラブルを紹介しました。あまり時をおかずして、C/C++またハマりました。コメント事件ほどの意外性はないにしろ、事情を知らないと対処しにくいトラブルなので顛末を記しておきます。

この記事の内容は、僕が実際に体験した状況そのものではありませんが、それらしい例題を仕立てたので、ストーリーを追いかけてみてください。

内容:

  1. 例題:時刻付きのメッセージキュー
  2. 実装を変えてみると
  3. なんで、こんなことに
  4. 誰が悪いのか

例題:時刻付きのメッセージキュー

例題として、次のような機能を持つクラスを考えます。

  • 文字列メッセージを、時刻(タイムスタンプ)を添えてキューで管理する。

クラスのインターフェースを、次のようなヘッダーファイルに記述します。

// msgq.h
#ifndef MSGQ_H
#define MSGQ_H

#include <queue>
#include <string>

class MessageQueue {
public:
    void PostMessage(const std::string& msg);// 時刻を付加する
    const std::string TakeMessage(void);
    bool IsEmpty(void) const;
private:
    std::queue<std::string> queue_;
};

#endif

実装ファイルは次のようです。

// msgq.cpp Version 1
#include <time.h>    // time(), localtime()
#include <stdio.h>   // sprintf()

#include "msgq.h"

void MessageQueue::PostMessage(const std::string& msg) {
    time_t now;
    time(&now);
    struct tm *ptm = localtime(&now);
    char timeStamp[30]; // 多め
    sprintf(timeStamp, "[%4d-%02d-%02d %02d:%02d:%02d] ",
        ptm->tm_year + 1900,
        ptm->tm_mon + 1,
        ptm->tm_mday,
        ptm->tm_hour,
        ptm->tm_min,
        ptm->tm_sec
    );
    queue_.push(std::string(timeStamp) + msg);
}

const std::string MessageQueue::TakeMessage(void) {
    const std::string msg = queue_.front();
    queue_.pop();
    return msg;
}

bool MessageQueue::IsEmpty(void) const {
    return queue_.empty();
}

MessageQueueクラスをテストするためのプログラムも書きます。

// test-msgq.cpp
#include <iostream>
#include "msgq.h"

int main()
{
    MessageQueue msgq;
    msgq.PostMessage("hello");
    msgq.PostMessage("good morning");
    msgq.PostMessage("good afternoon");
    msgq.PostMessage("good evening");
    msgq.PostMessage("good night");
    while (!msgq.IsEmpty()) {
        std::cout << msgq.TakeMessage() << std::endl;
    }
    return 0;
}

このテストプログラムでは、メッセージに付加される時刻がほとんど同じになってしまいますが、それはいいとしましょう。

コンパイル&実行してみます。

$ g++ msgq.cpp test-msgq.cpp

$ ./a.exe
[2016-05-16 09:14:42] hello
[2016-05-16 09:14:42] good morning
[2016-05-16 09:14:42] good afternoon
[2016-05-16 09:14:42] good evening
[2016-05-16 09:14:42] good night

使っているコンパイラMinGWgccですが、今回の話では、コンパイラがなんであるかは影響しません。

実装を変えてみると

例題のプログラムはWindows上で動かすとしましょう。はじめに断っておくと、「まーた、Windows特有の話か」と言うと、そうでもなくて、ことの本質は、OS云々というよりはC/C++の仕掛けの問題です。

で、Windows上なので、time.hの関数を使う代わりに、Windows APIのGetLocalTime()関数を使うことにします。GetLocalTime()は次の点でtime.hの関数より便利です。

  1. time()とlocaltime()の2つを使う必要がなく、GetLocalTime()だけで済む。
  2. time_t型とstruct tm型(へのポインター)の2つを使う必要がなく、SYSTEMTIME型だけで済む。
  3. 年月に対して「+1900」「+1」のような補正をする必要がない。

GetLocalTime()版のMessageQueueクラスをVersion 2とします。

// msgq.cpp Version 2
#include <Windows.h> // GetLocalTime()
#include <stdio.h>   // sprintf()

#include "msgq.h"

void MessageQueue::PostMessage(const std::string& msg) {
    SYSTEMTIME now;
    GetLocalTime(&now);
    char timeStamp[30]; // 多め
    sprintf(timeStamp, "[%4d-%02d-%02d %02d:%02d:%02d] ",
        now.wYear,
        now.wMonth,
        now.wDay,
        now.wHour,
        now.wMinute,
        now.wSecond
    );
    queue_.push(std::string(timeStamp) + msg);
}

const std::string MessageQueue::TakeMessage(void) {
    const std::string msg = queue_.front();
    queue_.pop();
    return msg;
}

bool MessageQueue::IsEmpty(void) const {
    return queue_.empty();
}

さて、コンパイル&実行。

$ g++ msgq.cpp test-msgq.cpp
C:\Users\hiyama\AppData\Local\Temp\ccIGR1jP.o:test-msgq.cpp:(.text+0x55): undefined reference to `MessageQueue::PostMessage(std::string const&)'
C:\Users\hiyama\AppData\Local\Temp\ccIGR1jP.o:test-msgq.cpp:(.text+0xa2): undefined reference to `MessageQueue::PostMessage(std::string const&)'
C:\Users\hiyama\AppData\Local\Temp\ccIGR1jP.o:test-msgq.cpp:(.text+0xef): undefined reference to `MessageQueue::PostMessage(std::string const&)'
C:\Users\hiyama\AppData\Local\Temp\ccIGR1jP.o:test-msgq.cpp:(.text+0x13c): undefined reference to `MessageQueue::PostMessage(std::string const&)'
C:\Users\hiyama\AppData\Local\Temp\ccIGR1jP.o:test-msgq.cpp:(.text+0x189): undefined reference to `MessageQueue::PostMessage(std::string const&)'
collect2: ld returned 1 exit status

あんれー? エラーです。エラーの内容は、test-msgq.cppから参照されている`MessageQueue::PostMessage(std::string const&)'関数が見つからない、というものです。

なんで、こんなことに

現在時刻の取得に、time()とlocaltime()を使うか、それともGetLocalTime()を使うかは、実装者の判断であって、どっちを選ぶかは自由です。コンパイラに文句を言われる筋合いはないですよね。にもかかわらず、GetLocalTime()を使用するとダメなんですよ。なんで?

実は、(しばらく…が続く)

GetLocalTime()関数が直接の原因ではありません。問題なのは、MessageQueueクラスのメソッド(メンバー関数)であるPostMessage()です。「PostMessage」という名前そのもの、名前だけが問題なのです。

Windows APIにPostMessage()という関数があり、それと名前がかぶっているのです。しかし、Windows APIのPostMessage()は大域的関数、かたやクラスのメソッドなのだから、同じ名前でも問題がないだろう、と、そう思うでしょ。でも、ダメなんです。影響されちゃうんです。

Windows API関数の名前は、Windows.hのなかでマクロ定義された名前なんです。今回のケースでは、次のマクロ定義が作用します。

  • #define PostMessage PostMessageA

.cppソースコード内では、このマクロ定義が働いて「PostMessage → PostMessageA」という名前の置換が起きていたのです。定義された名前が MessageQueue::PostMessageA で、呼び出しに使った名前が MessageQueue::PostMessage ですから、呼び出せるわけがありません。

誰が悪いのか

やっぱりWindowsが悪いんでしょ -- とは言えないです。Windows.hに限らず、意図せぬマクロ置換によってコードを壊されることは、それほど珍しく無いと思います。コンパイルエラー/リンクエラーになってくれればいいですが、たまたま構文的に正しかったりすると相当分かりにくいでしょう。

C/C++では、プリプロセッサが言語処理系全体のなかでけっこう重要な役割を担っています。そのプリプロセッサは、C/C++の構文に関して何も知りません。名前のスコープのことなんか分からないので、闇雲なテキスト置換をやらかします。無知ゆえに間違いを犯しやすいのです。

プリプロセッサって、処理の入り口担当なんですが、処理対象に対する知識を全く持たないヤツに最初の処理を任せるってヒドイと思いませんか。栃木県生まれ東京在住で琵琶湖を見たことがない僕に、滋賀県の観光大使を任せるようなもんです(例えが意味不明? そうですね)。

昔に比べれば、プリプロセッサへの依存度は減ってはいる(inline関数とかconstによる定数とか)でしょうが、危なっかしいプリプロセッサ処理をナシにできないのかなー、と思ったります。

shiroshiro 2016/05/16 20:41 X11のヘッダだったかな。Statusという名前をマクロ定義していて、自分のコードの何かの名前とかぶってて悩んだことがあります。以来、自分が書く時はパブリックヘッダに含めるマクロ名には必ずプレフィクスをつけるようにはしています。

m-hiyamam-hiyama 2016/05/17 08:53 shiroさん、
マクロで意図せぬ置換は昔からありましたよね。他人様のものを上書きしないように用心してたこともありました。

#ifdef MY_MACRO
# error MY_MACRO is already defined.
#else
# define MY_MACRO
#endif

あと、一時的なマクロは使い終わるとすぐに #undef したり。でも、面倒さ(と、どことない虚しさ)でやらなくなってしまいましたね(苦笑)。

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