「指標の圏はコンテキストの圏の反対圏」と「指標の圏に対する余ディスプレイ包含構造」で述べたように、コンテキストの圏と指標の圏は互いに反対圏です。この事実を利用することにより、型理論とインスティチューション理論を密接に結びつけることができま…
命題と型は実質的に同じ概念であり、同じ構造を持つ -- これはカリー／ハワード／ランベック対応の主張です。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〉」という言葉を幾つかの意味で使います。この記事では複数の意味を切り分けて別な呼び名を与えることにします。ある人々にとっては、いちいち呼び分けることは鬱陶しくてバカバカしいことに思えるでしょう。しかし、誰も…
指標〈signature〉と呼ばれる構文的形式は、数学ならば公理系の記述に使われます。例えば、群の公理系とか可換環の公理系とかを指標で書けます。ソフトウェア／プログラミング分野の言葉で言うなら、指標はインターフェイスです。インターフェイスには、それ…
与えられた関数達を素材にして新しい関数を作り出すこと -- これは基本中の基本ですね。でも、整理されてないかも知れません。整理しましょう。$` \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\mbf}[1]{\mathbf{#1}} %\newcommand{\msf}[1]{\mathsf{#1…
昨日の記事「エンテイルメント記号とシーケント」において、従来のシーケントの書き方は変更したほうがいいと提案しました。この機会に、シーケントに対する長年の不満とその対策を記しておきます。$` \newcommand{\Imp}{\Rightarrow } \newcommand{\Ent}{ \…
「記号のグリフと使用場面・使用意図： 型理論、圏論、集合論、論理など」において、矢印記号 '$`\to`$' やターンスタイル記号 '$`\vdash`$' のオーバーロードとコンフリクトが長年の悩みの種であることを述べました。上記過去記事で次のように書きました。 …
Windows OS において、バックアップスクリプトを書こうとしたのですが、cmd.exe のバッチファイル〈.batファイル〉で書くのは辛いので Powershell のスクリプト〈.ps1ファイル〉として書くことにしました。Powershell は、シェル（OSのコマンドラインUI）と…
「型理論のコロン、ターンスタイル、カンマ」への追記ですが別記事にします。ターンスタイルをオーバーロードすることの弊害は、（ターンスタイルに限らないけど）ターンスタイルが表す複数の意味がゴッチャになりがちなことです。もちろん、区別できる人は…
昨日の記事「記号のグリフと使用場面・使用意図： 型理論、圏論、集合論、論理など」より： なんでそこまでコロンとターンスタイルにこだわるのか？ 僕にはちょっと意味不明です。...[snip]...僕の個人的感想としては、型理論独自の記法をやめて、圏論と集合…
