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

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

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

参照用 記事

雑記/備忘

余ベキ関手とポイントセット関手の随伴

随伴系〈adjunction〉の典型的例というと、やはり自由忘却随伴系〈free-forgetful adjunction〉でしょうかね。あと、カリー化・反カリー化も典型的だと言えるでしょう。集合圏で考えるとして、カリー化・反カリー化による次のホムセット同型があります。$`\n…

球体集合とペースティング図/指標

ひとつ前の記事「球体集合と組み合わせ幾何」で、球体集合の圏についておおよそは説明しました。この記事では、次元が低い球体集合達の圏について述べます。球体集合の絵図表示であるペースティング図とテキスト表示である指標についても補足します。低次元…

球体集合と組み合わせ幾何

最近の2回、バタニン・ツリーの記事を書きました。 バタニン・ツリー 再論 バタニン・ツリーの参考資料/参考文献 これは、今年の5月頃の話題の蒸し返しです。 指標の組織化と表現方法と呼び名は色々だ 指標の話: ペースティング図とバタニン・ツリー 球体…

バタニン・ツリーの参考資料/参考文献

過去記事「バタニン・ツリー 再論」の最初の節にバタニン・ツリーの参考文献を載せました。内容的重複がありますが、この記事でも参考資料/参考文献を紹介します。過去記事より細かいコメントを付けます。が、いずれの論文も拾い読みしかしてないので、拾い…

バタニン・ツリー 再論

バタニン・ツリーについては、以下の過去記事に書いています。 指標の話: ペースティング図とバタニン・ツリー ディーン達の論文の p.6 "2 Batanin trees" でもバタニン・ツリーを扱っています。 [DFMRV22-24] Title: Computads for weak ω-categories as a…

イコール/等式の話: 集合論、古典述語論理、圏論

$`x = y`$ と書かれていたら、「その意味は明らかだ」と多くの人は思うでしょう。が、イコール/等式の意味や用法はそんなに簡単でもないですよ。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\mbf}[1]{\mathbf{#1}} %\newcommand{\mfk}[1]{\mathfrak…

圏論で使う「図式」と「形状」

「図式」「形状」という言葉は普通に使う日常語なので、テクニカルタームとして使うのはかえって難しいですね。が、使うことはけっこうあるので、ある程度は運用法を決めておきます。特にフォーカスするのは、「図式」「形状」が組み合わせ幾何的対象物〈com…

指標から名前の削除

指標は宣言文の集まりです。各宣言文は、順番〈位置番号〉でも名前でも一意識別できます。実用上は、(順番は覚えにくいので)名前が使われます。が、理論上は名前が邪魔になることがあるので、ときに、名前を削除する必要があります。名前の削除方法の記述…

カリー/ハワード/ランベック対応のための“呼び名”と“書き方”

ここ最近の本ブログのテーマは「カリー/ハワード/ランベック対応」です。最近の記事がすべてカリー/ハワード/ランベック対応に関係するわけではありませんが、9月の記事「関数の構成法 (カリー/ハワード/ランベック対応も少し)」あたりから、カリー/…

コンテキストの圏と指標の圏と限量子

「指標の圏はコンテキストの圏の反対圏」と「指標の圏に対する余ディスプレイ包含構造」で述べたように、コンテキストの圏と指標の圏は互いに反対圏です。この事実を利用することにより、型理論とインスティチューション理論を密接に結びつけることができま…

「命題」と「型」の曖昧性を図示

命題と型は実質的に同じ概念であり、同じ構造を持つ -- これはカリー/ハワード/ランベック対応の主張です。Propositions-as-Types, Types-as-Propositions と表現されることもあります。ところが、「命題」という言葉は非常に曖昧です。同様に「型」という…

群作用と対称な部分集合

x-y-平面において、座標軸上の四点 $`(1, 0), (0, 1), (-1, 0), (0, -1)`$ を順に結んで閉じるとひし形(正方形)ができます。このひし形は、次のようにしても作り出せます; 二点 $`(1, 0), (0, 1)`$ を結ぶ線分は第一象限にあります。この線分を、x軸、y軸…

指標の圏に対する余ディスプレイ包含構造

「指標の圏はコンテキストの圏の反対圏」で述べたように、指標の圏とコンテキストの圏は互いに反対圏です。まさに表裏一体の関係にあります。となると、コンテキストの圏に関する知見を用いて指標の圏を調べる、あるいは逆に、指標の圏に関する知見を用いて…

Autohotkey で、長音記号の入力を楽にした話

IME(日本語入力)において長音記号〈音引き〉の入力には通常マイナスキーを押すでしょう。僕も右小指でマイナスキーを押して長音記号を入力していたのですが、このとき右肘を外に回転させる動作が気になってきました(歳のせいでしょう)。肘・指の動作を少…

ハイティング圏をもう少し

昨日の記事「カリー/ハワード/ランベック対応とハイティング/ド・モルガン圏」で話題にしたハイティング圏について、もう少しダラッと述べます。$` \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\mbf}[1]{\mathbf{#1}} \newcommand{\cat}[1]{\mathca…

カリー/ハワード/ランベック対応とハイティング/ド・モルガン圏

カリー/ハワード/ランベック対応については、このブログ内で何度も言及しています。 このブログ内 ハワード の検索結果 論理/型理論/圏論の三者のあいだに、精密で綺麗な対応があります -- それがカリー/ハワード/ランベック対応です。カリー/ハワー…

型理論の「代入」の分析

型理論では、「代入〈substitution〉」という言葉を幾つかの意味で使います。この記事では複数の意味を切り分けて別な呼び名を与えることにします。ある人々にとっては、いちいち呼び分けることは鬱陶しくてバカバカしいことに思えるでしょう。しかし、誰も…

インターフェイスとしての指標、設計者と利用者と実装者

指標〈signature〉と呼ばれる構文的形式は、数学ならば公理系の記述に使われます。例えば、群の公理系とか可換環の公理系とかを指標で書けます。ソフトウェア/プログラミング分野の言葉で言うなら、指標はインターフェイスです。インターフェイスには、それ…

関数の構成法 (カリー/ハワード/ランベック対応も少し)

与えられた関数達を素材にして新しい関数を作り出すこと -- これは基本中の基本ですね。でも、整理されてないかも知れません。整理しましょう。$` \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\mbf}[1]{\mathbf{#1}} %\newcommand{\msf}[1]{\mathsf{#1…

シーケントに関する不満と対策

昨日の記事「エンテイルメント記号とシーケント」において、従来のシーケントの書き方は変更したほうがいいと提案しました。この機会に、シーケントに対する長年の不満とその対策を記しておきます。$` \newcommand{\Imp}{\Rightarrow } \newcommand{\Ent}{ \…

エンテイルメント記号とシーケント

「記号のグリフと使用場面・使用意図: 型理論、圏論、集合論、論理など」において、矢印記号 '$`\to`$' やターンスタイル記号 '$`\vdash`$' のオーバーロードとコンフリクトが長年の悩みの種であることを述べました。上記過去記事で次のように書きました。 …

プログラミング言語としての Powershell の印象

Windows OS において、バックアップスクリプトを書こうとしたのですが、cmd.exe のバッチファイル〈.batファイル〉で書くのは辛いので Powershell のスクリプト〈.ps1ファイル〉として書くことにしました。Powershell は、シェル(OSのコマンドラインUI)と…

追記: ターンスタイルのオーバーロードの弊害

「型理論のコロン、ターンスタイル、カンマ」への追記ですが別記事にします。ターンスタイルをオーバーロードすることの弊害は、(ターンスタイルに限らないけど)ターンスタイルが表す複数の意味がゴッチャになりがちなことです。もちろん、区別できる人は…

型理論のコロン、ターンスタイル、カンマ

昨日の記事「記号のグリフと使用場面・使用意図: 型理論、圏論、集合論、論理など」より: なんでそこまでコロンとターンスタイルにこだわるのか? 僕にはちょっと意味不明です。...[snip]...僕の個人的感想としては、型理論独自の記法をやめて、圏論と集合…

記号のグリフと使用場面・使用意図: 型理論、圏論、集合論、論理など

あっ、そうか! と気が付きました。型理論、圏論、集合論、論理などを一緒にやるときに、同義語・多義語に悩まされるのですが、記号に関しても同義記号・多義記号のカオス状態にストレスがたまります。例えば、矢印記号に関しては次の過去記事に書いています…

型理論のインスタンスとは

型理論の「インスタンス」の意味がハッキリしないのですが、次の3種にわければだいたい説明が付きそうです。 一般インスタンス ポインティングインスタンス セクションインスタンス 圏論的な解釈をします。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand…

実用になる型理論の記法

型理論では、「代入〈substitution〉」という言葉を幾つかの意味で使います。この記事では複数の意味を切り分けて別な呼び名を与えることにします。ある人々にとっては、いちいち呼び分けることは鬱陶しくてバカバカしいことに思えるでしょう。しかし、誰も…

GAT〈ガット〉の構文: スターリングの論文から

過去記事「GAT〈ガット〉」で、次の論文に言及しました。 [Ste19-] Title: Algebraic Type Theory and Universe Hierarchies Author: Jonathan Sterling Submitted: 23 Feb 2019 Pages: 25p URL: https://arxiv.org/abs/1902.08848 6月にチラ見しただけなの…

ペアの形式的な定義

公理的集合論やグロタンディーク宇宙の公理系では、順序を持たないペアが作れることは保証しています。が、順序を持つペアは頑張って作るのが普通です。作り方は一通りではありません。典型的な順序ペアの作り方を見ておきましょう。$`\newcommand{\mrm}[1]{…

置換公理に出てくる「関数」とは

公理的集合論の置換公理を「関数の像は集合である」と説明したり理解したりする人がいます。まー、そうなんですけど、ここに出てくる「関数」を普通の意味で理解すると、まったくのトンチンカンなことになります。置換公理に出てくる「関数」は、普通の関数…