証明ターゲット 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パスでは、配列インデックス（非負整数値）とオブジェクトプロパティ名（文字列）により部分構造にアクセスする。インデックス／プロパティ名によるアクセスには、ブラケット記号（'[', ']'）とドット記号（'.'）が使わ…

この日付（100年前）でCatyの型解析関係記事を書きます。