STEM
ERモデリング 外部世界を「集合、写像、関係」でモデル化して、ノード、アロー、ブリッジで図示する。 TCモデリング ERモデリングの成果物であるER図を変形してTC図を作成する。 ER＝Entity-Relationship、TC＝table-column。ER図の構成要素： 《ドメイン》…
《リレーション》 関係にあらず 《タプル》 タプルにあらず 《ジョイン》 結合にあらず 《ドメイン》 域、領域にあらず 念のための退避（ほとんど使わないけど）： 関係→関連 タプル→順序タプル 結合→合成 域→始域 グラフ用語の追加・概念の追加 装飾：形状…
ともかく用語がたくさんある。 表示（denotationやrepresentationじゃなくて、presentation） 生成系と関係 ： 古典的な用法、たぶん群表示が起源 生成系と等式系 ： 関係が等式のとき 生成系 ： 関係も生成系の一部と考える コンピュータッド ： 次元（次数…
RDB的タプルの呼び名： レコードみたいなものに関して - 檜山正幸のキマイラ飼育記 メモ編 いろいろな言語での Map, Dictionary 的なものの名前 - Qiita ハッシュマップ、ハッシュ、マップなどは実行時に名前を持っているもの。構造体やオブジェクト（の多く…
リレーションの理論はダメだ - 檜山正幸のキマイラ飼育記 メモ編の続き。 RVA（relation valued attribute）って、ホントにバカじゃないの?! group-byの結果を再びリレーションとして表現するために導入したらしいが、なんでそんなバカなことする？ Rel(A, B…
レコードライクなデータ構造 レコード ロー、行 （名前付き）タプル 構造体 オブジェクト 名前・値ペアの集合 フィールド相当 成分、コンポネント 項目、アイテム カラム、列 メンバ プロパティ フィーチャ 属性、アトリビュート 要素 スロット 名前がないと…
タプルを入れ子ペアとするか、インデックス集合からの写像とするか。 インデックス集合からの写像のほうが扱いやすい。これを仮にマップタプルと呼ぶ。 入れ子ペアを右標準形または左標準形にすれば、{1, ..., n}上で定義されたマップタプルと対応が付く。 …
論理式（formula）は極性（ポラリティ polarity, 符号 sign）を持つとする、正負号（positive sign）と負符号（negative sign）。正負号は省略してもよい。（書き方は後で）正（極性が正）の論理式の集まりを論理資産（logical asset(s)）、負の論理式の集ま…
前提（premise; プレミス）は次のもの達の総称する。 公理（axiom） 定理（theorem） 仮説（hypothesis, 複数形 -ses） 仮定（assumption） 公理と定理はどちらも論理式またはシーケントで、表現形式上の差はなくて（Mizarでは公理と定理の区別はない）、定…
0次元 頂点（グラフの、複体の） ポイント、エンドポイント ノード コーナーポイント ストリンググラフでは、頂点、ポイント頂点、ノード頂点の区別がある。ポイント＝エンドポイントには、開エンドポイントと閉エンドポイントがある。エンドポイントは入り…
こうすればCoqに入門できそうだ （誰も書かないCoq入門以前 5） - 檜山正幸のキマイラ飼育記 : そして、説明に使う言葉がまた問題です。Coqの説明には、関数型言語、論理、型理論などの言葉が入り混じって登場します。型理論の用語や記号が無茶苦茶のグチャ…
A proposition is a well-typed term of type prop, a theorem is a proven proposition. theoremはproven propositionsとか言っているが、 thmデータをtheoremと言っていることが一番多い感じ。 ポールソンは、theoremはruleだ、と言っているし、 ウェンツ…
現状と対策、、、ほぼ地獄の様相 - 檜山正幸のキマイラ飼育記 メモ編の方針で、1エントリに1語ずつ説明していく。[用語法][多義語]タグを付けて、タイトルにも「多義語：」と入れる。 辞書的意味 Isar文書内で、theoremコマンドによるIsar文の後に続く部分 …
基本は、滅茶苦茶、恣意的、行き当たりばったり、気分次第、その場限り、思い付きで、イイカゲン、ルール無し、である。が、たまに区別を要求するからタチが悪い！多用されて多義性が強い（オーバーロードが激しい）用語は、その意味を列挙した辞書を作るし…
「これはひどい」としか言いようがない。[追記]研究対象→曖昧な用語法の研究 - 檜山正幸のキマイラ飼育記 メモ編[/追記]他の参考記事： 「ならば」記号の部分 - 檜山正幸のキマイラ飼育記 メモ編 論理の用語、日本語-英語 - 檜山正幸のキマイラ飼育記 メモ編…
名詞で言えば、implication, deduction, reasoning, inference, derivation, proof, entailement, verification, judgment 、それぞれに動詞がある。 テクニカルタームなのか説明の地の文としての言葉なのか? つまり、理論的／技術的な定義があるのか、それ…
何度も同じことを繰り返し書くが、そのときどきの現状報告 assertion あまり使われてない claim 構文範疇のclaimはある thesis - "?theis"というシェマ変数（schematic variable）はある。哲学用語だと「ヘーゲルの弁証法の正」、命題、テーゼだとか。複数形…
「ならば」記号があると、左右または上下がある。その部分は何と呼ぶのだろう。まったく確信がないが、 A⊃B で、Aが前件（antecedent）でBが後件（consequent）だったか？ 前件／後件は条件法（conditional; 条件表現、条件文）に対して使われる言葉だと思う…
⊃ implies |- provable（probableじゃない、注意） ⇒（シーケント） entailsかな |= valid, satisfies A |- B に対して、B is provable from A のようになる。|= A も A is valid。A |- B を A proves B と読むとおかしいのかな？ proveする主語はAじゃなく…
makeに関してしみじみ感じたのは、やはり適切な概念と用語法が欠如していることだ。そのために、正確な事を誰も記述できない状況になっている。 makeが作る（であろう）グラフを依存関係グラフと呼んでいいかあやしい。むしろ実行計画グラフだろう。 ターゲ…
カリー／ハワード対応は、まさにアナロジーの勝利。マーク・ホプキンスの観測もアナロジーだし、バエズ／ステイのロゼッタストーンにしろアナロジーだ。表のまとめ： 2015年10月、11月、12月ほんの少し - 檜山正幸のキマイラ飼育記 メモ編 の表の多くはアナ…
グラフ、特にツリーのリーフ（葉）といえば、末端の頂点のことだろうよ、普通。が、例のマニン（だけではないだろうが）の用語法では、グラフ全体のなかでエッジ（フラグのペア）になってないフラグのこと。ヒドイ！さすがに尻尾（テイル）とか脚（レッグ）…
