コンピュータサイエンスの型理論の分野において、商型はユーザ定義の等価関係を尊重するデータ型です。商型は型の要素に同値関係を定義します。たとえば、型の 2 つの値がそれぞれ同じ x 座標と y 座標を持つ場合、それらは等価であると言えます。正式にはの場合です。商型を許容する型理論では、すべての演算が要素間の同値性を尊重する必要があるという追加要件が設けられています。たとえば、 が型 の値の関数である場合、2 つのおよびに対して が成り立ち、の場合が成り立ちます。
Pointp1 == p2p1.x == p2.x && p1.y == p2.yfPointPointp1p2p1 == p2f(p1) == f(p2)
商型は、代数的データ型として知られる一般的な型クラスの一部です。1980年代初頭、ロバート・L・コンスタブルらの研究により、商型はNuprl 証明支援系の一部として定義・実装されました。[1] [2]商型は、マルティン＝レーフ型理論、[3]依存型理論、[4]高階論理、[5]ホモトピー型理論の文脈で研究されてきました。[6]
意味
商型を定義するには、通常、データ型とその型に対する同値関係を指定します。例えば、Point // ==は==ユーザ定義の同値関係です。商型の要素は、元の型の要素の同値類です。 [3]
商型は剰余算術を定義するために使用できます。例えば、Integerが整数のデータ型である場合、差が偶数であればは と定義できます。そして、2を法とする整数の型は次のようになります。[1]
Integer //
整数に対する演算は、+新しい-商型で明確に定義されていることが証明できます。
バリエーション
商型を持たない型理論では、商型の代わりにsetoid（同値関係を明示的に備えた集合）がしばしば用いられる。しかし、setoidとは異なり、多くの型理論では、商型上に定義された関数がwell-definedであることの形式的な証明が求められる場合がある。[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日閲覧。
- ^ ホフマン、マーティン (1995). 「商型の単純なモデル」.型付きラムダ計算とその応用. コンピュータサイエンス講義ノート. 第902巻. ベルリン、ハイデルベルク: シュプリンガー. 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日閲覧。
- ^ ホフマン、マーティン (1997).内包型理論における外延的構成概念. doi :10.1007/978-1-4471-0963-1. ISBN 978-1-4471-1243-3。
参照
