証明支援系Lean〈リーン〉は、かなり前（2017年くらい）から注目しているソフトウェアです。注目はしているんですが、ちゃんと調べる機会がなかったので、このブログで触れたことはありませんでした。2022年のうちに紹介したい（今は大晦日の夜）。Leanは現…

jq（https://stedolan.github.io/jq/）の紹介では、「JSON処理のワンライナー〈一行野郎〉としてめちゃくちゃ便利！」とアピールするのが定番です。もちろんそれは本当で、「めちゃくちゃ便利！」です。が、実は jq は、ワンライナー記述にとどまらない、か…

ECMAScript Modules（ESM）方式のモジュールシステムを前提に、ブラウザ向けJavaScriptプログラムを書いていたら奇妙な現象に遭遇しました。同一のJavaScriptモジュールが、ブラウザ内に二回ロードされていたのが原因でした。内容： クラスの定義とクラスの…

「二重圏を語るために」にて： 広く合意された約束はないので、二重圏を語るときは、ローカルルールをしっかり決めましょう。そうでないと、話がワヤクチャになります。 ローカルルールの事例を述べておきます。$`\newcommand{\twoto}{\Rightarrow} \newcomm…

二重圏を話題としたコミュニケーションは、なかなかに大変です。前もって約束を決めておかないと、話がワヤクチャになります。この記事でガイドラインを示します。$`\newcommand{\cat}[1]{ \mathcal{#1}} \newcommand{\mrm}[1]{ \mathrm{#1}} \newcommand{\I…

圏論、型理論（型付きラムダ計算含む）、論理は、カリー／ハワード／ランベック対応により、同種の構造（例えばデカルト閉圏）を扱っていると理解することが出来ます。しかし、用語法・記法はバラバラです。このバラバラさゆえに、対応関係を捉えられなかっ…

全称型／存在型のことを調べていて（「全称型？ 存在型？ ‥‥？？」参照）、気になったことがありました。some（論理記号 ∃）と any（論理記号 ∀）がほぼ同じ意味で使われていたり、用法が逆転していたりが起きていて、これは何でだろう？ と疑問を感じました…

昨日「まとめ」もしたので、この話題も一段落ですが、僕が言いたいことは； 「全称／存在」という言葉、「∀／∃」という記号を、型理論のなかで使うのはやめたほうがいいよ、ってことです。何も得することがなくて、弊害があります。「全称／存在」「∀／∃」を…

昨日・今日と、「全称型／存在型で困惑した」という話を書きました。 全称型？ 存在型？ ‥‥？？ アハハハハ（ちからない笑い）： 全称型／存在型 全称型／存在型 補遺 なんとなく情勢は見えてきたので、いったんまとめをしておきます。それと、存在型の一部…

「アハハハハ（ちからない笑い）： 全称型／存在型」で触れた Swift の existential any だけど； some というキーワードは既に使われていて、any にするしかなかった、という事情みたいです。Swift では、キーワードを付ける付けないに関わらず、プロトコル…

「全称型？ 存在型？ ‥‥？？」を書き終わった後で見つけた、Swift の存在型に関する記事、： Existential any in Swift explained with code examples Existential any allows you to define existential types in Swift by prefixing a type with the any k…

「多相関数を表す全称記号がしゃくに障るワケ」において、多相関数や依存型を表すときに使う全称記号を話題にしました。僕は全称記号反対派ですが、実際には全称記号が使われています。さてところで、「全称限量された型〈universally-quantified type〉」、…

「グリッド計算とコーナリング、そして二重圏」において、二重圏の2-射を描くペースティング図とストリング図を紹介しました。ストリング図では、縦方向ワイヤーは上から下、横方向ワイヤーは左から右で、常識的な書字方向に一致していて「あー、気持ちいい…

過去記事「フリーモナド 1： 自由で無料な木」において、フリーモナドの説明をしました。その過去記事の冒頭は次のようでした： 説明には、多くの場合、HaskellコードまたはHaskell風擬似コードが使われています。プログラミング言語としてのHaskellの利便性…

テレオロジー圏、コンパクト閉圏、トレース付きモノイド圏などのあいだの親族的関連性を調べたい、という動機から資料を探しているうちに、二重圏を使う手法に出会いました。そのことを前の記事に書きました。 グリッド計算とコーナリング、そして二重圏 モ…

ここ最近、テレオロジー圏、コンパクト閉圏、トレース付きモノイド圏などのあいだの親族的関連性に興味を持っています。なんか資料がないかな、と探していたら次の論文を見つけました。 Title: Cornering Optics Authors: Guillaume Boisseau, Chad Nester, …

「両側テレオロジー圏とプレオートマトン」にて： 両側テレオロジー圏は自己双対コンパクト閉圏とよく似た構造になります。テレオロジー圏とコンパクト閉圏には、親族的関連性があるのでしょう。 テレオロジー圏、コンパクト閉圏、トレース付きモノイド圏の…

「テレオロジー圏の公理の自然な解釈」にて： [テレオロジー圏に関する] このような事実を、スッキリと短く書く記述方法はないものでしょうか？ ロマン〈Mario Roman〉のストリング図は確かに便利ですが、大規模高次な代数系を直接的に表現する記法・描画法…

今日は三連休の真ん中の日なのか。そんな日に僕は、理屈っぽいけど感情的な記事を投稿します。多相型／多相関数の表現に使われる全称記号を僕はずっと嫌っています。その理由を説明します。理屈っぽい話に興味がないなら、最後の節だけで「しゃくに障るワケ…

昨日の記事「テレオロジー圏の公理の自然な解釈」にて： [テレオロジー圏に関する] このような事実を、スッキリと短く書く記述方法はないものでしょうか？ ロマン〈Mario Roman〉のストリング図は確かに便利ですが、大規模高次な代数系を直接的に表現する記…

昨日、テレオロジー圏を拡張する話をしました。拡張した“両側テレオロジー圏”という概念に、どの程度の意義があるかハッキリとはわからないのですが、もとにしたテレオロジー圏という概念は、けっこう安定したものだろうと思います。そう思う理由は、テレオ…

状態遷移系やオートマトンをレンズで記述しようとすると、どうも“痒い”ところがあります。テレオロジー圏に、双対的な同語反復射を追加した圏を構成すると、状態遷移系／オートマトンの記述には都合が良さそうです。思い付いただけで、あまり確認・吟味はし…

応用圏論〈ACT -- Applied Category Theory〉で頻繁に使用されるワイヤリング図は、ケリー／マックレーン・グラフとして表現できます。ケリー／マックレーン・グラフを経由すれば、ワイヤリングの関数による表現も自然に感じるでしょう。この記事は、以下の2…

ここ何回か不動点の話を書きました。 不動点方程式／不動点不等式と不動点オペレーター (2022-09-22) タルスキーの最小プレ不動点定理（訂正） (2022-09-23) 証明のツリー構造も描いてみる (2022-09-23) タルスキーの定理の実例と応用 (2022-09-24) 解析学や…

ここでのタルスキーの定理は、不動点に関するタルスキーの定理です。不動点関連でも次のような「タルスキーの定理」があります。 最小プレ不動点と最小不動点の関係を述べた定理 最小不動点の存在定理 不動点集合の性質に関する定理 「最小プレ不動点ならば…

「タルスキーの最小プレ不動点定理（訂正）」において： 証明の流れを完全に追えるように、中間の命題にいちいち名前（ブラケットで囲った文言）を付けて参照することにします。 と、やってはみたのですが、“証明の流れ”がテキストで直列に（シリアライズさ…

「不動点方程式／不動点不等式と不動点オペレーター」において、タルスキーの最小プレ不動点定理を出しましたが、記述が間違っていたので訂正し、省いていた証明を記します。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\cat}[1]{\mathcal{#1}} \newco…

「フリーモナド 1： 自由で無料な木」において、次のように予告しました。 圏論的な不動点方程式と、不動点方程式によるフリーモナドの構成については「2」で述べます。 しかし、不動点の話はフリーモナドとは独立に語れるので、「フリーモナド」の続きでは…

ひとつ前の記事「フリーモナド 1： 自由で無料な木」において次のように書きました（ブラケット内は要約です）。 [圏論的に考えた場合と、型クラスで考えた場合とでは] メンタルモデルがだいぶ違います。この食い違いがコミュニケーションの障害になることが…

フリーモナドの「フリー」は、「自由」の意味と共に「ただ〈for free〉」の意味もあります。「ただで手に入るモナド」ということです。しかし、この「ただで」は、「課金したらガチャをただで引けるよ」の「ただで」と同じで、事前のコストはかかっています…