このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」(http://d.hatena.ne.jp/m-hiyama-memo/)のデータを移行・保存したものであり、今後(2019年1月以降)更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

1910-01-01から1ヶ月間の記事一覧

右に型更新演算子が含まれるとき

証明ターゲット S ⊆ y<

左に型更新演算子が含まれるとき

xは変数、Kは変数を含まない型マップ、Tは任意の型(型項、型表現)だとして、証明ターゲット x<

型解析:用語 型マップ

見た目はオブジェクト型(の型項、型表現)とまったく区別できないが、名前と型の対応を型マップと呼ぶことにする。'<<'の右側は型マップ。型マップがオブジェクト型と違う点は: ワイルドカードは現れない。 出現しない名前(プロパティ名)に対する型は単…

型解析:動的なPCL (Path Check Logic)

型演算'<<'を扱うためには、推論も拡張しなくてはならないが、実行時の検査条件を記述するPCL(path check logic)の変更のほうがむしろ大きい。今までのPCLは、pをパス、'_'を無名変数だとして、次の3つの形の式を原子論理式にすれば十分だった。 (p) exists(…

型解析:型ユニフィケーション in Erlang 暫定

場合分けを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 は成立しない(その意味では失敗…

型解析:型ユニフィケーションの分類結果と処理順番

左側分類と右側分類の番号が微妙にずれてしまった。が、もう直すのが手間だから、ずれた番号をそのまま使うことにする。ちと不恰好だが、もう勘弁してくれ。これで一応の結果としたい(間違いが発見されなければ)。後で元気があるときに、番号付けと順番を…

型解析:気分転換にErlang

型を次の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固有の公理と推論規則を付け加えた論理システムである。●連言論理ベースの演繹系としてのSIL項と簡約計算Caty(新)スキーマ言語の型表現を型項、あるいは単に項(term)とも呼ぶ。項には変数(型変数)を含んでもよい…

型解析:SILへの準備としての連言論理

SIL(Simple Inclusion Logic; 汁)は、Catyの型解析の基盤/背景となる論理システムである。型解析アルゴリズムは、SILを直接的に実装する必要はないが、アルゴリズムの解釈と正当性の主張はSILをベースに行う。注意:このエントリーは他の関連エントリーと…

型解析:雑多な予備知識

用語法の注意型検査、型推論、型解析は同義語として使う、特に明確な区別はない。あるCatyスクリプト式(Caty式とも略称)に対する型解析が失敗するとは、否定的な結果を出して解析が成功することである。型解析は、成功する(肯定的な結果を出して終了する…

型解析:細かい注意点

never型、undefined、型変数の値となる領域never型はいかなるインスタンスも持たない。never?型の唯一のインスタンスはundefinedと書く。undefinedは意味領域に存在する値だが、表層には出てこない。コマンドの入力にundefinedが入ることはなく、コマンドの…

型解析:タグ付きJSONパス

型解析でもJSONパスは大活躍する。JSONパスでは、配列インデックス(非負整数値)とオブジェクトプロパティ名(文字列)により部分構造にアクセスする。インデックス/プロパティ名によるアクセスには、ブラケット記号('[', ']')とドット記号('.')が使わ…

Catyの型解析

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