『抽象によるソフトウェア設計 -- Alloyではじめる形式手法』の献本をいただきました*1。書店に並ぶ前、7月9日に届きました。訳者のみなさん、ありがとうございます。 抽象によるソフトウェア設計−Alloyではじめる形式手法− 作者: Daniel Jackson,中島震,今井健男,酒井政裕,遠藤侑介,片岡欣夫出版社/メーカー: オーム社発売日: 2011/07/15メディア: 単行本（ソフトカバー）購入: 8人 クリック: 274回この商品を含むブログ (35件) を見る 「序文」、「監訳者序文」、「訳者あとがき」、そして第1章「はじめに」あたりを読んで感心しておりました。第1章はわずか4ページですが、素晴らしい、実にいいことが書いてあります。それで僕はスッカリ満足して（残りは読まないままで ^^;）いました。 金曜日（7月15日）にid:bonotakさんに、「アンタ、いくらなんでも

対象の集まり、射の集まりが集合となるような圏は小さい圏（small category）と呼びます。ここでは、小さな圏のなかでも特に、対象集合や射集合が身近なモノであるような圏を可愛い圏として紹介します。 内容： やせた圏 直積、直和、始対象、終対象 モノイド積とモノイド閉構造 もうひとつのモノイド閉圏 可愛い豊饒圏 やせた圏 Cが圏だとして、次の条件を満たすときやせた圏（thin category）といいます。 任意の対象A, Bに対して、ホムセットC(A, B) が空集合か単元集合。 Cがやせた圏のとき、関係 A ≦ B を次のように定義します。 A ≦ B ⇔ C(A, B) が空ではない Cはやせているので、「空ではない」は「単元集合である」でも同じです。次のことはすぐにわかります。 任意の対象Aについて、A ≦ A 任意の対象A, B, Cについて、A ≦ B かつ B ≦ C な

ものすごく久しぶりにXPathを使おうと思ったのですが、「XPathってなんだっけ？」という程度に忘れています。 細部はリファレンスマニュアルを調べれば分かることなので、概念的にどんなものかを思い出すのが先。概念や構造を手っ取り早く理解するには、抽象化したほうが都合がいいです。抽象化すると本質がコンパクトにまとまるので忘れにくいし、忘れても思い出す手間も少ないですからね。 内容： ツリー、有向グラフ、ノードセット 全順序付きノードセット 軸 コンテキスト ステップ ロケーションパスの評価 続きの記事：XPathの構文を割と具体的にまとめておく ツリー、有向グラフ、ノードセット XPathが相手にするデータ構造はツリーです。XMLのツリーには属性ノード、名前空間ノードとかもあるので、ノードにも辺にもいろいろな値（ラベル）が付着している有向グラフと考えましょう。ルートが特定されていてサイクルが

アミダくじによる場所（位置）の入れ替えは、置換を定義します。置換の全体を圏だと考えることができます。置換の圏を少し一般化して代入の圏を定義しましょう。一般化とは、「切れた線」と「枝分かれする線」を導入することです。単なる線（紐）だけではなく、印が付いたオダンゴを入れると、記号計算の枠組みとなる圏ができます。 内容： アミダの圏と置換の圏 代入の圏 圏Substの射の表現方法 ランク付きアルファベット上の代入の圏 アミダの圏と置換の圏 アミダの圏に関して僕は随分と色々書いています。 「アミダ」に関する記事一覧 比較的まとまった説明は次の2つの記事（2006年）にあります。 はじめての圏論 第7歩：アミダの圏 はじめての圏論 中間付録B：アミダとブレイド 2006年の記事だと、図形としてのアミダ図（Amida diagram）と、アミダ図により定義される置換（permutation）の区別が曖

KuwataさんがCatyのカインドの話を書いています。Catyのカインド（kind、種）は「型の型」ですが、高階の型としてはやたらに簡単な定義になっています。 Catyでは、JSONデータからなるデータ領域Dを固定して、Dの部分集合を型と考えています（Sets-as-Types解釈）。このため、型の型と言っても、ベキ集合を1回取るだけでモデルが作れます*1。これはどういうことかと言うと： 「値に関する概念」を、そのまま1レベル上げるだけで「型に関する概念」が得られる。 「1レベル上げる」作業は、ほとんど機械的と言えるくらいに単純です。 内容： 値と型、定数と関数 値の集合、型の集合 関数と集合の使い方をもう少し 構文が悩みの種 値と型、定数と関数 擬似言語で定数と関数を定義してみます。 /** 定数の定義 */ const two = 2; /** 右辺に算術演算を含んだ定数の定義 */

CatyScript2.0の言語仕様を検討してまして、その意味論をどうやって記述しようか？ と考えています。意味論の記述言語にCatyScript自体を使うという方法があります。次の記事で断片的にそれを試みています。 CatyScriptで記述するCatyシェル CatyScriptで記述するCatyのリクエスト処理 CatyScript2.0によりCatyScript2.0の仕様を書くのは割と容易で楽しい（やってみた）のですが、循環論法なのは確かです（意図的に循環させているのですがね）。やはり意味論には、もっと形式化された記述言語がふさわしいでしょう。 以前、CatyScript1.0（現状のCatyScrip)の意味論を表示的意味論風に書いたことがあります。 Catyのインタプリタ＝評価関数の表示的意味論 これは、数学的な関数概念を使って次のEval関数を定義する方法です。 Eval(

まっとうなハイパースキーマがないことはシリアスな問題なんだよなー。わしゃ困るわ、フントに。ハイパースキーマに向けて； まずはセレクター。 JSONデータが与えられたとき、その部分構造の集合を取り出す（セレクトする）式があると便利です（つうか、必要なんだけど、今）。CSSのセレクターやXPathのパターンのようなものです。もちろん、JSONPathをはじめとして既にいくつもの仕様＆実装が存在します。しかし、どうもオーバースペックです。もっと単純なJSON向けのセレクターを定義することにします*1。 内容： 構文の基本 JavaScriptを使った説明 いくつかの実例 フィルタリング条件の指定 プロパテイ名のクォーティング パス式としての利用 XJSONへの拡張 その他の拡張や略記 BNFによる構文定義 課題 構文の基本 これから定義するセレクターは、ドットで区切ったフィールドアクセス式にワイ

正月などは別にドーデモイイと思いつつも、明けましておめでとうございます。 「ハイパースキーマについて再び考えよう、っと」という次第で、年末年始も、ナントハナシにJSONハイパースキーマについて考えていました。ハイパースキーマが必要なのは、Webサービスの状態遷移をちゃんと記述するためです。目標から逆順に、必要なビルディングブロックをたどってみると： Webサービスの（クライアント側）状態遷移を記述するには、ハイパースキーマが必要である。 ハイパースキーマにはトリガー型とトリガー定義が必要である。 トリガー型の定義には、型コレクションが必要である。 トリガー定義には、パートとセレクター式が必要である。 パートの定義にはパス式が必要である。 型コレクションは、名前が仰々しいのですが、たいした概念ではありません。 パス式（path expression）はセレクター式（selector expr

ちょっと時間がたってしまったネタですが： プログラミングの出来る人と出来ない人の決定的な違い。 「プログラミングの出来る人と出来ない人の決定的な違い」？ ワンヤグさんの「プログラミングの出来る人と出来ない人の決定的な違い。」は、たくさんのブックマークを集めた記事。それに対して、id:JavaBlackさんが随分と否定的な記事を書き、さらにワンヤグさんが当該記事への追記として反論（らしきこと）を書いています。内容的に、ドチラかが全面的に正しいとは思えないし、ドチラかに味方する気もありません。 ですが、僕のセンサー（どんなセンサーかは最後に述べます）が反応したので、思うところを書いておきます。 時間順が前後しますが、まずはJavaBlackさんの記事のほうから。僕は、元記事「プログラミングの出来る人と出来ない人の決定的な違い。」を読む前に、JavaBlackさんの記事のほうを先に読んだのです。

1年半ほど前、「JSONスキーマとユーザーインターフェース」とか「JSONスキーマと列挙型」において、ランチの注文フォームを素材にスキーマとユーザーインターフェースの問題を考えてました。今、2010年末ならこの問題をどう扱うか？ まず、データ型の定義は次のようになります。 /** * ランチの注文 */ type LunchOrder = { /** 会員識別情報 */ "ident" : { "name" : string, "memberNum" : integer }, /** 今日の注文 */ "order" : { "mainDish" : ( "special"| "fish"| "meat" ), "drink" : ( "teaHot"| "teaIce"| "coffeeHot"| "coffeeIce" ), "dessert" : ( "pudding"| "stra

CatyScript2.0を企画してますが、実際に使えるようになるのはだいぶ先かな。 プログラミング言語がある程度の表現能力を持っていることの基準として、「自分で自分を記述できる」ことがあります。CatyScript2.0は、Catyのメカニズムを記述できる能力を持たせるつもりです。とはいえ、アルゴリズムの詳細を書くような用途にはまったく不向きです。概略を説明する擬似コードのように使えるが、擬似じゃなくて実際に動く、というのが目標。 CatyScriptを使ってCaty自身を記述するとはどういうことか、Catyの対話的シェルを題材にして実際にやってみます。その過程で、CatyScript2.0の（予定されている）機能も紹介します。 タグと分岐 Catyの扱うデータ構造はJSONをわずかに拡張したもの（XJSON）です。拡張した点はタグが付けられることです。タグはアットマークで始まる名前で、

MongoDBでは、dbがデータベース、collがコレクションだとして、db.coll.find(＜クエリ式＞) によって問い合わせが行えます。クエリ式として、JavaScriptの関数をそのまま渡すことができます。例えば、db.coll.find(function(){return this.a == 3;}) のように。 JavaScript関数には、コレクション内のドキュメント（オブジェクト）が順に渡されますが、引数ではなくてthisとしてドキュメントが渡されます。述語（boolean値関数）でコレクションを絞り込む高階関数をfilterとすると、db.coll.find(fun) は、filter(fun, db.coll) と同じことです。 findの引数に文字列が渡されると、その文字列はJavaScriptの関数ボディと解釈されます。db.coll.find(str) は、db

Catyのデータベースバックエンドの候補としてMongoDBを検討しています。MongoDBのクエリ言語が、現在Catyで実装しているクエリ言語とやたらに似ているんで笑ってしまいました。同じアイディアに基づき、構文もほとんど同じです。比較してみると -- 身贔屓な評価かもしれませんが -- Catyクエリ言語のほうがデキがいいと思います。 Catyでは、JSONデータを保存する貯蔵庫を「JSONストレージ」と身も蓋もない呼び方をしています。今まで紹介したことがなかったのですが、JSONストレージへのクエリ（問い合わせ）言語が存在します。JSONストレージとクエリ言語の設計と実装は、全部Kuwataさんによるものです。いつの間にか出来ていました。 現時点でのJSONストレージは、バックエンドにSQLiteを使っています。JSONデータ構造とRDB的なデータモデルにはセマンティックギャップがあ

Catyで何かしようとすると、スキーマ定義から始めます。スキーマ駆動なんです。スキーマ駆動の工程がどんな感じなのかをお伝えするため、割とリアリティがある実例を使います。細部は気にしないで全体の流れを感じ取ってください。 内容： 例題は林データ構造 ノードのデータ型を定義する ストレージ資源と例外 コマンドを定義してみる もっとコマンドを定義する 重いコマンドを分割してみる 林操作APIのまとめ 例題は林データ構造 「有向グラフにサイクルを作らない方法 -- レベル関数」において、有向グラフのサイクルを排除する話をしましたが、この方法が簡単に使えるのはグラフが木（ツリー）または木の集合体である林（forest）の場合です。例題として、林のデータ構造を扱うことにします。 林は何本か（0本でも1本でもよい）の木の集まりです。下の図を見てください。林のなかの木の本数を勘定すると4本です。ルートノー

http://twitter.com/hiyama_on_caty でゴニョゴニョ言っていた（http://twitter.com/hiyama_on_caty/status/26596332016 の前後）の件を解説してみます。 Catyのデータ型自動変換のメカニズム 次のようなデータ型を考えます。 /** ピザの注文のデータ型 */ type PizzaOrder = { // ベースタイプは必須 "baseType" : ( "プレーン" | "マルゲリータ" | "マリラーナ" | "ロマーナ" | "ナポリターナ" ), // トッピングのデフォルト値は []（空列） "topping" : [ ( "オニオン" | "ズッキーニ" | "トマト" | "ブラックオリーブ" | "マッシュルーム" | "コーン" | "エビ" | "ブロッコリー" | "ベーコン" | "モッツ

「Webサービスの設計： ハイパーオブジェクトとトリガー」において： 僕は「Webとはハイパーリンクなり」と考えているので、Web APIでもなんでもハイパーリンクを使ってないなら「Webっぽい」とは思いません。RPC（遠隔手続き呼び出し）的な要素を取り入れても、ハイパーリンクを活用しているならWebっぽいでしょう。「っぽい」とか「らしい」は単なる趣味嗜好の問題ではなくて、ハイパーリンクの活用は大きなメリットがあります（そのメリットの説明は今日[注：2010年8月11日]はしませんが）。 「ハイパーリンク活用の大きなメリット」について、今日（2010年8月25日）は説明します。 内容： 遠隔呼び出しとHTTP インターフェースと手順の合意 あなたに任せるわ、私は言われるまま 理想のケースは人間がクライアントのとき 状態遷移モジュール インターネット／Webの驚嘆すべき頑健性 遠隔呼び出しと

「Webサイト」、「Webアプリケーション」、「Webサービス」、「Web API」などの用語の区別はそれほど明確でもないし、きっちり区別して使うのもめんどくさいので、ここでは、これらを総称してWebサービスと呼んでしまうことにします。 山本陽平さんは、その著書『Webを支える技術』のなかで、人間がブラウザを使って利用するWebサイトとプログラム向けのWeb APIを区別すべきではないと述べています。この点は僕もまったく同感・同意です。 人間が相手となると、視覚的な効果や装飾、JavaScriptを使った操作性などにフォーカスが向けられ、Web APIとはまったく別物のような印象を与えます。しかし、各ページが持つべき情報やページ遷移の有向グラフ構造などは、相手が人間でもプログラムでも同じだと思うのです。そんな事情で、Webページの機能的／情報的なエッセンスを表現したHTML文書をクリーンH

とある論文に、パズルのネタになりそうな計算の話があったので紹介します。予備知識は特に要りませんが、けっこう難しい。 小学校で最初に習う計算は足し算です。しばらくして掛け算を習います。整数の掛け算、例えば 3×4 は、足し算の繰り返しとして導入することもできます。3×4 := 3 + 3 + 3 + 3 。 掛け算を先に習って、掛け算をベースに足し算を定義するような学習コースは聞いたことがありません。が、宇宙のどっかに、そんな順序で計算を教えている星があるかもしれません。我々地球人には不自然ですが、掛け算をもとに足し算を定義することは出来るようです。 実数の集合に対して、足し算を忘れてしまい、掛け算だけを考えます。掛け算の法則は全部使えます。具体的に書けば： (a×b)×c = a×(b×c) a×b = b×a a×1 = a a≠0 ならば、a×a' = 1 となるa'（aの逆数）が存在

正規表現と構文図について解説します。オートマトンについても詳しく述べます。オートマトン・スゴロクで遊びましょう！ 世間でよく知られている／使われている概念・方法にはこだわらず、僕（檜山）の感覚で一番わかりやすいと思われる筋書きと用語法／図式法を使って説明します。この記事に目を通して“感じ”が掴めたら、形式言語理論の教科書を読み始めることが出来るでしょう。 [追記]この記事の内容に対する具体例は、「正規表現とオートマトン：なんだ簡単じゃん、JavaScriptによる実装」にあります。[/追記] 内容： 正規表現 正規表現の例 構文図 基本記号 連接 選択 省略可能 繰り返し ストレートワイヤーによるレイアウト調整 有限状態オートマトン 有限状態オートマトンの実行 バックトラックと先読み スゴロクとオートマトン コマをたくさん使うスゴロクと並列処理 非決定性オートマトンと決定性オートマトン 正