このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

Jcentric型システム:ホスト型システムの要件

Jcentric(JSON centric)型システムは、既存プログラミング言語の型システムに埋め込んで、あるいは寄生させて使うことになります。埋め込み先/寄生先となる型システムをホスト型システムと呼ぶことにします。今、Kuwataさんが実装しているケースでは、Pythonの型システムがホスト型システムです。

Jcentric型システムはプログラミング言語中立、つまり、色々なホスト型システム内に埋め込めるように設計しています。現存するたいていの型システムに埋め込めると思いますが、Jcentric型システムをサポートするために必要な条件があります。それを述べます。

内容:

  1. データインスタンスとデータ領域
  2. 基本的な命題の判断可能性
  3. ボトムと普遍領域の存在
  4. 配列構成とオブジェクト構成、再帰的構成
  5. JSONの型とは何か
  6. Jcentric型システムの要件は?

データインスタンスとデータ領域

個々のデータを表現する対象物をデータインスタンス、または単にインスタンスと呼びます。インスタンスと呼ぶこともあります。データインスタンスの集合をデータ領域、または単に領域と呼びます。データインスタンスの勝手な集まりをデータ領域と呼ぶわけではなくて、ひとまとまりの全体として把握できる(例えば名前を付けて再利用できる)ような集合だけをデータ領域と呼びます。

ホスト型システムは、データインスタンスとデータ領域という概念を持たなくてはなりません。

基本的な命題の判断可能性

xがデータインスタンス、A, B がデータ領域とするとき、次の命題の真偽が確実に判断できる必要があります。

  1. x∈A -- インスタンスxは領域Aに所属する
  2. A ⊆ B -- 領域Aは領域Bに包含される
  3. A∩B = 0 -- 領域Aと領域Bの共通部分は空である

これらの命題の判断(真偽決定)可能性を次のように呼びましょう。

  1. 所属性の判断可能性
  2. 包含性の判断可能性
  3. 無共分性の判断可能性

「判断可能」の意味は、具体的に実行できるアルゴリズムが存在することです。そのような判断が正しいという条件は、A, Bが無限領域なら超越的になります(A, Bが有限領域ならシラミツブシ方式で確認可能ですが)。

  • A ⊆ B ⇔ ∀x.(x∈A ⊃ x∈B) (「⊃」は含意記号)
  • A∩B = 0 ⇔ ¬∃.(x∈A ∧ x∈B)

このような判断は問題なくできると思うかもしれませんが、実際の型システムでは、何らかの規約やライブラリを追加しないと判断できないこともあります。例えば、"12" と 12 が等価に使えるようなシステムでは、「"12" ∈ 整数領域」がなんとも言えません。そうなると、「整数領域∩文字列領域 = 0」もハッキリしません。

ボトムと普遍領域の存在

ボトム(⊥)は不在や未定義を表す値です。未定義を表すために、JavaScriptのundefinedのような値(データ)があると便利です。ただし、未定義がモノとして表現できないなら、コトとしての表現でもかまいません。例えば、例外を発生させるとかです。次のいずれかでボトムを実現します。

  1. 未定義を表す値
  2. 未定義による例外/エラーの発生

任意のデータ領域Aに対して、A ⊆ U となるような領域Uを普遍領域と呼びます。ホスト型システムに普遍領域が存在することを要求します。これは、ユーザー定義型を自由に追加するために必要で、ユーザー定義型がないなら特に必要ありません。

配列構成とオブジェクト構成、再帰的構成

JSONデータの全体は、基本となるスカラーデータの領域からはじめて、配列構成とオブジェクト(キーバリュー・レコード)構成を再帰的に繰り返して得られます。ですから、素材となる領域からの配列構成、オブジェクト構成ができないと困ります。これらの構成は再帰的に適用できて、最終的には極限領域としてJSONデータの領域が得られます。

JSONデータ領域の構成を厳密に述べると面倒ですが、多くの型システムは、配列とオブジェクトの再帰的な構成をサポートしています。

JSONの型とは何か

型がいつでも名前を持つ必要はありませんが、名前を持つ型(named type)について考えます。ここで、名前とは文字列やシンボルです。

ホスト型システム内に実現されるJSONの型(ホスト型システムの型ではない!)は、次の構成要素からなります。

  1. 型の名前
  2. 型の表現領域
  3. 型の値領域
  4. 表現領域上のイコール関係
  5. 表現領域上で定義された値を求める関数

表現領域値領域とは、「Jcentric型システム:プラグインによるユーザー定義型」に出現した字句空間、値空間(もともとはXML Schemaの用語)とほぼ同じです。字句空間より一般性がある状況を考えるので、表現領域と呼ぶことにしました。

型の名前をtとして、各構成要素を次の記号で表します。

  1. t -- 型の名前
  2. Rep(t) -- 型の表現領域
  3. Val(t) -- 型の値領域
  4. eq[t] -- 表現領域上のイコール関係
  5. val[t] -- 表現領域上で定義された値を求める関数

表現領域Rep(t)と値領域Val(t)には、前もって何の仮定もしません。Val(t) = Rep(t) でも、Val(t)∩Rep(t) = 0 でもかまいません。eq[t](x, y) が x = y (ほんとに同じ)を意味する必要はありませんが、eq[t] は同値関係になっているとします。

  • eq[t]:Rep(t)×Rep(t)→{true, false}
  • val[t]:Rep(t)→Val(t)

また、次の条件を仮定します。

  1. eq[t](x, y) ならば、val[t](x) = val[t](y)
  2. x∈(Rep(t)∩Val(t)) ならば、val[t](x) = x

次の2つの条件は必須ではありませんが、成立していれば便利です。

  1. Val(t)⊆Rep(t)
  2. val[t]は全射

前もって次の作業をすれば、上の条件を満たすようにできます。

  1. Rep'(t) = Rep(t)∪Val(t) とする。
  2. val'[t](x) = if x∈Val(t) then x else val[t](x) と定義する。
  3. Rep'(t)とval'[t]を、改めてRep(t), val[t]とする。

よって、以下の条件を最初から全部仮定してもかまいません。

  1. Val(t)⊆Rep(t)
  2. val[t]は全射
  3. eq[t](x, y) ならば、val[t](x) = val[t](y)
  4. x∈Val(t) ならば、val[t](x) = x

Jcentric型システムの要件は?

以上に述べたことは、ホスト型システムの要件でした。たいていのプログラミング言語の型システムが要件を満たしていると思います。つまり、たいていのプログラミング言語の型システム内にJcentric型システムを埋め込めるはずです。

複数のJcentric型システム実装が存在すると、プログラミング言語によらない、実装によらない、Jcentric型システム自体の特性や機能が問題になってきます。「これは、××言語によるJcentric型システムの実装である」という主張の根拠、判断基準を与えるものです。その判断記述を形式的に記述できるといいんですが、完全にやるのは無理そう。参照実装や自然言語をまじえてタラタラやってみることにしますわ。