型検査
[追記] ンギャ、http://d.hatena.ne.jp/m-hiyama-memo/20110509/1304896664 にも書いていた。アッチのほうが詳しいわ。[/追記]JSONスキーマのスキーマ属性 スキーマ属性名 適用対象となる型 意味 値の型 Catyのサポート状況 minimum number 最小値 number ○ …
有向グラフGのchildren関数 |G|→Pow(|G|) を、children(x) = {y∈|G| | xからyに向かう辺がある} で定義する。すべてのchildren(x)が全順序集合になっているようなグラフを考える。局所順序グラフと呼びたいが、誤解されそうだから、semifatグラフと呼ぶ。無…
似たことは何度も書いているような気がするが、2011年春夏シーズン向けのアルゴリズム（新作じゃないけど）。準備いろいろと記号の約束をする。 G, Hなどは有向グラフ 圏論の記法を借りて、グラフの頂点集合を|G|、辺集合を記号の乱用でGとも書く。 辺eに対…
えーと、最初に言っておくが； 複素解析ともリーマン面とも微分方程式とも特異点とも接続とも曲率とも、何の関係もない。被覆とは少し似ているし、（正錐により順序が付いた可換群としての）整係数ホモロジー群ともなんとなく関係ありそう。だが、、再帰的定…
ツリーをいちいちリアルに描くとめんどくさいから、三角形で略記。◎の「ツリー全体を表すノード」は、DOMの文書ノード（ルート要素ノードとは別）のようなもの。ルートノードとは別にあったほうが便利。参照ノードはリーフの位置にあるが、意味的には他の場…
絵だけ。説明は後で書く。別な場所に引越した。
Catyの型システムだと、1階述語論理と完全な対応が付く。 論理 英語 型 変数 variable 型変数 定数 constant symbol 具体型 関数 function symbol 総称型 述語 predicate symbol カインド 結合子 logical connective 結合子 限量子 quantifier 限量子 原子論…
コゥゼンのtermset algebraの公理を参考にして、型の代数を公理化しないとダメだと思うな。今のように実例ドリブンでは計算の根拠がハッキリしない。
言葉と記号法の問題が色々とある。型代入（type substitution, 行為とオペレータの意味がある）は構文的操作、型環境は意味論的な概念としよう。そう定義する。型環境は型評価に使う。型評価は型計算と言ってもいいが、型項を具体化して結果として具体型を求…
従来からのCaty用語も整理。TYPEを型（の意味）全体の集合、Mを計算モデル圏とする。 コマンド -- プロファイルと実行ボディの組。名前を持つか持たないかは理論上は重要ではない。 プロファイル -- 同一の型変数スコープ内に置かれた2つの型項のタプル ネイ…
新しい用語を導入しないと辛い。 型項 -- 型の構文的な表現、概念的には無限かもしれないGornツリー。 型制約 -- 型の等号、不等号、論理AND、論理OR、全称を含む論理式（formula） 連言的型制約 -- 論理ORを含まない型制約 原子型制約 -- 等号または不等号…
型解析系がやること： プロファイルのないスクリプトを解析して、プロファイル（宣言）を作る。 人間がプロファイルを書いているとき、そのプロファイルが正しいかどうかをチェック。 実行時の安全性を保証する。 1,2番はそれほど重要じゃなくて、重要なのは…
カインドを肥大させないように禁欲的に考えてたが、どうもこれがよくないかも。ブール半環の構造を持たせてもいいかもしれない。カインドKに対して、最大値 max(K) の存在を要請するのは無理がある。極大元の集合をtops(K)として、tops(K)が有限集合ならいい…
再帰的データ型の包含性の判定、わかった - 檜山正幸のキマイラ飼育記 メモ編 の「すべてのノードをくまなくチェックしたことの確認が難しい。」というハナシ。これも大丈夫だろう。とりあえず、練習問題としてサイクルがあるツリー（言葉は変だが）のノード…
SGMLに関連して割と有名な論文。"deterministic"を使っているが、決定性オートマトンの「決定性」とは違う。 Title: Deterministic Regular Languages (1992) （実際にはたぶん1991） Authors: Bruggemann-Klein, Wood URL: http://citeseerx.ist.psu.edu/vi…
結局、分かった後から眺めれば、正規表現型のときと事情は同じだ。あからさまに（陽に）正規表現を使ってなくても、再帰的な定義を入れれば、結局は正規言語になる。「再帰的データ型（の領域）＝正規言語」と言ってよいから、正規表現型の導入と再帰的なデ…
http://twitter.com/#!/hiyama_on_caty/status/67728585816948736 とか http://twitter.com/#!/hiyama_on_caty/status/68582156598910976 とかつぶやいてるだけだと後で分からなくなる。型の代数はブール半環層を係数とする多元環圏型の表現を台集合Aとその…
「各レベルの構成子、演算記号」にだいたいまとめたが、別な観点からまとめておく。型の全体を代数系と考える。これは2ソート代数で、「ラベル型」ソートと「データ型」ソートを持つが、単に「ラベル」と「データ」と言ってしまうこともある。Lをラベル型の…
集合圏の部分圏で、isoの族Eが指定されていて、Eに関して亜群になっているようなものUを考える。そして： 空集合と単元集合（少なくとも1つ）を含む A, B∈|U| ならば、A×B∈|U| A, B∈|U| ならば、A+B∈|U| 半環圏としての構造同型がEに入っている。 このような…
「片方向伝搬法は精度が悪い」と書いたが、簡単な例でも実際に精度が悪い(苦笑)。精度を上げるには、いくつかの方法がある。 論理系SILのなかで論理簡約をがんばる。 充足可能性問題の精度を上げる。 充足例問題の精度を上げる。 このなかで、充足可能性問題…
※ 内部的に別な形式を採用 △ 曖昧（明瞭でない） × 実装しない スキーマ属性名 適用対象となる型 意味 値の型 デフォルト値 minimum ※ number 最小値 number なし maximum ※ number 最大値 number なし exclusiveMinimum ※ number 最小値はイコールを含まな…
制約解決の部分は今までいいかげんでしたね。そもそも、連立不等式系なので、解があっても一意的に決まるわけではない。なにか「最適性」の基準を決めて、「制約（不等式の集まり）を満たしてコレコレを最大にする」ような最適解の問題にできればいいのだけ…
不等式的な型付けとは、ワイヤー（パイプ）が1本あると、その両端に型がラベルされる型付けの方法。普通の圏論だと、f:A→B, g:C→D が結合可能なのは B = C のときだけだが、Catyでは B = C は要求しない。B ⊆ C という集合の包含に関する不等式を要求する。…
お絵描き圏論とCatyScriptの変数など - 檜山正幸のキマイラ飼育記 とか 変数なしプログラミングとお絵描き圏論 - 檜山正幸のキマイラ飼育記 とかにデータフローグラフの例はある。ボックス＆ワイヤーの絵を描けばいいのだが、ワイヤリングのための特殊なノー…
次の5段階になるかな。 式（スクリプトコード）からデータフローグラフを作る。 データフローグラフをもとに、不等式版の型単一化を行い制約系（連立不等式系）を作る。 制約系（連立不等式系）は論理式なので、推論により論理式を簡約する（より短く単純な…
これから、型検査と制約解決の解説をするが、絵を使う。本質的にCatyScriptは絵図言語なので。既に絵を描いてスキャンした。が、見直したら細部（でもないか？）では絵が間違っている。直すのはめんどくさいので、絵はそのまま使う。いちおう修正は入れるが…
静的型検査のアルゴリズムは、2009年末から2010年はじめに（2010-01-05, 2010-01-11）だいたいは考えた。その手順を述べると： スクリプトコードからデータフローグラフを作る。（プログラムで実行するなら記号的な操作となる。） データフローグラフのワイ…
1910-01-05 - 檜山正幸のキマイラ飼育記 メモ編 「実行時型チェック条件」は、最弱事前条件から算出できるはず。最弱事前条件は、「可能な限り実行の邪魔をしない」条件。 制御不可変数、制御可能変数、伝搬変数って用語はよくない。独立変数と伝搬変数とい…
実行すべきプログラムを式と呼ぶ。Catyでは、式＝スクリプトコード。型を表す構文的対象を型項とする。型項を項として、包含関係 t⊆s を原子論理式とする論理系を考える。これはデクスター・コゥゼンのset constraintsと同じ。ただし、型変数が含まれて、全…
100年前の日付を付けてなんだかんだ書いている（例えば、http://d.hatena.ne.jp/m-hiyama-memo/19100110）。コゥゼンの集合制約（set constraints）を参考にしているが、types as sets の立場の型理論なので、type constraintsといったほうが実情にあってい…
