最近の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軸…

「指標の圏はコンテキストの圏の反対圏」「型理論とインスティチューション理論が繋がるぞ！」で述べたように、指標の圏とコンテキストの圏は互いに反対圏です。まさに表裏一体の関係にあります。となると、コンテキストの圏に関する知見を用いて指標の圏を…

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

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

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

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