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

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

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

[参照用 記事]

2022-01-01から1年間の記事一覧

プログラミング言語Lean 4の現状

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

パイプライン指向JSON処理プログラミング言語 jq

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

JavaScriptモジュールは二回ロードされる可能性がある

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

二重圏の語法・記法、ローカルルール事例

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

二重圏を語るために

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

コンテキスト、判断、指標、シーケントなどのゴチャゴチャを整理

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

型クラス述語とイプシロン型

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

全称型/存在型: 代替案

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

全称型/存在型: まとめと Models-as-Types

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

全称型/存在型 補遺

「アハハハハ(ちからない笑い): 全称型/存在型」で触れた 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, …

Int構成〈GoI構成〉 再論

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

テレオロジー圏の記述

「テレオロジー圏の公理の自然な解釈」にて: [テレオロジー圏に関する] このような事実を、スッキリと短く書く記述方法はないものでしょうか? ロマン〈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」で述べます。 しかし、不動点の話はフリーモナドとは独立に語れるので、「フリーモナド」の続きでは…

Functor型クラスの型インスタンスは関手なのか?

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

フリーモナド 1: 自由で無料な木

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