同意語・多義語の解釈、悪戦苦闘記
何度も同じことを繰り返し書くが、そのときどきの現状報告
- assertion あまり使われてない
- claim 構文範疇のclaimはある
- thesis - "?theis"というシェマ変数（schematic variable）はある。哲学用語だと「ヘーゲルの弁証法の正」、命題、テーゼだとか。複数形はtheses。学位論文の意味でも使うよね。
- statement 構文範疇にstmtとstatementがある。よくわからじ。
- proposition あまりにも意味がイッパイ有り過ぎて、、、
- theorem あまりにも意味がイッパイ有り過ぎて、、、
Isabelleの中核部について、
- ポールソンのM foundation論文で定義されていてはっきりしている。
- Isabelle/Pure ソフトウェアシステムのサブシステムとしてだいたい分かる。
- Primitive Logic - implementation文書の第2章のタイトル
- framewrok logic, logical framework (LF) ポールソンによると、LFとmeta-logicは同義だそうだ。framewor logicとmeta-logicも同義だろう。
- logical core, core logic - implementation文書 2章に出てくる。primitive logicと同義かどうか分からない。が、型推論と型略称展開機能がない、とは書いてある。
- the Pure logic ポールソンのMのことだと思われる。
implementation文書 2章で、
- the sort order 「整列の順序」としか思えないが、ソート全体が持つ順序構造のこと。
- arity 型構築子のソートに関するプロファイルのこと。
- the universal sort これはまーいい。
- type inference layer - core logicの外だそうだ。
- logical category なんと構文範疇のこと。sytactic category。syntactic typeよりはマシか。
- type scheme 型構成子の型パラメータに、具体的型を入れた形か？ 一般的には、型変数を含む型表現を型スキームと呼ぶが、、、？
- type expression 型表現、これは僕の用語法と同じようだ。型項ともいうね。
- type constructorも単にtypeと呼んでいる。
- type arityのtypeは型構成子＝型関数で、arityはプロファイルのこと。
- type abbreviation Haskellのtype synonymと同じ？ TypeScriptならtype alias
- sort constraint, type constraint、これはTypeScriptのtype annotation（型注釈）と同じか？ インライン型宣言、インラインソート宣言がいいような気もするが。
implementation文書 2章を読んで、
