t-wise testing 入門

マイクロソフト製テストケース生成ツール PICT を同僚に教えてもらいました。そのツールと、それが実装しているテスト生成アルゴリズムを紹介しているペーパー Czerwonka, Pairwise testing in real world, 2006 を読んだので、PICT とそれが採用している生成アルゴリズムである t-wise strategy について簡単に紹介します。

t-wise testing strategy

問題設定としては、「テスト対象のパラメータが幾つかと、それぞれのパラメータの取り得る値の(有限通りの)バリエーション(レベルと呼ぶ)が与えられたとき、良い組み合わせのテストケースを生成する」というものです。

ここでテストケースとは各パラメータに対応するレベルの集合のことをいい、パラメータとレベルとConstraint(後述)のことをまとめてモデルと呼びます。

当然全てのレベルのあらゆる組み合わせを生成(してテスト)すれば最も安心なワケですが、組み合わせ数が爆発しますので、実際的なシステムのテストには現実的ではありません。

良いテストケースが何かというのは難しい問題ですが、一般的には、よりバリエーションに富んだ(つまり一部のパラメータのレベルの組み合わせが冗長だったりしない)組み合わせを含みつつ、現実的な入力に対して十分小さい出力を生成出来ることが望ましいでしょう。

そこで PICT が採用しているテストケース生成戦略が、 t-wise strategy です。

これは、互いに異なる t 個のパラメータの全てのレベルの組み合わせが含まれるようにテストケースを生成するものです。

t=2 の場合は特に Pairwise testing (strategy) と呼ばれます。PICT のデフォルト設定も t=2 です。

例: モデル1

例えば、レベルa1,a2,a3を取るパラメータA、レベルb1,b2を取るパラメータB、レベルc1,c2と取るパラメータCを持つモデルを考えた場合、生成される組み合わせは以下の6通りになります。

ParamA ParamB ParamC
a1 b2 c2
a1 b1 c1
a3 b2 c1
a2 b1 c2
a2 b2 c1
a3 b1 c2

ParamA と ParamB だけを考えれば $\{a1,a2,a3\}\times{}\{b1,b2\}$ の6通り全てが出現していますし、ParamB と ParamC に注目すれば $\{b1,b2\}\times{}\{c1,c2\}$ の4通りが網羅されています。

3つのパラメータのあらゆる組み合わせを網羅するためには $3\times{}2\times{}2=12$ 通りになりますが、ここでは任意の二つのパラメータの組み合わせを尽くすように生成しているため6通りで済みます。このケースでは、例えば $\{a1,b2,c1\}$ という組み合わせは生成されていません。

上の例を PICT に与えるには以下のように記述します。

ParamA: a1, a2, a3
ParamB: b1, b2
ParamC: c1, c2

見たままです。

Constraint

任意のレベルの(pairwiseの)組み合わせを考えた場合、その中にシステムとして不正な入力が含まれてしまうことがあります。これをあらかじめ生成対象から排除するための組み合わせを指定する式を Constraint として与えることが出来ます。

例えば以下のような入力(モデル2)を PICT に与えると:

ParamA: a1, a2, a3
ParamB: b1, b2
ParamC: c1, c2
# constraint
IF [ParamA] = "a2" THEN [ParamB] <> "b2" ;

次のような出力になります。

ParamA ParamB ParamC
a3 b1 c1
a2 b1 c2
a2 b1 c1
a1 b2 c2
a3 b2 c1
a3 b2 c2
a1 b1 c1

$\{a2,b2\}$ を含む組み合わせが出力から除かれています。また $a2$ と $b2$ をそれぞれ含む(t=2の)組み合わせを網羅するために出力が冗長になり、7通りのテストケースが生成されています。

PICT では Constraint を(生成してからフィルタするのではなく)生成器側で(生成候補に排除マークを付けることで)考慮しており、効率的にテストケースを生成出来ます。

Seeding

(ランダムテストではなく) t-wise testing の場合でも、必要な条件を満たす組み合わせにはバリエーションがあり、そこからどれが選ばれるかは実装依存となります。

PICT ではこの選択は決定的に行われ、含んでいるべきレベルの集合($\subset{t{-}wise\ test}$) を与えることで、含んでいるべき組み合わせ(の族)を明示的に与えることが出来ます。

例えば、最初のモデル1に加えて以下のような seed を与えると:

# NOTE: 本物のファイルはタブ区切り
ParamA	ParamB	ParamC
a1      b1      c2

次のような出力が得られます。

ParamA ParamB ParamC
a1 b1 c2
a3 b2 c2
a2 b1 c2
a3 b1 c1
a1 b2 c1
a2 b2 c1

モデル1の出力では含まれていなかった $\{a1,b1,c2\}$ を含んでいます。

seed として一部のパラメータのみを指定することも出来、これによって

  • モデルの変更時の変更を小さくしたり、
  • 変更しづらいパラメータの組み合わせの変更を抑えたり

することが出来ます。

ランダムテスト(QuickCheck)との比較

QuickCheckのようなランダムテスト系と異なり、

  • パラメータ(やレベル)の増加をほとんど気にしなくてもいい点、
  • どのような性質を持ったテストケースなのかが分かり易い点、
  • また実装と表現力次第ですが、constraintを好きなだけ与えることが出来る点*1
  • 特定の組み合わせ(の族)を含むように指定することが簡単に出来る点

が優れていると思います。一方、以下のようなことは苦手です。

  • 特定のレベルの出現確率を任意に調整する
    t-wise strategy では組み合わせの冗長性を廃してテストケースを出来るだけ小さくするのが基本目標なので、出現確率分布を出力にナイーブに反映出来ません。
  • (ある範囲の)数値パラメータについて網羅的に生成(検査)する
    組み合わせ爆発するため $[0, 2^{32})$ のようには指定出来ません。(0, 10, 100, 10000のように与える必要があります)

感想

この論文は2006のものですが、pairwise testing 自体は80年代には提案されていたようです。

だからなのかは分かりませんが、問題設定も提案手法自体も非常にナイーブで分かり易いものです。またその分実装や改良が比較的簡単に行えそうです(ほんとか？)。

また私はほぼ常に論文を読むより先にツールを動かそうとするため*2、実際に簡単に動かせるツール (PICT) があり、使い方が(15年前の)論文そのままなのも良かった点として挙げておきます。

機を見計らって実用していきたいです。

*1:QuickCheck系では前提が満たされづらいpredicateをナイーブに与えるとテスト本体がほとんど実行されない

*2:分野によりますが

sigplanブログにMPLの記事が投稿されていた

日記 SML MaPLe

並列MLであるMPLについての記事がsigplanのブログに投稿されていました> Provably Space-Efficient Parallel Functional Programming | SIGPLAN Blog。
面白いし論文より分かり易いので読みましょう。


MPLはSMLに並列計算のための機能を追加した並列MLの一つです。Parallel for関数*1を使うとruntimeがスケジューリングします。
MLtonをforkして開発されており、シーケンシャルなプログラムについてはMLtonと同じように使うことが出来るので使いましょう。
以前このブログでも紹介しました > 並列ML: MaPLe v0.2 がリリースされていた - ::Eldesh a b = LEFT a | RIGHT b ちょうど1年前ですね(POPL2021の論文を読んだ時期)。


sigplanの記事はとても分かり易いので改めて紹介することは特に無いんですが一応まとめておくと、ポイントとしては以下二つで：

  • (dis)entanglement というプログラムとヒープについての並列化出来るフラグメントについて(大抵簡単に)成り立つ性質を提案
  • それを使ったヒープのCPU割り当てをスレッドスケジューラと統合(GCとも統合？)
  • 学部生でも並列アルゴリズム記述するのに使えたよ(eldesh注: CMUの学生である)

です。


気になる点として、(dis)entanglementであることを機械的に保証or検査する手段が無いというのが有ったんですが、
直近のコミットには CONTROL_FLAGS.detectEntanglement というのが含まれており、とりあえず動的な検査が可能になりそうです。


リポジトリをwatchしている感じでは、わずかずつですが基幹的な部分にコミットがあるので Sam Westrick 先生の次回作に期待です。

*1:ForkJoin.parfor

Coqのモジュールの基本機能

Coq

あけましておめでとうございます。今年もよろしくお願いします。


Coqのモジュール関連の機能について和訳したので基本的な機能を紹介します。
リファレンスの文中で「対話的」モジュールとされているのは Vernacular を使って定義するからで、実体は Structure です*1 。


Coqのモジュールは(S)MLのモジュールに近い機能で、型とその実装をひとまとめにして名前を付けることができます。
実はリファレンスを読んだだけではどんな機能か分からなかったので分かったことをこの記事にまとめます(多分構文はOCamlに近いけどワタシ用のメモなので随所でSMLと比較しています)。

基本

SMLで言うstructureとsignatureはそれぞれCoqでは Module(モジュール) と Module Type(モジュール型) という名前で扱われます。
ただしCoqではこれらはお互いにネストできます。


モジュールのフィールドにアクセスするには、MLと同じくモジュールとフィールド名をドット(.)で区切った表記を使います。
例えばモジュールOptionのフィールドmapにアクセスしたければOption.mapです。

定義

モジュールはModule identからEnd identの間に、モジュール型の方は Module Type identとEnd identの間に定義を書きます。

モジュールの定義
(* モジュール M の定義 *)
Module M.
  Definition T := nat.         (* 型 T を持つ *)
  Definition x : T := 0.       (* 型 T を持つ x を持つ *)
  Definition y : bool.         (* 型だけ指定すると証明モードになる *)
  Proof. exact true. Defined.
End M.

普通ですね。Module M : SIG. で制約を指定して定義を始めることも出来ます。

モジュール型の定義
Module Type SigM.
  Parameter T : Set.
  Parameter x : T.
  Declare Module M : SigM2.
End SigM.

こちらもほぼ見たままで、モジュールに要求する制約に名前を付ける定義です。

Declare というのは「～というモジュール型を満たすモジュールを含むべき」という制約の宣言を表します。
SMLなら単に structure M : SigM2 と書くところですが、Coq では冒頭述べた通りモジュール型の定義中にモジュールの定義が出来てしまうので明示的に書き分ける必要があります。

制約

MLのモジュールは特定のシグネチャを満たしていることを強制出来ますが、Coqでも同じことが出来ます。
(SMLと表記が微妙に違って混乱する…)

不透明(opaque)制約

Module CM : SigM := M. (* SigM を満たす実装 M を与える *)
Fail Print CM.y.       (* SigM には y が含まれていないので CM.y も見え無い *)

: SigMは不透明制約と呼ばれます。モジュールCMがモジュール型SigMを満たすことを確認し、かつSigMに含まれるフィールド以外を隠蔽します。
つまりSigMに記述されているフィールドにのみCMのフィールドとしてアクセス出来ます。


以下のようにその場で実装を与えることも出来ます。

Module CM : SigM.
  Definition T := nat.
  Definition x := 0.
  Definition y : bool.
  Proof. exact true. Defined.
End CM.

CM.xでCMモジュールの外からxにアクセス出来ますが、SigM.Tの実装は隠蔽されているため、CM.xの値は見えません。

Print CM.x.  (* *** [ CM.x : CM.T ] *)

透明(transparent)制約

モジュールが特定の制約を満たすことだけを確認し、実装を隠蔽しないことも出来ます。これを透明制約と言います。

Module TCM <: SigM := M. (* SigM を満たす実装 M を与える *)
Print TCM.x.
(* TCM.x = 0 : nat *)

透明制約はモジュールの実装に影響しないため、モジュール外部でもTCM.xがnatだということが分かります。

合成/拡張

Coqのモジュール(型)はモジュール同士を合成したり、一部を詳細化したり、拡張したり出来ます。

Include

モジュール(型)定義内でInclude <module-ident>を実行すると、指定したモジュールの内容がその場に導入されます。

Module Nat1Core.
  Inductive natopt := SOME : nat -> natopt | NONE.
  Definition t := natopt.
End Nat1Core.

Module Nat1Map.
  Include Nat1Core.
  Definition map f (x : t) : t := (* Nat1Core.t が修飾無しで使える *)
    match x with | SOME x => SOME (f x) | NONE => NONE end.
End Nat1Map.

Print Nat1Map.
(**
Module Nat1Map := Struct
     Inductive natopt : Set :=  SOME : nat -> natopt | NONE : natopt.
     Definition natopt_rect : ..
     Definition natopt_ind : ..
     Definition natopt_rec : ..
     Definition natopt_sind : ..
     Definition t : Set.
     Definition map : (nat -> nat) -> t -> t.
   End
 *)

SMLのopenやincludeに似ていますが、同名の定義が表れたときの扱いはCoqの方が厳しく、後に出現した方は(同様の定義であっても)エラーになります。

Module OnlyNat. Definition n := nat. End OnlyNat.
Module Nat2.
  Include OnlyNat. (* n := nat が導入される *)
  Definition n := nat. (* n already exists. *)
End Nat2.

Import

モジュール(型)定義内でImport <module-ident>を実行すると、指定したモジュールのフィールド名が導入されます。
上のIncludeに似ていますが、インポートしたフィールドはモジュール定義の一部になるわけでは無いことに注意して下さい。

Module Nat1Core. .. End Nat1Core.

Module Nat1Map.
  Import Nat1Core.
  Definition map f (x : t) : t := (* Include のときと同じく Nat1Core.t が修飾無しで使える *)
    match x with | SOME x => SOME (f x) | NONE => NONE end.
End Nat1Map.

Print Nat1Map.
(**
Module Nat1Map := Struct
  (* t の定義は含まれ無い *)
  Definition map : (nat -> nat) -> Nat1Core.t -> Nat1Core.t.
End
 *)

Nat1Mapの定義にDefinition tが含まれていないことに注意して下さい。
定義時に(モジュール内部で)修飾無しにアクセス出来るようになっただけであり、現在のモジュールの一部になるわけでは無いということです。


定義の一部になっていないため、以下のように定義し直せば(？)実装の一部にすることが出来ます。

Module Nat1Map.
  Import Nat1Core.
  Definition t := t.       (* インポートされた t を使って Nat1Map.t を定義 *)
  ..
End Nat1Map.
Print Nat1Map.
(**
Module Nat1Map := Struct
  Definition t : Set.      (* 定義に追加されている *)
  Definition map : (nat -> nat) -> t -> t.
End
 *)

Export

Export <module-ident>は、Importに加えて、現在のモジュールがImportされた際にmodule-identのフィールドも同時に導入される機能です。

Module Nat2Map.
  Export Nat1Core.
  Check t.                        (* Import と同様にフィールドを導入する *)
  Definition map f (x : t) : t := ..
End Nat2Map.
Print Nat2Map.
(**
Module Nat2Map := Struct 
  Definition map : (nat -> nat) -> t -> t. (* Nat1Core.t は定義の一部にはならないが… *)
End
 *)

Import Nat2Map.
Check t.        (* インポートすると t が見える *)

定義に表れない名前が導入されるなんて実際に使われたらものすごく混乱する機能な気がします…。

with句

(公式には特に構文に名称は付いてないもよう)

型指定

Module Typeに含まれる一部の定義をその場で与えて詳細化することが出来ます。SMLのwhereに相当します。

Module N : SigM with Definition T := nat := M.
Eval compute in (N.x : nat).
(* = N.x : nat *)
Fail Eval compute in (CM.x : nat). (* CM: 不透明制約のセクションで定義したやつ *)
(**
The term "CM.x" has type "CM.T" while it is expected to have type "nat".
 *)
モジュール指定

withにはモジュールを指定することも出来、サブモジュールが特定の実装になっていることも表現出来ます*2。

Module Type Single.
  Parameter t : Set.  Parameter v : t.
End Single.

(* モジュールを要求するモジュール型を作る *)
Module Type Wrap.
  Declare Module In : Single.
End Wrap.

Module SBool.
  Definition t := bool.  Definition v : t := true.
End SBool.

(* boolで実装を与える *)
Module WrapB.
  Module In := SBool.
End WrapB.

Module MBool : Wrap := WrapB.
Fail Check (false : MBool.In.t). (* 実装は見えないため型チェックに失敗する *)

Module MBool' : Wrap with Module In := SBool := WrapB. (* サブモジュールに SBool を指定 *)
Print MBool'.
Check (false : MBool'.In.t).     (* 実装が見えている *)

この例の場合、サブモジュールInがSBoolになっていることを強制しています。

*1:さらにStructureはRecordの別名です。https://coq.inria.fr/distrib/V8.8.2/refman/language/gallina-extensions.html#coq:warn.ident-cannot-be-defined

*2:これに相当することはSMLでは出来ません

CoqのマニュアルのTermの章を翻訳した

Coq 日記

Coq v8.8.2 の Term の章を翻訳しました。
この章では Gallina の項の構成について説明しています。


恐らくトピックとして一番難しいのは依存型を扱うマッチ式についての説明で、詳細は別のページに独立してるくらいですが、この章で示されている例は簡潔なので分かり易いです(それでも難しいんですが…)。


あと分かりにくいと言ったら型キャストの部分で、term <: typeとかterm <<: typeは項目が存在する割には全く説明が無いに等しいので何のことやら全然分かりません。これはヒドイ。


他に気になったところでは cofix についての説明で、以下の説明に依るとこれは相互(構造)再帰ではないようなんですね。

The expression “fix ident1 ..." ... defined by mutual structural recursion. It is the local counterpart of the Fixpoint command.
...
The expression “cofix ident1 ..." ... defined by a mutual guarded co-recursion. It is the local counterpart of the CoFixpoint command.

https://coq.inria.fr/distrib/V8.8.2/refman/language/gallina-specification-language.html#recursive-functions

和訳した方では相互ガード付き余再帰としてありますがどうなんでしょう。
油断すると再帰と呼んでしまう気がしますね。

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:ビューってことか？

opamでmathcompをインストールした

Coq 勉強会

最近 coqtokyo 第7回Ssreflect勉強会 に参加しています。
隔週で火曜日にやっているので是非。


もうすぐ第五回講義資料(ssrcoq5.pdf)に到達しますが、ここでようやく mathcomp の話が出てきます。
さっそく opam で mathcomp をインストールしようとしたところ、以下のようなエラーが出ました。

eldesh@hostname:~/work/garrigue.git$ opam install coq-mathcomp-ssreflect
The following actions will be performed:
  ∗ install coq-mathcomp-ssreflect 1.12.0

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved coq-mathcomp-ssreflect.1.12.0  (cached)
[ERROR] The compilation of coq-mathcomp-ssreflect.1.12.0 failed at "make -C mathcomp/ssreflect -j 3".

#=== ERROR while compiling coq-mathcomp-ssreflect.1.12.0 ======================#
# context     2.1.0 | linux/x86_64 | ocaml-base-compiler.4.05.0 | https://coq.inria.fr/opam/released#2021-10-15 21:00
# path        ~/.opam/4.05.0/.opam-switch/build/coq-mathcomp-ssreflect.1.12.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -C mathcomp/ssreflect -j 3
# exit-code   2
# env-file    ~/.opam/log/coq-mathcomp-ssreflect-122950-b76a3b.env
# output-file ~/.opam/log/coq-mathcomp-ssreflect-122950-b76a3b.out
### output ###
# make: Entering directory '/home/eldesh/.opam/4.05.0/.opam-switch/build/coq-mathcomp-ssreflect.1.12.0/mathcomp/ssreflect'
# /bin/sh: 1: /home/eldesh/lcl/bincoqtop: not found
# /bin/sh: 1: /home/eldesh/lcl/bincoqtop: not found
# /home/eldesh/lcl/bincoq_makefile  -f Make -o Makefile.coq
# make: /home/eldesh/lcl/bincoq_makefile: Command not found
# ../Makefile.common:55: recipe for target 'Makefile.coq' failed
# make: *** [Makefile.coq] Error 127
# make: *** Waiting for unfinished jobs....
# make: Leaving directory '/home/eldesh/.opam/4.05.0/.opam-switch/build/coq-mathcomp-ssreflect.1.12.0/mathcomp/ssreflect'



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build coq-mathcomp-ssreflect 1.12.0
└─
╶─ No changes have been performed

ここがよく解りませんね🤔

# /bin/sh: 1: /home/eldesh/lcl/bincoqtop: not found

PATH も正常に見えます。

eldesh@hostname:~/work/garrigue.git$ which coqc
/home/eldesh/.opam/4.05.0/bin/coqc
eldesh@hostname:~/work/garrigue.git$ echo $PATH
/home/eldesh/.opam/4.05.0/bin:/home/eldesh/.cargo/bin:/home/eldesh/.local/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games

実は COQBIN が犯人で、以下のようになっていました。

export COQBIN=/home/eldesh/lcl/bin

おそらく opam は ${COQBIN}coqtop としているんでしょう。(/ は冗長でも意味変わらないので付けるべきなんですが、空の場合を判定する手間を嫌ったんでしょう)
というワケで、末尾に / を付けて解決しました。

export COQBIN=/home/eldesh/lcl/bin/

MLLex と MLYacc を Poly/ML に移植

SML

移植

MLLex と MLYacc を Poly/ML で使えるように移植しました。
移植と言うよりは使える状態のリポジトリを作って Makefile とか書きましたというだけですが、やはりこの二つは重要なので使える状態で維持したいですね。


移植先のリポジトリは eldesh/mllex-polyml と eldesh/mlyacc-polyml です。
どちらも MLton のリポジトリから持ってきたもので、ドキュメントなどもビルド出来るようにはしてますが中身はそのままです。

インストール

以下のようにしてインストール出来ます。

$ make install PREFIX=~/.sml/polyml/5.8.1

他の処理系向けのコマンドと区別が付かないので、実行コマンド名はそれぞれ mllex-polyml と mlyacc-polyml としてあります*1。

SML/NJ では mlyacc-lib.cm が提供されていたりするので今回の移植版でもライブラリをインストールします。

Poly/ML のパーサ事情

他の SML 処理系は大抵 mllex/mlyacc を使ってパーサが書いてあります。このため実装がそれぞれの内部に mllex と mlyacc を抱え込んでます。
一方 Poly/ML は全部手書きパーサで頑張ってますので独立した lex/yacc を持っていないため移植する必要がありました。

*1:mllex と mlyacc にシンボリックリンク張るとかしてもいいかも？