無料で入手できる本格的（紙なら高額）な理数系専門書15選 - 檜山正幸のキマイラ飼育記に追加みたいなもの。The Convenient Setting of Global Analysis (Mathematical Surveys & Monographs)作者: Andreas Kriegl,Peter W. Michor出版社/メーカー: Amer Mat…

伝統的な微分的構造 題名に「微分幾何」と付いている教科書で扱う分野伝統的微分幾何のスタイル 標準的伝統的 代数幾何風のスキームを使う SDG、その他トポスベース 基本部分の後で各論を扱う 計量構造（リーマン多様体、ローレンツ多様体） シンプレクティ…

ゾゾウスキ導分（Brzozowski derivative） クレイジー計算 リソースに敏感 可逆計算 積分 ラムダ計算 接関手 チェーンルール ベックの法則 自己分配法則 超準解析 SDG、なめらかなトポス 導来微分幾何

無料で入手できる本格的（紙なら高額）な理数系専門書15選 - 檜山正幸のキマイラ飼育記に追加みたいなもの。Synthetic Differential Geometry (London Mathematical Society Lecture Note Series)作者: Anders Kock出版社/メーカー: Cambridge University Pr…

僕が定義する多圏は、三部結合（tripartite composition）を持つ多圏だ。多射は、三部スパイダー（tripartite spider）。

本編に書いた→ 教養としてのC言語プログラミング入門は成立するのか - 檜山正幸のキマイラ飼育記一昨日と昨日（土日）、「教養としてのC言語によるプログラミングのお勉強」つう感じのものに付き合う機会があったのだけど、トピックや課題の選び方はなかなか…

本編に書いた→ 教養としてのC言語プログラミング入門は成立するのか - 檜山正幸のキマイラ飼育記僕は最初から「scanfは使うべきではない」と教わったので、scanfの存在は知っているが使ったことはない。正体がハッキリした文字列にsscanf()を使うことはある…

数量の感覚 - 檜山正幸のキマイラ飼育記 メモ編 長さ（道のり）、比、面積と体積などに関して、あまり感覚を持ってない人はいる。 ... 数量や空間に対する基本的な感覚の欠如は意外と（本人も周りも）気付かないみたいだ。 数量感覚の欠如はそれほど珍しくな…

たくさん、少し、少ない （個数） 長い、短い （長さ） 大きい、小さい （体積、面積などの測度） 広い、狭い （体積、面積） 重い、軽い （重量、比重、密度） 速い、遅い （速度） 濃い、薄い （濃度） 甘い、無味 （砂糖の濃度） 高い、安い （価格） 長…

isar-ref "2.2.1 Context elements"

モノイド圏の一貫性は難しい。定理の記述も色々ある。http://ocw.mit.edu/courses/mathematics/18-769-topics-in-lie-theory-tensor-categories-spring-2009/lecture-notes/MIT18_769S09_lec03.pdf にある次の形が使いやすいように思う。 Let X1, ..., Xn ∈ …

7月17日の日本テレビ「ザ！鉄腕！DASH！！」の「0円食堂」にて、東京ドーム31個分の畑。この畑から、1000トンの大根を生産。 アール=a=100m^2 ヘクタール=ha=100a=100*100m^2=一辺100mの正方形の面積 ドーム=4.7ha

どんな経験を仮定してるんだろう。 積み木、レゴ、ラキュー、オハジキなどを手でいじった経験 特に、同じ形のモノを直線状に並べたり、さまざまな形に並べ替えたりした経験 砂で山を作ったり、穴を掘った経験 部屋のなかに散在したおもちゃを片付けた経験、…

Prologで関手（圏論とは無関係！）とか関数子と言っているものと同じデータ構造を持つようだ。 基本、関数型言語らしいが、Prologフレーバーな構文。 パターン表現があって、引数渡しはパターンマッチング。これには異質な構文を使う、はじめて見た構文。 リ…

生成規則 generation： 前提（既存証明オブジェクト）がないところから証明オブジェクトを1個作る 変形規則 deformation： 1つの前提から証明オブジェクトを1個作る 組み合わせ規則 combination： 複数の前提から証明オブジェクトを1個作る また、リーズニン…

どうにもならないなーー(溜め息)「除去規則の適用」のレゾリューションアルゴリズムの圏的意味論を考えてみたが、これは複雑。なのに、Isabelleのなかでは天下り。これでは納得出来るわけがない！それはそうと、ポールソンは、メインゴールとサブゴールズと…

自然演繹の正規形定理は、直和を持つデカルト閉圏の等式的な公理系から出てしまう。つまり、直和を持つデカルト閉圏を計算するシステムのなかに自然演繹は埋め込めて、正規形定理は埋め込み先では自明になってしまう。自明になってしまうのだけど、そこまで…

離散数学 講義 資料 (1) から (11) http://ocw.nagoya-u.jp/files/16/eng_c02_01.pdf (1) 面白い問題が幾つかある http://ocw.nagoya-u.jp/files/16/eng_c02_03.pdf (2) よくある基本的なこと http://ocw.nagoya-u.jp/files/16/eng_c02_05.pdf (3) 高校の順…

CoqでもIsabelleでも同じ。Coqの証明ゲームの表側と裏側 （誰も書かないCoq入門以前 4） - 檜山正幸のキマイラ飼育記 : Coqシステムは、そして自分は、いったい何をやっているんだ？ これが証明って、いったい何でだ？ こういう疑問を払拭できないのは、Coq…

Isabelleの用語法の無茶苦茶さや、概念の混乱、理解のためのミッシングリンク、これらの大きな部分は「次元概念の欠如」によるのではないだろうか？ -- まず間違いない。 参考：シーケント計算、ムービー、高次圏 - 檜山正幸のキマイラ飼育記 メモ編 参考：…

オカシイ、オカシイ。除去規則（elim rule）がIsar satement formatだとobtainsで書かれる。これはオカシくはない、つうかまっとうなんだが、逆に通常の除去規則の書き方はいったいなんなんだ？ ということになる。disjEの例だと： ?P ∨ ?Q ==> (?P ==> ?R) …

ウッヒャーー、またしても新用法を発見。subgoalがsolveすべき対象である命題（＝論理式＝ルール＝定理）で、goalはそれらsubgoal達の集合の意味で使っている。つまり、ゴール＝サブゴールズ。しかし、サブゴールの結論をゴールと呼ぶことがあるから。「ゴー…

メニューツリーのパス: [Plugins]-[Plugin Options] タブ: [Plugin Options] ツリーコントロールのパス: /Isabelle/General レコードのフィールド名: Auto Quickcheck UIの種類を無視してパスで示すと Plugins/Plugin Options/Plugin Options/Isabelle/Gener…

「なるほど」とは思うが、なんか、これしか方法がないのかよ？ とも感じる。 Isabelleではgoal文はないので、lemma "命題" と書いて、この行の表示（カーソルあわせてOutputを見る）で、ゴールを見せる。 タクティクの説明は、apply(タクティク) oops とする…

ストリング図とストリンググラフの関係を使い、グラフ理論的な操作として証明行為＝リーズニングを理解する。キーワード（大事な言葉）の定義： 推論ノード：通常の推論規則を表す。複数（0個もあり）の入力（仮定）と1つの出力（結論）を持つ。 ワイヤー：…