このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

2017-09-01から1ヶ月間の記事一覧

おススメのネコ動画

ネコパンチの動画は色々ありますが、↓これはホントに凄い。ガチのボクシング・ファンです。傑出した身体能力を持つネコちゃん↓のジャンプ。カメラワークと編集も素晴らしい。カッコイイ!なんか笑っちゃう↓。ズンズン歩いてくるところが面白い。[追記]動画の…

証明の“お膳立て”のやり方 2: 証明の顧客・業者モデル

昨日の記事「証明の“お膳立て”のやり方」の続きを書きます。発展編と言えるかも知れません。昨日“お膳立て”という言葉を使った理由は、形式的論理体系の話ではなく、コンピュータによる証明の話でもなく、人間が例えば「f:A→B は全射 ⇔ f*:Pow(B)→Pow(A) は…

証明の“お膳立て”のやり方

N君が「こういうのは、どうやって証明したらいいのか… わかんないなー?」と困った顔をしてました。的確な処方箋を述べることは出来ないのですが、ヒントになりそうなことを記しておきます。目的: 証明の“お膳立て”とは 例題 命題、証明可能性判断、証明要…

マイクロコスモ原理の恐怖

怖い話。内容: スノーグローブ現象 マイクロコスモ原理 僕が出会った例:モノイド圏 どうやって無限後退を避けるか マイクロコスモ原理とスノーグローブ現象 過去記事 スノーグローブ現象スノーグローブ現象(snowglobe phenomenon)とは、世界(あるいは環…

困った時の米田頼み、ご利益ツールズ

米田埋め込みはやっぱり役に立ちますね。米田埋め込みを利用するときに便利なツールを幾つか紹介します。それらのツール達は: 関手に使うラムダ記法 米田の星 (-)米, (-)米 関手・自然変換のテンソル積 マルチ米田埋め込みのドット記法 内容: 過去の事例:…

辻褄が合わなくて困ってしまう用語法:圏・グラフ・射の変種達

オペラッド(operad)は圏の変種ですが、最近はよく使われます。複圏(multicategory)はオペラッドの同義語だと思っていいでしょう。単一対象(single object)の複圏だけをオペラッドと呼び、色付きオペラッド(colored/coloured operad)を複圏と同義語だ…

Globularの使い方 (3): 定理と証明

Globularにおける定理と証明とは何でしょうか? 実は、この問には明確な答はありません。強いて言えば、あなたが定理だと感じたものは定理だろうし、あなたが証明だと思いたいものは証明でしょう。曖昧過ぎますか? -- しかしでは、Globularの外の世界で定理…

量子力学←→熱力学 : 沙川さん達の大発見?

東京大学工学部からのプレスリリース: http://www.t.u-tokyo.ac.jp/foe/press/setnws_201709061614152431248138.html 2017.09.06量子力学から熱力学第二法則を導出することに成功 〜「時間の矢」の起源の解明へ大きな一歩〜:物理工学専攻 伊與田英輝助教、…

Globularの使い方 (2): サンプル・ワークスペース

簡単な例題のワークスペースを公開しました。 http://globular.science/1709.001 内容: 扱っているトピック 注意事項 指標(セル一覧) ワークスペースを作る手順 第1回とシリーズ目次 扱っているトピックワークスペースの内容は、「記法バイアスと記法独立…

Globularの使い方 (1)

証明支援系Globularを使っている人っているのかな? まー、いても少数でしょうね。僕はたまに使います。しばらく使わないでいると使い方を忘れます。少なくとも一人のユーザー(=僕・檜山)にとっては意味があるので、「Globularの使い方」を記録しておきま…