Remove ads
ウィキペディアから
圏論において、圏がデカルト閉(デカルトへい、英語: cartesian closed)であるとは、大雑把に言えば任意の二つの対象の直積上で定義される射が直積因子の一方で定義される射と自然に同一視できることである。デカルト閉な圏はラムダ計算の自然な設定ができるという点で数理論理学およびプログラミングの理論において特に重要である。デカルト閉圏の概念はモノイド圏に一般化される(モノイド閉圏を参照)。
圏 C がデカルト閉であるとは、以下の三条件
が全て満たされることをいう。上ふたつの条件は、組み合わせて「C の対象からなる任意の有限族(空でも構わない)に対し、それらの直積対象が C に存在する」という一つの条件に読み替えることができる。これは、圏における直積が自然な結合性をもつことと、圏における空積はその圏の終対象となることとに拠る。
3番目の条件は圏 C の任意の対象 Y に対して、関手 – × Y(すなわち、C から C への関手であって、任意の対象 X に対し X × Y を対応させ、任意の射 φ に対し φ × idY を対応させるもの)が右随伴 –Y を持つこと仮定することに同値である。これはまた、hom-集合の間に双射
で X と Z の両方に関して自然変換となっているものが存在することとも言い換えられる。
任意のスライス圏がデカルト閉であるような圏は、局所デカルト閉 (locally cartesian closed) であるという。
デカルト閉圏の例として以下のようなものが挙げられる。
デカルト閉ではない圏の例には以下のようなものが挙げられる。
デカルト閉圏において、「二変数関数」(つまり、射 f: X × Y → Z)は常に「一変数関数」(つまり射 λf: X → ZY)として表現できる。計算機科学における応用ではこれはカリー化として知られ、単純型付ラムダ計算の任意のデカルト閉圏における解釈を実現に導く。
カリー-ホワード-ランベック対応は直観主義論理、単純型付ラムダ計算、デカルト閉圏の間の深い同型を与える。
トポスという種類のデカルト閉圏は、数学に対する従来の集合論に替わる一般的な枠組みとして提示された。
高名な計算幾何学者ジョン・バッカスは(後から考えるとデカルト閉圏の内部言語にどこか似たところのある)無変数記法あるいは関数レベルプログラミングを提唱した。CAMLはデカルト閉圏のさらに意識的なモデルである。
任意のデカルト閉圏において(冪記法を用いて)、(XY)Z と (XZ)Y は任意の対象 X, Y, Z に対して同型である。これを等式の形で
と書き表す。任意のデカルト閉圏において、ほかに有効な等式にはどんなものがあるだろうか。これについては、以下の公理に従って論理的にすべての有効な等式を計算することができる[2]。
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.