証明支援系がダメだった理由と、AIでブーストする理由 - 檜山正幸のキマイラ飼育記 (はてなBlog)
不満があっても、「言ってもどうせ何も変わりはしない」という諦めがあればあえて不満を口に出すことはないでしょう。願望があっても、「どうせ叶わぬ夢だし、言ったところで虚しくなるだけ」と断念しているなら語ることはないでしょう。 僕は今から不満と願望を書き記します。それは、諦め・断念していた事が、にわかに現実味を帯びてきたからです。不満と願望は、悪態と文句のように受け取られるかも知れませんが、僕の蓄積されたストレスの捌け口というわけではなくて（いや、多少は「蓄積されたストレスの捌け口」だけど）、前向きな予測〈希望的観測〉なんです。$`\require{color} \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} } \newcommand{\have}{\Keyword{have } } \newcommand{\need}{\Keyw
高次圏の下部構造を箙〈えびら〉で表現してみる - 檜山正幸のキマイラ飼育記 (はてなBlog)
Cが2次元の圏であって、対象、射、2-射（2-セル）を持っているとします。このとき、2-射を忘れて対象と射だけを考えることに何の問題もありません。Cを通常の（1次元の）圏とみなせます。 では、対象を忘れて射と2-射だけを考えたいときはどうでしょう。射の集合と2-射の集合を単純に取り出しただけでは圏にはなりません。次元が低い構成素を削り落とすには何らかの工夫が必要です。 そんな工夫のひとつとして、高次圏の台となる構造（下部構造）を、高次の箙〈えびら〉を使って表現してみます。高次の箙は、高次圏（higher category, n-category）を記述する便利な言葉を提供します。 内容： 反射的箙 反射的箙の別な定式化 半反射的箙と概反射的箙 高次圏と高次箙 共端対とホム箙 実例：小さい圏の圏 まとめと展望 反射的箙 箙（quiver）とは、「多重辺と自己ループ辺を許す有向グラフ」という長
王OKさんは実在するのか？ - 檜山正幸のキマイラ飼育記 (はてなBlog)
「別にどっちだっていいじゃないか」と言われれば、まー、そうなんですけど。 現時点では実在しそうだと思ってますが、最初見たのはこの動画： golden hour -JVKE (王OK cover) 2022/11/23 姿かたちが人工的。100%生成したものじゃないにしろ、例えば、モーションアクターと声優〈歌手〉と編集・加工のプロが作ったものじゃないだろうか、と思いました。王OK〈ワン・オーケー〉さんの最初の動画投稿は 2022/07/20 で、この時期からなら技術的には問題なく作れそうです。 以下の動画ではステージで歌っていて、実写っぽい。 The Next EP1 2023/07/31 The Next EP4 2023/08/20 それにしても、リアルっぽいフェイクとフェイクっぽい実在物の境界がほんとに曖昧になってしまったなぁ。「別にどっちだっていいじゃないか」が健全な態度なのでしょう
はじめての圏論 その第4歩：部分圏 - 檜山正幸のキマイラ飼育記
「第4歩」と書いたからと言って続くかどうかはわからない -- というセリフはもうやめよう。はじめの何歩かは進んだから、もう、いつ中断してもいいからな。 で、第4歩のネタなんですが、もっともっと実例を出すか、一般的な議論をするか悩みました（少しだけ）。結局、今までの例から新しい例を作り出してみることにしました。与えられた圏から新しい圏を作り出す手続きを（圏論的）構成（construction）というのですが、構成は非常に重要です。例えば、純関数の圏から状態機械の圏を作り出すCirc構成、モナドを使って射の概念を拡張するKleisli構成*1、よい性質の射の対を選び出すEP（埋め込み／射影）構成、2つの圏C, Dから関手圏DCの構成、非決定性（の一種）を導入するベキ構成、トレース付きモノイド圏からコンパクト閉圏を作るInt構成（GoI構成とも呼ぶ）などが、新しい圏を大量生産する製造機械として活
双対や随伴に強くなるためのトレーニング - 檜山正幸のキマイラ飼育記 (はてなBlog)
最初に言っておくと、これはマジな話です。ジョーダンやネタじゃないです。絵やテキストにおける、上下左右のひっくり返し／裏返しに慣れないと、双対や随伴の理解は困難です。いやっ、ホントに。 内容： 絵図とテキストにおける向き 平面における向きの変換 文字の変換 コーヒーでも飲みながら 絵図とテキストにおける向き 圏論的な絵算（pictorial/graphical/diagrammatic calculation）で使うストリング図を描くときの方向の取り方が人によりバラバラだという話を何度かしています。 絵算（ストリング図）における池袋駅問題の真相 絵算のススメ 2015 年末版 絵算の描画方向を示すために旗を使うことにした 射や自然変換の方向（第一の方向）とモノイド積や関手の方向（第二の方向）を、それぞれ上下左右のどの向きにとるか？ ということが問題なんです。第一方向、第二方向の順で矢印を使っ
はじめての圏論 第9歩：基本に戻って、圏論感覚を養うハナシとか - 檜山正幸のキマイラ飼育記 (はてなBlog)
まーた、気が変わった、コロリ（気が変わった音）。あっ、いや、米田の補題はやるつもりですよ、ええ。それはいいんですけどね、第8歩の冒頭で「新年の挨拶なんてのは省略。」と書いたのですが、なんか松の内も過ぎて「新年の挨拶」でもしたくなったよ。 まー、圏の定義とかやせた圏（thin category）の補足説明するついでに、圏論（そのコンピューティング・サイエンスへの適用）プロモーションの方針(?)でも述べるべ。 内容： 圏の直感的イメージを作る：孤立から連絡へ 論理とやせた圏 重い圏から軽い圏へ 圏もどきと構造付き圏 まとめ 全体目次 ●圏の直感的イメージを作る：孤立から連絡へ この「はじめての圏論」シリーズ、気まぐれで米田の補題に向かって舵を切ってしまったのですが、「はじめての」である点を忘れているわけではない（ホントか？）ので、基礎的概念と共に基礎的イメージ（感覚、気分）についても述べましょ
最近の型理論： 依存型理論で述語論理が出来てしまう理由 - 檜山正幸のキマイラ飼育記 (はてなBlog)
タイトルの件に関して、とりあえず概要だけ述べます。おおよそのストーリーを語るので、細部の抜けやギャップはあります。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\J}{\mathrm{J}} \newcommand{\In}{\text{ in }} \newcommand{\hyp}{ \text{－} } `$ 内容： はじめに 記法の約束 型圏化 相対的完備性 ファミリーのインデックス付き圏 射影と随伴トリプル系 おわりに シリーズ・ハブ記事： 最近の型理論： 宇宙と世界、そして銀河 はじめに 「階層化された宇宙達を備えた型理論」のヨーガ〈基本教義〉は、 型は宇宙の要素である です。が、「宇宙より銀河」（「最近の型理論： 型理論の構文論と意味論」参照）というキャッチ
n-圏とは何だろう - 檜山正幸のキマイラ飼育記 (はてなBlog)
The n-Category Cafeというグループブログがあります。僕はたまに覗いてみるのですがサッパリ分かりません。まれに分かる部分があるとうれしいので、やっぱりたまに覗きます。 さて、The n-Category Cafe のn-categoryって何でしょう？ nは任意の非負整数*1を表しているので、0-category, 1-category, 2-category, ... などを総称的にn-categoryと呼んでいます。higher dimensional category, higher category などとも呼ばれます。日本語だと、n-圏、高次元圏、高次圏などでしょうか*2。 一般的な定義は難しい（というか、現状、誰もわかってないようです）ので、2-圏の具体例をひとつ紹介して、n-圏の雰囲気をお伝えしましょう（それ以上の説明は僕には無理ですし）。この分野も用語法が混
高次圏： 用語法と文脈（主に2次元） - 檜山正幸のキマイラ飼育記 (はてなBlog)
高次圏論〈higher category theory〉に興味はあるし、必要性も感じているのですが、難しくてよく分からん、の状態が何年も続いています。 高次圏に関してちゃんとした事をちゃんと書くのは僕には荷が重いので、思い付きをダラダラ書くことにします。そういう記事のタイトルには「高次圏：」を接頭語に入れます。ダラダラ記事でも（少なくとも自分自身にとっては）無意味ではないと思います。錯綜した分野なので、道案内のヒントはそれなりに有意義かと。 内容： テキスト（教科書的資料） だらしなくザンネンな用語法 文脈により言葉の解釈が変わる 厳密n-圏 n-圏の意味 厳密、強、ラックス、反ラックス 2-関手と擬関手 自然変換の種類 まとめ シリーズ： 高次圏： 用語法と文脈（主に2次元） 高次圏： 複雑さの2つの方向と半厳密性 高次圏： 複雑さの3つ目の方向と相対階数 テキスト（教科書的資料） 2次
証明の“お膳立て”のやり方 - 檜山正幸のキマイラ飼育記 (はてなBlog)
N君が「こういうのは、どうやって証明したらいいのか… わかんないなー？」と困った顔をしてました。的確な処方箋を述べることは出来ないのですが、ヒントになりそうなことを記しておきます。 目的： 証明の“お膳立て”とは 例題 命題、証明可能性判断、証明要求 連言の分解 含意の変形 全称限量子を型宣言に お膳立てルールの繰り返し適用 同値な命題に置き換える お膳立てを完成させる シリーズ目次： 証明の“お膳立て”のやり方 証明の“お膳立て”のやり方 2： 証明の顧客・業者モデル 証明の“お膳立て”のやり方 3： さらに事例 証明の“お膳立て”のやり方 4： 随伴による集合差の定義 証明の“お膳立て”のやり方 5： 証明可能性判断と推論規則 証明の“お膳立て”のやり方 オマケ1： 集合の内包的記法の困惑 有限集合とは何だろう（ストーリー付き練習問題集） 有限集合とは何だろう への補足 距離空間と位相
証明検証系Mizarのジレンマと証明系の村 - 檜山正幸のキマイラ飼育記 (はてなBlog)
証明検証系Mizarを試した印象の続報です。 内容： 「これはひどい!」が、「これは素晴らしい!!」 Mizarコミュニティ Mizarの可能性 「これはひどい!」が、「これは素晴らしい!!」 Mizarの解説にあるサンプルコードはほぼ動きません*1。僕が試した範囲ではひとつも動きませんでした。理由は簡単で、構文的に完全じゃないからです。特に、構文上必須であるenviron部はたいてい欠如してます。 environ部とは、当該の証明記述ファイル（.mizファイル）が依存しているライブラリファイル（コンパイルされているが、.mizファイルと同等）を列挙する部分です。モジュールのインポート宣言と思えばいいです。 このインポート宣言を書くのが尋常じゃなく難しいのです。なぜなら： モジュールはグルーピングも階層化もされてなく、1257個がフラットに配置されている。 モジュール名は8文字までの英数字
フォワード・リーズニングとバックワード・リーズニング - 檜山正幸のキマイラ飼育記 (はてなBlog)
現状の証明支援系〈proof assistant〉について、僕はしょっちゅう愚痴と文句を言っています（twitterでぼやいたりしてる）。大きな不満点は、フォワード・リーズニングの対話的サポートがまったくない点です。不便だし面白くない。 内容： 証明ソフトウェアの進歩は遅い バックワード・リーズニング フォワード・リーズニング フォワード・リーズニングの対話的サポート 証明ソフトウェアの進歩は遅い 「プログラミング言語Lean 4の現状」に書いたように、証明ソフトウェアの開発は膨大な時間と手間がかかるもので、Coq, Isabelle, Mizar は30年から50年ほどの開発期間を経ています。新しいソフトウェアであるLeanでも、もう10年になります。どの開発チームも最優秀の人材を揃えています。それでも「使いものにならない」事実が、証明ソフトウェアの開発が極めて困難であることを物語ってい
含意記号に対する誤解 -- それは間違いだ - 檜山正幸のキマイラ飼育記 (はてなBlog)
年に2,3回、誰かに向かって同じ話をしている気がするので、ブログ記事にしておきます。$` \newcommand{\Imp}{\Rightarrow } \newcommand{\Iff}{\Leftrightarrow } \newcommand{\mrm}[1]{\mathrm{#1}} \require{color} \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\For}{\Keyword{For } }% \newcommand{\Define}{\Keyword{Define } }% `$ 論理記号のなかで、$`\land`$（論理AND、連言）、$`\lor`$（論理OR、選言）、$`\lnot`$（論理NOT、否定）を誤解する人はあまりいない*1のですが、$`\Imp`$（含意）
群の作用の左と右 - 檜山正幸のキマイラ飼育記 (はてなBlog)
群が「左から作用する」「右から作用する」という言い方があります。このときの「左」「右」はどんな意味なんでしょう？ また、「左」か「右」かはどうやって判断するのでしょう？ なにかを左（あるいは右）と呼ぶべき必然的根拠があるとは思えないので「約束によって左右を決める」のでしょうが、その約束はどのように決めるのでしょうか？ 約束を変えると、どのような影響があるのでしょう？ 以下、左右の問題を考えてみます。$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\On}{\:\text{ on } } % 使う \newcommand{\id}{\mathrm{id} } \newcommand{\hyp}{\text{-} } \newcommand{\GL}{\mathrm{GL}} \newcommand{\Lin}{\mathrm{Lin}} \n
掛け算の順序問題： 檜山の地雷を踏まないで - 檜山正幸のキマイラ飼育記 (はてなBlog)
「掛け算の順序問題： 左右の意味あいが違う事例はあるけど…」： 掛け算順序区別論に反論する気もないです。理由は、めんどくさいからです。鬱陶しいからです。 反論しない主たる理由が「めんどくさい／鬱陶しい」からなのはホントです。 で、「それはそうだけど」の事例を幾つか出します。「もう、それは分かっているからさー」と言いたいから確認するだけです。そこから先の本論はしないけどね。 「そこから先の本論」はしたくないのです（したくなかったのです）。 実は、したくない理由がもうひとつありまして； そこから先の本論に入ると、僕は感情的になり強い言葉を吐くであろうことが予測できるからです。 僕は、根性主義や体罰を極度に嫌っているのですよ。2006年3月以前の、「アンチ根性主義」に関連する記事は、次のリンク集からたどれます。 アンチ根性 ミニリンク集 そこから2016年までの間の記事は、次の記事内にリンクがあ
衝撃的なデータベース理論・関手的データモデル 入門 - 檜山正幸のキマイラ飼育記 (はてなBlog)
デイヴィッド・スピヴァックによる衝撃的なデータベース理論である関手的データモデル。どうしたらうまく説明できるか？ と色々と悩んでしまいますが、まー、書けるところから書き始めてしまいましょう。 さー、いらっしゃい、いらっしゃい。関手的データモデルの世界へようこそ。圏論の言葉は出てきますが、圏論の予備知識はほぼゼロでOKですよ。 [追記 date="翌日"]取り急ぎ勢いで書きましたので、不注意と早とちりが混じっていました。追記と取り消し線の形で訂正と注記を足しました。字句レベルの表現の変更は直接編集しています。 あとそれと、圏論の基本用語を知りたいときはコチラ、… って、……、ゴメン！[/追記] 内容： はじめに 本の購入のサンプル スキーマのグラフ表現 キーとか計算カラムとか 圏としてのスキーマ 関手としてのデータベース状態 テーブルの変化 自然変換としてのデータ操作 データベースに圏論が使
「コミュニケーションの多次元化」という革命に立ち会っているのだと思う - 檜山正幸のキマイラ飼育記 (はてなBlog)
先週の記事でGlobularを紹介しました。日本語を食わせるとお腹を壊して死んだりします。でも、けっこう使えるし十分に面白い。 僕がなぜ絵算やGlobularに興味を持つのか、と言うと； これが計算や証明、そしてコミュニケーションに革命を起こすものだと感じるからです。革命とはいってもゆるやかに進行し、30年、50年あるいは100年たったら随分と様変わりしたね、という感じでしょうが。 多次元の言語 文字はもともとは絵で、今でも四角形に収まる図形です。構成要素である基本図形を組み合わせて何かを表現するという点においては、テキストもストリング図（下に例）も変わりはありません。違うのは、ストリング図（や3次元内の曲面を使うサーフェイス図）が、本質的に2次元以上の空間を必要とすることです。 [*1] [*2] [*3] テキストだって2次元に配置されますが、あれは折り返しているだけ*4。音声読み上げ
Isabelleについて： 証明支援系は何を目指し、どこへ向かうのか - 檜山正幸のキマイラ飼育記 (はてなBlog)
昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelleシステムを紹介しましょう。客観的な紹介ではなくて、僕の雑駁な印象記です。 内容： Isabelleの独自な世界 Isabelleの未来 Isabelleの独自な世界 「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」より： PIDE構想は、Isabelleプロジェクト／コミュニティを世の趨勢とは離れた孤立化へと導くのか、それとも、時代がPIDEの先進性にいずれ追いつき、PIDEがスタンダードな証明支援系UIとなるのか？ なかなかに興味深いですな。 Isabelleが世の趨勢と離れるのか？
誰も書かないCoq入門以前の話 - 檜山正幸のキマイラ飼育記 (はてなBlog)
「WindowsへのCoqのインストール」： 事情があって、AgdaかCoqを触ってみようか、と。 事情というのは、個々の命題の証明（確認）は割と簡単そうだが、命題がイッパイあるのでウンザリな状況のことです。家計簿の計算が筆算だと面倒だから電卓を使いたい、という状況と同様です。 それでCoqのインストールは済んだのですが、処理系の使い方が分からない。個々の操作は覚えていけばいいのでしょうが、そもそもCoq処理系が何をするものなのか？ が理解できないのです。Web上にCoqの解説は幾つもあるのですが、「いやいや、そうじゃなくて、それ以前のことがサッパリわからんのですけど」という感じ。スタートラインに立てない。 それで、「Coqの解説」じゃなくて「Coqの仕様」を読んだほうがいいのかも、と https://coq.inria.fr/distrib/current/refman/ （リファレンス
プログラムの実行時間を計る事と半環の代数 - 檜山正幸のキマイラ飼育記 (はてなBlog)
「零の概念とmax-plus半環の紹介」において： max-plus半環やmin-plus半環の計算技術は、トロピカル代数（tropical algebra、より一般にはエキゾチック代数）と呼ばれたりします。[...snip...] 例えば、プログラム意味論に計量的な要素を入れるとき、トロピカル代数が使えそうです。 実際にトロピカル代数を使ってプログラムの実行時間を計って*1みます。 「零の概念とmax-plus半環の紹介」で導入した概念は断りなしに使います。内容はまだ生煮えなところがあります。 内容： プログラムのモノイドとプログラムの半環 プログラムの実行時間 実行時間の計測値となる半環 もっと精密に実行時間を記録するには まだ精密さが足りないと思うなら プログラムのモノイドとプログラムの半環 p, q などはプログラムを表すとします。プログラムの全体をMとします。当然に、その「プログ
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
