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

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

歴史的なシガラミ、因縁、因習

Isabelle 用語法

進化なのか、退行なのか？ - 檜山正幸のキマイラ飼育記 メモ編に出した

サラ・ケベレ(?)女史の1994年チュートリアル。

これに書いてあること、読んでわかること。

  1. Isabelleを a framework for developping proof systems と捉えている。今もそうだけど。
  2. proofのobjectとactivityを区別するような記述がある。結局、proofという語の使い回しだが。
  3. core file, image file, heap file は類義語
  4. core file にコンパイルすることと、エクスポートすることは同じ
  5. object-level "sentences" are entered as ML strings.
  6. 複数行のMLストリングは、行末の\で継続していたらしい。
  7. オブジェクト論理の限量子は、!（∀）と?（∃）
  8. 定理と公理は区別してない。つうか、公理⊆定理 という解釈。
  9. Theorems are objects in Isabelle
  10. Theorems are entered as axioms
  11. or (theorems are) produces by proof
  12. 定理は、公理としてenterされるか、証明（というactivity）により生成される。分かりやすい。
  13. theoremはpostulateされて、acceptされる。ここのpostulateは提示の意味だろう。propose, claim, state（動詞）と同義だろう。
  14. axiomsはassertされる、とも言っている。
  15. シェマ変数を meta-level variable と言ってるが、これはマズイ。Pureの変数には、普通の自由変数があり、これもメタレベル変数になるし。高階対象を表す変数もメタレベル変数と呼ぶことがある。
  16. 4.1節に、In Isabelle, inference rules are theorems that contain premises and a conclusion. とハッキリ書いてある。
  17. よって、ルール⊆定理
  18. この当時から、論理式と命題と定理は区別せず、公理は定理であり、ルールも定理である、と言っていた。
  19. theoremコマンドがなくて、Goalコマンドだったので混乱は少なかったのだろう。
  20. meta-levelをML言語のレベルの意味でも使っている。
  21. つまり、メタレベルの意味が、(1)Pureレベル (2)MLレベル (3)個体領域より高階のレベル (4)ほんとのメタ くらいでオーバーロードされている。
  22. problemがテクニカルタームっぽい。「theorem : goal ＝ theory : problem」という感じか？
  23. theoryは set of theorems ではなくて、タクティクや構文定義も含む。
  24. proof environmentという言葉を使っている。proof state, proof contextと同義だろうが、トップレベルのセオリーコンテキストも意味してるかも知れない。
  25. assert, claim, proposeとほぼ同義でstate（動詞）を使っている。
  26. セオリーをML REPLで表示すると、constsとrulesに分けて表示する。constsがシグニチャ、rulesが公理。この表示で既に、公理＝定理＝ルール となっている。
  27. シグニチャを構成するconstantはdeclareするものらしい。axiomはenter/assertして、theoremはproofし、goalはsolveする。
  28. arityという独特な分かりにくい言葉（後述）は、1990年代からあった。
  29. 定理は、MLの束縛のなかに埋もれていた。定理名はMLの変数名であり、thm型のデータが束縛されている。よって、MLインタプリタの環境が、セオリーコンテキストでもあった。まー、分かりやすい。
  30. 個々のセオリーはMLストラクチャで、それらのストラクチャは、セオリーというMLシグニチャを持つ。

驚いたのは、1984の時点で型クラスがあったこと。今のとは違うかもしれないが、型の型は存在していて、型／型構成子の導入と一緒に、その型／型構成子のプロファイルとして型クラス（のようなもの）を宣言する。

型システムの上位の「型の型システム」（今のソートシステム）はあった。で、型／型構成子のプロファイルをarityと呼んでいた。arityやrankをプロファイルの意味で使うことはあるにはある。多義的なプロファイルを許すという意味でarityはpolymorphicなのだが、多相性の表現にパラメータを使うのではない。列挙的な多相と言えばいいのかな？

関数で言うと、id:'a -> 'a は、'aを型パラメータとする多相だが、id:(int -> int OR string -> string) のような有限個のプロファイルを実際に並べたのが列挙的多相。

関数ではなくて型関数＝型構成子のプロファイルを、型クラスの列挙的な多相で書く。それがarities宣言。