型検査
デクスター・コゥゼンの "A Complete Gentzen-style Axiomatization for Set Constraints" とか読んで思ったこと。「Σコゥゼン σ-順序代数」という概念を考えた。Σ-kozen σ-ordered algebra, あるいは、Σ-kozen ordered σ-algebra かな。コゥゼンの termset …
原子論理式（atomic formula）ってのがなんか決まっているとき、それら原子論理式をベースに、∧（連言）、∨（選言）、¬（否定）を使って組み立てた式（formula）の全体が古典論理の式。ド・モルガンの法則を使えば、∧と∨のどちらかと¬だけでも古典論理の式は…
総称ラムダとかを参考にすると、次のようになる。ただし、これは厳密結合の推論で、型制約が出てこない。残念ながら、これでは実用にならないが、キレイにまとまる感じはある。S, Tなどは型項（または型表現）、f, gなどはコマンド項、M, Nなどは式（formula…
「勝たす異論」じゃねーよ。型推論とかいうとつっこまれそうだから、型解析にする。問題はパイプ結合だけ。 型ユニフィケーションをして、SIL命題のセットを出力する SIL命題セットを整理、計算（簡約）する。 SIL命題セットから代入を取り出して、再帰的に…
式Eの計算が、すべての部分式の計算も含めて安全に行われる（と予測できる）とき、《E》 と書く。式Eのすべての部分式とパイプ記号には、番号（一意的ならなんでもいい）が振ってあるとする。異なる番号が同じ場所を指す可能性がある。（[追記]そんなにイッ…
これは、あくまで構文的であり、決して意味的ではないことに注意。意味的な議論は解釈を決めないとできないし、解釈は色々あり、解釈ごとに定義は変わる。基底：コマンド呼び出しと定数 Dom(f::S -> T) = S Dom(c) = null Cod(f::S -> T) = T Cod(c) = sing(…
「文字列（名前）の集合と非負整数値」の組をシグニチャと呼ぶ。次の形で書く； {"foo", "bar"; 2}, {; 3}, {"baz"; 0}, {;0}。シグニチャパターンはオプションシグニチャパターンと引数シグニチャパターンの組である。オプションシグニチャパターンは： 文…
モノ（値）かコト（事態、動作）か モノとコトの相互変換 soft-nothing と hard-nothing ⊥の追加、厳密射、リフト 結局は、バンドルと層を使うことになるな。 集合圏の始対象／終対象の非対称性 関数と関数型（べき、指数） 特異値と非特異台 外延的記法によ…
u = undefined として、記号の乱用で u = {u}。ブラケット内の数値はランクが減少する量。 ●opt-right A ⊆ B+u [u!∈A] -----------[-1] A ⊆ B●opt-both A+u ⊆ B+u [u!∈A, u!∈B] -----------[-2] A ⊆ B●object object {pi: Ai} ⊆ object {pi: Bi} -----------…
Catyの型推論のために、分解還元法というのを考えた。シーケント計算とタブローの中間のような感じのもの。推論は逆向きに（結論から仮定へと）行われるので、次の用語を導入する。 分解図 -- 推論図（1ステップ）の逆 還元図 -- 証明図（nステップ）の逆 シ…
A?? → A? (A?|B) → (A|B)? など A? & B → A & B など A? & B? → (A & B)? bag [A?] → bag [A] (ハテナ定理には不要) @name A? → @name A (ハテナ定理には不要) ハテナ定理に必要なのは、演算子?, |, & に関する正規化だけ。
制限の追加ではなくて、領域（型の意味）の構成となっている演算は7種。 配列構成 オブジェクト構成 バッグ構成 （追加） ?演算 オプショナル構成 |演算 ユニオン構成 @演算 タギング構成 （追加） &演算 インターセクション構成 （追加） 配列、オブジェク…
たいした内容ではないけど、名前を付けておこう。 タグ排他性の原理：α≠β ⇒ (@α A)∩(@β B) = 0 単調性の原理：S ⊆T ⇒ tags(S)⊆tags(T) ハテナ定理：正規形の式なら、一番外側の'?'で確定型か不確定型か判断できる。 ν（nu）定理：ν(T) ≧ 1、ν(T) = n なら、T…
タグの基本はラベル（マーカー）。型情報としての利用は付随的／二次的であり、ラベルをインスタンス型情報として流用しているに過ぎない。利用可能な範囲も限定的である。バリデータをvalidateとすると： 基本は、validate(x, T) Tは型表現 validate(x) → v…
Tが型表現、またはその意味であるインスタンス領域だとして、tags(T) は、Tのインスタンスに付いている可能性のあるタグの集合。次のことを保証したい。 tags(T) は空ではない。 x∈T ならば tag(x) ∈ tags(T) そうなれば、S|T に対して、tags(S)∩tags(T) = 空…
形式系の微妙なところhttp://d.hatena.ne.jp/m-hiyama-memo/20090828/1251438577 より（竹内本を参考）意味じゃなくて、もっぱら記号の話。 定数とarity 0の関数 関数と演算子 fooとfoo()の区別 関数の引数渡しのバリエーション：可変引数、省略とデフォルト…
証明ターゲット S ⊆ y<
xは変数、Kは変数を含まない型マップ、Tは任意の型（型項、型表現）だとして、証明ターゲット x<
見た目はオブジェクト型（の型項、型表現）とまったく区別できないが、名前と型の対応を型マップと呼ぶことにする。'<<'の右側は型マップ。型マップがオブジェクト型と違う点は： ワイルドカードは現れない。 出現しない名前（プロパティ名）に対する型は単…
型演算'<<'を扱うためには、推論も拡張しなくてはならないが、実行時の検査条件を記述するPCL(path check logic)の変更のほうがむしろ大きい。今までのPCLは、pをパス、'_'を無名変数だとして、次の3つの形の式を原子論理式にすれば十分だった。 (p) exists(…
場合分けを17ステップに集約して、Erlangにしてみた。色々と問題もあるが、まーとりあえず動く。このエントリーに張り付けておく。 %% -*- coding: utf-8 -*- %% unify.erl -module(unify). -compile(export_all). %-define(DBG, 1). -ifdef(DBG). -define(P…
証明ターゲット S⊆T が完全失敗とは、S∩T = never が証明できてしまうこと。以下、S∩T = never を、S⊥T を書くことにする。 S⊆T が成功 ⇔ S⊆T が成立（健全性より） S⊆T が完全失敗 ⇔ S⊥T が成立 S⊆T が条件付きで成功 ⇔ S⊆T は成立しない（その意味では失敗…
左側分類と右側分類の番号が微妙にずれてしまった。が、もう直すのが手間だから、ずれた番号をそのまま使うことにする。ちと不恰好だが、もう勘弁してくれ。これで一応の結果としたい（間違いが発見されなければ）。後で元気があるときに、番号付けと順番を…
型を次の12種13種に分類する。 番号 型種別 旧構文 新構文 Erlang 備考 1 never型 never never never みんな同じ 2 any型 any any any みんな同じ 3 リテラル JSONリテラル JSONリテラル Erlangリテラル ほとんど同じ 3.1 数値リテラル JSON数値 JSON数値 Er…
型ユニフィケーションは、証明ターゲット S⊆T を証明する過程の中心的な処理である。処理の結果として、いくつかの「不定命題＝動的なチェック条件」を出力する。注意：このエントリーは他の関連エントリーとの兼ね合いで大幅に修正したり、場所を移動したり…
SILは、連言論理の枠組み（汎用）に、SIL固有の公理と推論規則を付け加えた論理システムである。●連言論理ベースの演繹系としてのSIL項と簡約計算Caty(新)スキーマ言語の型表現を型項、あるいは単に項（term）とも呼ぶ。項には変数（型変数）を含んでもよい…
SIL（Simple Inclusion Logic; 汁）は、Catyの型解析の基盤／背景となる論理システムである。型解析アルゴリズムは、SILを直接的に実装する必要はないが、アルゴリズムの解釈と正当性の主張はSILをベースに行う。注意：このエントリーは他の関連エントリーと…
用語法の注意型検査、型推論、型解析は同義語として使う、特に明確な区別はない。あるCatyスクリプト式（Caty式とも略称）に対する型解析が失敗するとは、否定的な結果を出して解析が成功することである。型解析は、成功する（肯定的な結果を出して終了する…
never型、undefined、型変数の値となる領域never型はいかなるインスタンスも持たない。never?型の唯一のインスタンスはundefinedと書く。undefinedは意味領域に存在する値だが、表層には出てこない。コマンドの入力にundefinedが入ることはなく、コマンドの…
型解析でもJSONパスは大活躍する。JSONパスでは、配列インデックス（非負整数値）とオブジェクトプロパティ名（文字列）により部分構造にアクセスする。インデックス／プロパティ名によるアクセスには、ブラケット記号（'[', ']'）とドット記号（'.'）が使わ…
