カッパ計算

Subset of lambda calculus

数理論理学、圏理論、コンピュータサイエンスにおいて、カッパ計算は一次関数を定義するための正式なシステムです。

ラムダ計算とは異なり、カッパ計算には高階関数がなく、その関数は第一級オブジェクトではない。カッパ計算は「型付きラムダ計算の第一階部分の再定式化」とみなすことができる。^[1]

その関数はファーストクラスオブジェクトではないため、カッパ計算式の評価にはクロージャは必要ありません。

意味

以下の定義は長谷川の205ページと207ページの図から改変したものである。^[1]

文法

カッパ計算は、以下の文法で示される型と式で構成されます。

${\displaystyle \tau =1\mid \tau \times \tau \mid \ldots }$

${\displaystyle e=x\mid id_{\tau }\mid !_{\tau }\mid \operatorname {lift} _{\tau }(e)\mid e\circ e\mid \kappa x:1{\to }\tau .e}$

言い換えると、

• 1はタイプ
• と が型である場合は は型です。 ${\displaystyle \tau _{1}}$ ${\displaystyle \tau _{2}}$ ${\displaystyle \tau _{1}\times \tau _{2}}$
• すべての変数は式である
• τが型であれば式である ${\displaystyle id_{\tau }}$
• τが型であれば式である ${\displaystyle !_{\tau }}$
• τが型でeが式であれば、式は ${\displaystyle \operatorname {lift} _{\tau }(e)}$
• とが式である場合、は式である ${\displaystyle e_{1}}$ ${\displaystyle e_{2}}$ ${\displaystyle e_{1}\circ e_{2}}$
• xが変数、τが型、eが式である場合、は式である。 ${\displaystyle \kappa x{:}1{\to }\tau \;.\;e}$

およびid、!、およびの添え字は、文脈から明確に判断できる場合には省略されることがあります。 ${\displaystyle :1{\to }\tau }$ ${\displaystyle \operatorname {lift} }$

並置は、組み合わせと構成の略語としてよく使用されます。 ${\displaystyle \operatorname {lift} }$

${\displaystyle e_{1}e_{2}\ {\overset {\operatorname {def} }{=}}\ e_{1}\circ \operatorname {lift} (e_{2})}$

入力ルール

ここでの提示では、単純型ラムダ計算との比較を容易にするため、仮定的な判断ではなくシークエント（）を用いている。これには追加のVar規則が必要であるが、これは長谷川 ${\displaystyle \Gamma \vdash e:\tau }$^[1]には記載されていない。

カッパ計算では、式は2つの型、すなわちソースの型とターゲットの型を持ちます。表記法は、式eがソースの型とターゲットの型を持つことを示すために使用されます。 ${\displaystyle e:\tau _{1}{\to }\tau _{2}}$ ${\displaystyle {\tau _{1}}}$ ${\displaystyle {\tau _{2}}}$

カッパ計算の式には、次の規則に従って型が割り当てられます。

${\displaystyle {x{:}1{\to }\tau \;\in \;\Gamma } \over {\Gamma \vdash x:1{\to }\tau }}$	（ヴァール）
${\displaystyle {} \over {\vdash id_{\tau }\;:\;\tau \to \tau }}$	（同上）
${\displaystyle {} \over {\vdash !_{\tau }\;:\;\tau \to 1}}$	（バン）
${\displaystyle {\Gamma \vdash e_{1}{:}\tau _{1}{\to }\tau _{2}\;\;\;\;\;\;\Gamma \vdash e_{2}{:}\tau _{2}{\to }\tau _{3}} \over {\Gamma \vdash e_{2}\circ e_{1}:\tau _{1}{\to }\tau _{3}}}$	（比較）
${\displaystyle {\Gamma \vdash e{:}1{\to }\tau _{1}} \over {\Gamma \vdash \operatorname {lift} _{\tau _{2}}(e)\;:\;\tau _{2}\to (\tau _{1}\times \tau _{2})}}$	（リフト）
${\displaystyle {\Gamma ,\;x{:}1{\to }\tau _{1}\;\vdash \;e:\tau _{2}{\to }\tau _{3}} \over {\Gamma \vdash \kappa x{:}1{\to }\tau _{1}\,.\,e\;:\;\tau _{1}\times \tau _{2}\to \tau _{3}}}$	（カッパ）

言い換えると、

• Var:仮定すると、 ${\displaystyle x:1{\to }\tau }$ ${\displaystyle x:1{\to }\tau }$
• Id:任意の型τの場合、 ${\displaystyle id_{\tau }:\tau {\to }\tau }$
• バン：任意の型τに対して、 ${\displaystyle !_{\tau }:\tau {\to }1}$
• 合成:のターゲット型がのソース型と一致する場合、それらはのソース型とのターゲット型を持つ式を形成するように合成される可能性があります。 ${\displaystyle e_{1}}$ ${\displaystyle e_{2}}$ ${\displaystyle e_{2}\circ e_{1}}$ ${\displaystyle e_{1}}$ ${\displaystyle e_{2}}$
• リフト：ならば、 ${\displaystyle e:1{\to }\tau _{1}}$ ${\displaystyle \operatorname {lift} _{\tau _{2}}(e):\tau _{2}{\to }(\tau _{1}\times \tau _{2})}$
• カッパ：という仮定の下でと結論づけられるならば、その仮定なしに と結論づけられるかもしれない。 ${\displaystyle e:\tau _{2}\to \tau _{3}}$ ${\displaystyle x:1{\to }\tau _{1}}$ ${\displaystyle \kappa x{:}1{\to }\tau _{1}\,.\,e\;:\;\tau _{1}\times \tau _{2}\to \tau _{3}}$

平等

カッパ計算は次の等式に従います。

• 中立性:ならば、そして ${\displaystyle f:\tau _{1}{\to }\tau _{2}}$ ${\displaystyle f{\circ }id_{\tau _{1}}=f}$ ${\displaystyle f=id_{\tau _{2}}{\circ }f}$
• 結合性:、、の場合、 となります。 ${\displaystyle f:\tau _{1}{\to }\tau _{2}}$ ${\displaystyle g:\tau _{2}{\to }\tau _{3}}$ ${\displaystyle h:\tau _{3}{\to }\tau _{4}}$ ${\displaystyle (h{\circ }g){\circ }f=h{\circ }(g{\circ }f)}$
• 終末性：もし、そして ${\displaystyle f{:}\tau {\to }1}$ ${\displaystyle g{:}\tau {\to }1}$ ${\displaystyle f=g}$
• 揚力低減: ${\displaystyle (\kappa x.f)\circ \operatorname {lift} _{\tau }(c)=f[c/x]}$
• カッパ還元: xがh内で自由でない場合 ${\displaystyle \kappa x.(h\circ \operatorname {lift} _{\tau }(x))=h}$

最後の 2 つの等式は、左から右に書き直す計算の簡約規則です。

プロパティ

タイプ1はユニット型とみなすことができます。これにより、引数の型が同じで結果の型が1は等しいはずです。なぜなら、型の値は1つしかないからです。1両方の関数は、すべての引数に対してその値を返す必要があります ( Terminality )。

型を持つ式は「定数」または「基底型」の値とみなすことができます。これは、 ${\displaystyle 1{\to }\tau }$1は単位型なので、この型から得られる関数は必然的に定数関数となる。カッパ則は、抽象化される変数が何らかのτの型を持つ場合にのみ抽象化を許可することに注意されたい。これは、すべての関数が一階であることを保証する基本的なメカニズムである。 ${\displaystyle 1{\to }\tau }$

カテゴリカルセマンティクス

カッパ計算は、文脈的に完全なカテゴリーの内部言語となることを目的としています。

例

複数の引数を持つ式のソース型は「右不均衡」な二分木です。例えば、A、B、Cの3つの引数とDの戻り値を持つ関数fは、以下の型を持ちます。

${\displaystyle f:A\times (B\times (C\times 1))\to D}$

左結合の並置をの略語として定義すると、 、、 と仮定して、次の関数を適用できます。 ${\displaystyle f\;c}$ ${\displaystyle (f\circ \operatorname {lift} (c))}$ ${\displaystyle a:1{\to }A}$ ${\displaystyle b:1{\to }B}$ ${\displaystyle c:1{\to }C}$

${\displaystyle f\;a\;b\;c\;:\;1\to D}$

式にはソース型があるため ${\displaystyle f\;a\;b\;c}$1 の場合、これは「基底値」であり、他の関数の引数として渡すことができます。の場合、 ${\displaystyle g:(D\times E){\to }F}$

${\displaystyle g\;(f\;a\;b\;c)\;:\;E\to F}$

ラムダ計算の型のカリー化された関数と同様に 、部分適用が可能です。 ${\displaystyle A{\to }(B{\to }(C{\to }D))}$

${\displaystyle f\;a\;:\;B\times (C\times 1)\to D}$

しかし、より高次の型（つまり ）は関係ありません。faのソース型は ${\displaystyle (\tau {\to }\tau ){\to }\tau }$1、次の式は、これまでに述べた仮定の下では適切に型付けできません。

${\displaystyle h\;(f\;a)}$

連続適用は複数の引数に対して使用されるため、関数の型を決定するために関数の引数の数を知る必要はありません。例えば、次の式が ${\displaystyle c:1{\to }C}$

jc

jが型を持っている限り、型付けは適切である

${\displaystyle (C\times \alpha ){\to }\beta }$あるαについて

そしてβ 。この特性は式の主要な型を計算する際に重要であり、型の文法を制限することで型付きラムダ計算から高階関数を除外しようとする場合には困難となる可能性がある。

歴史

バレンドレグトは、組合せ代数の文脈において「関数完全性」という用語を最初に導入した^[2] 。カッパ計算は、任意のカテゴリに対する関数完全性の適切な類似性を定式化しようとしたラムベック^{[3]の努力から生まれた（エルミダとジェイコブス[4]} 、第1節参照）。長谷川は後にカッパ計算を、自然数上の算術演算と原始的再帰を含む、（単純ではあるが）実用的なプログラミング言語へと発展させた^{[1] 。}矢印 との関連は、後にパワー、ティーレケらによって研究された^{[5] 。}

変種

カッパ計算には、線形、アフィン、順序付きといった部分構造型を用いたバージョンがあります。これらの拡張には、式を除去または制限する必要があります。このような状況では、×型演算子は真の直積ではなく、そのことを明確にするために通常は⊗ と表記されます。 ${\displaystyle !_{\tau }}$

参考文献

1. 長谷川正人 (1995). 「型付きラムダ計算をいくつかのカテゴリカルプログラミング言語に分解する」. ピット, デイビッド; ライドハード, デイビッド E.;ジョンストン, ピーター(編).カテゴリー理論とコンピュータサイエンス. コンピュータサイエンス講義ノート. 第953巻. シュプリンガー・フェアラーク・ベルリン・ハイデルベルク. pp.  200– 219. CiteSeerX 10.1.1.53.715 . doi :10.1007/3-540-60164-3_28. ISBN  978-3-540-60164-7. ISSN  0302-9743.
   • Adam (2010年8月31日). 「κappa-圏とは何か？」MathOverflow .
2. Barendregt, Hendrik Pieter編（1984年10月1日）『ラムダ計算：その構文と意味論』論理学と数学の基礎研究第103巻（改訂版）アムステルダム、北ホラント州：エルゼビア・サイエンス。ISBN 978-0-444-87508-2。
3. ラムベック, ヨアヒム(1973年8月1日). 「カルティシアン圏の機能的完全性」Annals of Mathematical Logic . 6 ( 3–4 ) (1974年3月発行): 259– 292. doi :10.1016/0003-4843(74)90003-5. ISSN  0003-4843.
   • Adam (2010年8月31日). 「κappa-圏とは何か？」MathOverflow .
4. クラウディオ・ヘルミダ、バート・ジェイコブス（1995年12月）「不定値を持つファイブレーション：多形ラムダ計算の文脈的完全性と機能的完全性」『コンピュータサイエンスにおける数学的構造』5 (4): 501– 531. doi :10.1017/S0960129500001213. ISSN  1469-8072. S2CID  3428512.
5. パワー、ジョン;ティーレッケ、ハヨ (1999)。 「閉じられたフレイドおよびκカテゴリー」。イジのヴィーダーマンにて。ピーター・ファン・エムデ・ボアス;ニールセン、モーゲンス (編)。オートマトン、言語、プログラミング。コンピューターサイエンスの講義ノート。 Vol. 1644年。シュプリンガー・フェルラーク・ベルリン・ハイデルベルク。ページ 625 ～ 634。CiteSeerX 10.1.1.42.2151。土井：10.1007/3-540-48523-6_59。ISBN  978-3-540-66224-2. ISSN  0302-9743.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Kappa_calculus&oldid=1320783335"