mathcomp bigop 概要を和訳

Coq

ガリグ先生の講義の9番目の資料(ssrcoq9.v)で出てくる bigop について、mathcomp.ssreflect.bigop の冒頭を訳しました*1。

ssrcoq9.v の中では Notation であるはずの \big[op/idx]_～ が Definition になっていたりして混乱しますが、直接定義だけを追うより全体像(=この文書の内容)を把握した方が早かったようです。
(といっても Tips の内容は全然分かってませんが…)

概要

This file provides a generic definition for iterating an operator over a set of indices (bigop);
このファイルはインデックス集合上で、あるオペレータを反復する一般的な定義 (bigop) を提供する。

this big operator is parameterized by the return type (R), the type of indices (I), the operator (op), the default value on empty lists (idx), the range of indices (r), the filter applied on this range (P) and the expression we are iterating (F).
このビッグオペレータは返り型 (R)、インデックスの型 (I)、オペレータ (op)、空リストのためのデフォルト値 (idx)、インデックスの範囲 (r)、この範囲に適用されるフィルタ (P)、反復する式 (F) によってパラメタライズされる。

The definition is not to be used directly, but via the wide range of notations provided and which support a natural use of big operators.
定義は直接ではなく、広範囲にわたって提供される記法を通して使用され、それはビッグオペレータの自然な使用をサポートする。

To improve performance of the Coq typechecker on large expressions, the bigop constant is OPAQUE.
大きい式上の Coq の型検査のパフォーマンスを向上するため、定数 bigop は不透明である。

It can however be unlocked to reveal the transparent constant reducebig, to let Coq expand summation on an explicit sequence with an explicit test.
しかしながら透明な定数である reducebig を公開するようにアンロックし、Coq に明示的なシーケンス上で明示的なテストによる概要を展開させることが出来る。

The lemmas can be classified according to the operator being iterated:
その補題は反復されるオペレータに従って分類することが出来ます:

1. Results independent of the operator:

  • extensionality with respect to the range of indices, to the filtering predicate or to the expression being iterated;
  • reindexing, widening or narrowing of the range of indices;
  • we provide lemmas for the special cases where indices are natural numbers or bounded natural numbers ("ordinals").

1. 結果がオペレータに非依存:

  • インデックスの範囲、フィルタする述語、反復される式についての外延性;
  • 再インデックス化、インデックス範囲の拡大や縮小;
  • インデックスが自然数または有界自然数 ("序数")

We supply several "functional" induction principles that can be used with the ssreflect 1.3 "elim" tactic to do induction over the index range for up to 3 bigops simultaneously.
"関数的" 帰納法の原理を提供し、それは3つまでの連続するビッグオペレータのインデックスレンジ上での帰納法を行うため、ssreflect 1.3 "elim" タクティックと一緒に使うことが出来る。

2. Results depending on the properties of the operator: We distinguish: monoid laws (op is associative, idx is an identity element), abelian monoid laws (op is also commutative), and laws with a distributive operation (semirings).
2. 結果がオペレータの性質に依存する: モノイド則 (op は結合的、idx は単位元)、アーベルモノイド則 (op は可換)、分配操作を伴う則 (半環) を区別する。

Examples of such results are splitting, permuting, and exchanging bigops.
そのような結果の例は 分割, 並べ替え, ビッグオペレータ入れ替えである。

A special section is dedicated to big operators on natural numbers.
ある特別なセクションは自然数上のビッグオペレータに特化している。

Notations

Notations: The general form for iterated operators is <bigop>_<range> <general_term>
記法: 反復されるオペレータの一般的な形式は <ビッグオペレータ>_<範囲> <一般項> である。

  • <bigop> is one of \big[op/idx], \sum, \prod, or \max (see below).
  • <ビッグオペレータ> は \big[op/idx]、\sum、\prod、\max (以下参照) のどれかである。
  • <general_term> can be any expression.
  • <一般項> は任意の式になり得る。
  • <range> binds an index variable in <general_term>; <range> is one of
    • (i <- s) i ranges over the sequence s.
    • (m <= i < n) i ranges over the nat interval m, m+1, ..., n-1.
    • (i < n) i ranges over the (finite) type 'I_n (i.e., ordinal n).
    • (i : T) i ranges over the finite type T.
    • i or (i) i ranges over its (inferred) finite type.
    • (i in A) i ranges over the elements that satisfy the collective predicate A (the domain of A must be a finite type).
    • (i <- s | ) limits the range to the i for which <condition> holds. <condition> can be any expression that coerces to bool, and may mention the bound index i. All six kinds of ranges above can have a part.
  • <範囲> は <一般項> 中のインデックス変数を束縛する; <範囲> は以下の内の一つである。
    • (i <- s) i は列 s 上を動く
    • (m <= i < n) i は自然数上の範囲 m, m+1, ..., n-1 を動く
    • (i < n) i は (有限) 型 'I_n (つまり ordinal n) 上を動く
    • (i : T) i は有限型 T 上を動く
    • i or (i) i はその (推論された) 有限型を動く
    • (i in A) i は集合述語 A (A のドメインは有限型でなければならない) を満たす元の上を動く
    • (i <- s | <条件>) i を <条件> を満たす範囲に制限する。<条件> は bool に矯正される任意の式になり得る、そして束縛されたインデックス i に言及するかも知れない。上の6種類全ての範囲は <条件> 部を持つことが出来る。
  • One can use the "\big[op/idx]" notations for any operator.
  • どんなオペレータにも "\big[op/idx]" 記法を使うことが出来る。
  • BIG_F and BIG_P are pattern abbreviations for the <general_term> and <condition> part of a \big ... expression; for (i in A) and (i in A | C) ranges the term matched by BIG_P will include the i \in A condition.
  • BIG_F と BIG_P は \big...式の <一般項> と <条件> 部の省略パターンである; (i in A) と (i in A | C) は BIG_P にマッチされる項を動き、条件 i \in A を含む。
  • The (locked) head constant of a \big notation is bigop.
  • \big 記法の (固定された) ヘッド定数(？？？)は bigop である。
  • The "\sum", "\prod" and "\max" notations in the %N scope are used for natural numbers with addition, multiplication and maximum (and their corresponding neutral elements), respectively.
  • %N スコープ中の "\sum"、"\prod"、"\max" 記法はそれぞれ加算、乗算、最大 (とそれらの中立元に対応する)。
  • The "\sum" and "\prod" reserved notations are overloaded in ssralg in the %R scope;
    • in mxalgebra, vector & falgebra in the %MS and %VS scopes;
    • "\prod" is also overloaded in fingroup, in the %g and %G scopes.
  • 予約記法である "\sum" と "\prod" は %R スコープ中での ssralg 中でオーバーロードされている;
    • mxalgebra 中では %MS と %VS スコープ中でベクトルとF代数であり;
    • fingroup と %g、%G スコープ中では "\prod" もまたオーバーロードされている。
  • We reserve "\bigcup" and "\bigcap" notations for iterated union and intersection (of sets, groups, vector spaces, etc).
  • "\bigcup" と "\bigcap" 記法は (集合、群、ベクトル空間、etc の)反復された和集合と交わりのために予約している。

Tips


Tips for using lemmas in this file: To apply a lemma for a specific operator: if no special property is required for the operator, simply apply the lemma; if the lemma needs certain properties for the operator, make sure the appropriate Canonical instances are declared.
このファイル中の補題を使うチップス: 特定のオペレータに補題を適用するには: そのオペレータに特別な性質が要求されないならば、単にその補題を適用する；その補題がそのオペレータに一定の特徴を必要とするならば、適切な正準インスタンスを確認すること。

Interfaces for operator properties are packaged in the Monoid submodule:
オペレータの性質へのインターフェースは Monoid サブモジュールにパッケージされている:

  • Monoid.law idx == interface (keyed on the operator) for associative operators with identity element idx.
  • Monoid.law idx == 単位元に idx を持つ結合的演算子 (に調整した演算子) のインターフェース
  • Monoid.com_law idx == extension (telescope) of Monoid.law for operators that are also commutative.
  • Monoid.com_law idx == 可換でもある演算子の Monoid.law の拡張 (テレスコープ)*2
  • Monoid.mul_law abz == interface for operators with absorbing (zero) element abz.
  • Monoid.mul_law abz == 吸収 (零) 元 abz を伴う演算子へのインターフェース
  • Monoid.add_law idx mop == extension of Monoid.com_law for operators over which operation mop distributes (mop will often also have a Monoid.mul_law idx structure).
  • Monoid.add_law idx mop == 演算 mop が分配するような演算子のための Monoid.com_law の拡張 (mop は Monoid.mul_law idx 構造を持つことが多い)
  • [law of op], [com_law of op], [mul_law of op], [add_law mop of op] == syntax for cloning Monoid structures.
  • [law of op], [com_law of op], [mul_law of op], [add_law mop of op] == Monoid 構造をクローンする構文。
  • Monoid.Theory == submodule containing basic generic algebra lemmas for operators satisfying the Monoid interfaces.
  • Monoid.Theory == Monoid インターフェースを満たすオペレータのための基本的な一般代数補題を含むサブモジュール
  • Monoid.simpm == generic monoid simplification rewrite multirule.
  • Monoid.simpm == 一般的なモノイド単純化書き換え規則(？)


Monoid structures are predeclared for many basic operators:
Monoid 構造はさまざまな基本演算についてあらかじめ宣言されている:

(_ && _)%B
論理積
(_ || _)%B
論理和
(_ (+) _)%B
排他的論理和
(_ + _)%N
加算
(_ * _)%N
乗算
maxn
最大値
gcdn
最大公約数
lcmn
最小公倍数
(_ ++ _)%SEQ
リスト連結

Additional documentation

Additional documentation for this file:
Y. Bertot, G. Gonthier, S. Ould Biha and I. Pasca.
Canonical Big Operators. In TPHOLs 2008, LNCS vol. 5170, Springer.
Article available at:
http://hal.inria.fr/docs/00/33/11/93/PDF/main.pdf

Examples of use in: poly.v, matrix.v

感想

ここまで頑張って Notation を定義する意味はあるんでしょうか。レンジ型を構成する Notation を定義して \big は高階関数にすれば良さそうに思えますが…？
あと、いい加減 canonical structure 理解したい。

*1:セクション分けは訳者による

*2:ビューってことか？