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)が有限集合ならいい…

関係圏とスパンの圏 - 檜山正幸のキマイラ飼育記の話は当座の応用があって、オートマトン（有限とは限らない）の圏をベースにしてSpan(C)を作ると面白い。スパンの左右の足を射影と考えると、ボディのオートマトンの2つの影を見ているように思える。逆に、ボ…

http://twitter.com/#!/hiyama_on_caty/status/71717718457450497 あたり： なんか行き詰まり感があるなー。今日は、この行き詰まりを解消するために、、、何をすりゃいいんだかね？ こういうときは、アイディアが足りないというよりは；見落としや勘違いを…

大局的プログラミング（programming in the large）：手でモジュールの計算をするときの演算記号を決めておこう。キーボードでも書けるようにアスキーベース。 演算記号 意味 + モノイド積、モジュールの集約／マージ |> 圏の結合、普通の結合 :> 閉じた吸収…

再帰的データ型の包含性の判定、わかった - 檜山正幸のキマイラ飼育記 メモ編 の「すべてのノードをくまなくチェックしたことの確認が難しい。」というハナシ。これも大丈夫だろう。とりあえず、練習問題としてサイクルがあるツリー（言葉は変だが）のノード…

[追記]category of modules って言葉は使えないわ。加群圏だもんな。 [/追記]ゴグエンの大局的プログラミング（programming in the large）の発想でモジュール計算をしていたら、GoI構成とコンパクト閉圏が出てきてビックリ。モジュールMとNが提供（provide…

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とその…

どこで実験していたか忘れる。 ~/ProjectCaty/latest-*/main/ui/pub/js/ ここにある。Webからは /ui/js/ として見える。

ココ で話題になっていた「名探偵コナン」の最新作（15作目)『名探偵コナン 沈黙の15分（クォーター）』を次男と見てきた。以前も次男とコナンみたけど、いつだったか？ 2009年の『漆黒の追跡者＜しっこくのチェイサー＞』か。あのときのようなムチャクチャ…

「各レベルの構成子、演算記号」にだいたいまとめたが、別な観点からまとめておく。型の全体を代数系と考える。これは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 - 檜山正幸のキマイラ飼育記 メモ編 「実行時型チェック条件」は、最弱事前条件から算出できるはず。最弱事前条件は、「可能な限り実行の邪魔をしない」条件。 制御不可変数、制御可能変数、伝搬変数って用語はよくない。独立変数と伝搬変数とい…

動くようになった： 変数生成 '>' 変数参照 '%' パイプラインの一時的終了 ';' eachによる変数スコープ（つうかエクステント） casmでスクリプトコマンド定義 kindのナンチャッテ第一段階。 バッグ型 actions/*.cara 新しいスキーマ属性 maxProperties, minP…