Loading article…
コンピュータサイエンスの型理論の分野において、商型はユーザ定義の等価関係を尊重するデータ型です。商型は型の要素の同値関係を定義します。たとえば、型の 2 つの値は、同じ名前を持つ場合、等価であると言えます。正式には の場合です。商型を許可する型理論では、すべての演算が要素間の同値性を尊重する必要があるという追加要件が設けられています。たとえば、 が型 の値の関数である場合、2 つのおよびに対してである場合、となります。
Personp1 == p2p1.name == p2.namefPersonPersonp1p2p1 == p2f(p1) == f(p2)
商型は代数的データ型として知られる型の一般クラスの一部である。1980年代初頭、商型はロバート・L・コンスタブルらの主導による研究の中で、Nuprl 証明支援系の一部として定義され実装された。 [1] [2]商型は、マーティン・レーフ型理論、[3]依存型理論、[4]高階論理、[5]ホモトピー型理論の文脈で研究されてきた。[6]
意味
商型を定義するには、通常、データ型とその型の同値関係を指定します。たとえば、Person // ==は==ユーザー定義の同値関係です。商型の要素は、元の型の要素の同値類です。 [3]
商型はモジュラー算術を定義するために使用できます。たとえば、がInteger整数のデータ型である場合、差が偶数であれば と定義できます。次に、2を法とする整数の型を形成します。[1]
Integer //
整数に対する演算は、+新しい-商型上で明確に定義されていることが証明できます。
バリエーション
商型を持たない型理論では、商型の代わりにsetoid （同値関係を明示的に備えた集合）がよく使われる。しかし、setoidとは異なり、多くの型理論では商型上で定義された関数が適切に定義されているという正式な証明が必要になる場合がある。[7]
プロパティ
商型は代数的データ型として知られる型の一般クラスの一部である。積型と和型が抽象代数構造の直積と非結合和に類似しているのと同様に、商型は集合論的商の概念を反映している。集合論的商とは、集合上の同値関係によって要素が同値類に分割される集合である。商を基礎とする代数構造も商と呼ばれる。このような商構造の例には、商集合、群、環、カテゴリ、位相幾何学における商空間などがある。[3]
参考文献
- ^ ab Constable, Robert L. (1986). Nuprl Proof Development System による数学の実装。Prentice-Hall. ISBN 978-0-13-451832-9。
- ^ Constable, RL (1984). 「プログラミングとしての数学」。Clarke, Edmund、Kozen, Dexter (編)。プログラムの論理。コンピュータサイエンスの講義ノート。第 164 巻。ベルリン、ハイデルベルク: Springer。pp. 116–128。doi : 10.1007 /3-540-12896-4_359。hdl : 1813 / 6405。ISBN 978-3-540-38775-6。
- ^ abc Li, Nuo (2015-07-15). 「型理論における商型」eprints.nottingham.ac.uk . 2023年9月13日閲覧。
- ^ Hofmann, Martin (1995). 「商型の簡単なモデル」.型付きラムダ計算とその応用. コンピュータサイエンスの講義ノート. 第902巻. ベルリン、ハイデルベルク: Springer. pp. 216–234. doi :10.1007/BFb0014055. ISBN 978-3-540-49178-1。
- ^ Homeier, Peter V. (2005)。「高階商の設計構造」。Hurd, Joe、Melham, Tom (編)。高階論理における定理証明。コンピュータサイエンスの講義ノート。第3603巻。ベルリン、ハイデルベルク：Springer。pp. 130–146。doi :10.1007/ 11541868_9。ISBN 978-3-540-31820-0。
- ^ 「The HoTT Book」。ホモトピー型理論。2013年3月12日。 2023年9月13日閲覧。
- ^ Hofmann, Martin (1997). 「内包型理論における外延的構成」SpringerLink . doi :10.1007/978-1-4471-0963-1. ISBN 978-1-4471-1243-3。