11簡約システム詳細

本章は，Egisonの数式処理システムの簡約が型システムとどのように連携しているかを詳しく解説する． 第9章では数式の簡約を組み込みの機能として紹介したが，簡約システムは実際には，ユーザーが拡張できるいくつかの直交した仕組みから組み立てられている． 本章では，（1）簡約規則の宣言，（2）イデアルの宣言による規則集合の機械生成，（3）数学関数の宣言，（4）型注釈による正規形の指定，（5）型の昇格タワーとその拡張，（6）タワーの外に置かれる商の型，の6つを順にみていく．

11.1簡約規則の宣言

第9章9.3節でみたように，\(i^2 = -1\)のような組み込みの簡約規則は，処理系のHaskellコードに埋め込まれているのではなく，標準ライブラリのなかでdeclare rule文により宣言されている． ユーザーもまったく同じdeclare rule文で，新しい簡約規則を宣言できる． つまり，組み込みの簡約規則とユーザーの簡約規則は同じ仕組みの上に載っている．

declare rule文は，次の形で書く．

declare rule (auto | name) (term | poly | frac) lhs = rhs

最初の指定子は，規則の適用のされ方を決める． autoを指定した規則（自動規則）は正規化処理に組み込まれ，数式に対する算術演算（+・*・/など）のたびに，適用できなくなるまで繰り返し自動で適用される． 規則名を指定した規則（名前付き規則）については，本節の最後で述べる． 2つ目の指定子は，左辺のパターンを数式のどの構造に対してマッチさせるかを決める． termは各項（単項式）に，polyは各（部分）多項式に，fracは各（部分）分数式に規則を適用する． いずれの場合も，関数適用の引数の内側のような部分式に対しても規則は適用される． 左辺には，リテラルな数式のほかに，パターン変数$xや値パターン#xを含む数式に対するパターン（10.6節）を書くことができる．

たとえば，第9章9.3節でみた\(\sqrt{x} \cdot \sqrt{x} = x\)のようなsqrtの簡約は，標準ライブラリのなかで，sqrtの引数を表すパターン変数$xを使った規則として宣言されている． 概念的には，次のような規則である．

declare rule auto term (sqrt $x)^2 = x

左辺の$xはパターン変数なので，sqrtの引数が具体的な数でもシンボルでも同じようにマッチする． そのため，この1つの規則だけで，たとえば以下がすべて成り立つ．

declare symbol a

(sqrt a)^2 -- a
(1 + sqrt 2)^2 -- 2 * 'sqrt 2 + 3

実際のライブラリの規則は，\((\sqrt{x})^2\)だけでなく一般の冪\((\sqrt{x})^n\)も扱えるよう，これよりもう少し複雑な形をしているが，本質は上のパターン変数を使った1つの規則である．

組み込みの簡約規則も，同じdeclare rule文で標準ライブラリのlib/math/normalize.egiに宣言されている． たとえば，以下は第9章9.3節で紹介した簡約を実現している宣言の一部である．

declare rule auto term i^2 = -1
declare rule auto term log (exp $n) = n
declare rule auto term (exp $x)^$n = exp (n * x)

1つ目のi^2 = -1は，虚数単位\(i\)についての規則である． これは数学的には\(\mathbb{Z}[i] = \mathbb{Z}[X]/(X^2+1)\)という代数拡大（多項式環の商）を，シンボル\(i\)の上に導入する操作にあたる． Egisonの簡約規則は大域的であるが，シンボルは大域的に一意であるため，規則はそのシンボルが現れる数式にしか作用しない． つまり，シンボルの一意性がスコープの役割を果たしている． 二重数（\(\varepsilon^2 = 0\)），1の冪根なども，同じパターンでシンボルの上に導入される代数拡大である． 実装上も，簡約規則は左辺に現れるシンボルで索引づけられており，そのシンボルを含まない数式には規則の適用が試されない． そのため，規則を宣言しても，その規則と無関係な計算はほとんど遅くならない． 2つ目と3つ目の規則のように，左辺にパターン変数を含む規則も宣言できる．

規則名を指定して宣言した名前付き規則は，自動では適用されず，simplify e using nameと書いた場所でだけ式eに適用される． たとえば正弦の加法定理は，左から右に使うと式を展開し，右から左に使うと式をまとめる，方向性のある等式である． このような等式を自動規則にすると，意図しない場所でも展開が起きてしまう． 名前付き規則として宣言しておけば，展開したい場所でだけ明示的に適用できる．

declare symbol a, b
declare rule sinAdd term sin ($x + $y) = sin x * cos y + cos x * sin y

sin (a + b) -- 'sin (b + a)
simplify (sin (a + b)) using sinAdd
-- ('cos b) * ('sin a) + ('cos a) * ('sin b)

11.2イデアルの宣言

前節でみたように，\(i^2 = -1\)のような簡約規則の宣言は，シンボルの上に代数拡大（多項式環のイデアルによる商）を導入する操作である． この見方を進めると，簡約規則の集合そのものをイデアルの生成元から機械的に作り出せる． 本節では，そのためのdeclare ideal文と，その土台になっているグレブナー基底のライブラリ関数を紹介する．

手書きの規則には完全性の問題がある． たとえば\(\sqrt{2}\)，\(\sqrt{3}\)，\(\sqrt{6}\)を表すシンボルs2，s3，s6を導入すると，定義から明らかな関係式は\(s_2^2 = 2\)，\(s_3^2 = 3\)，\(s_6 = s_2 s_3\)の3本である． しかし，この3本を規則として宣言するだけでは，たとえば\(s_2 s_6\)（\(= \sqrt{2}\cdot\sqrt{6} = 2\sqrt{3}\)）は簡約されない． 必要な規則をもれなく手で書き切るのは難しく，書けたとしても，停止性や合流性（適用順序によらず同じ正規形に到達すること）は目視で確かめるしかない．

グレブナー基底の理論は，この問題への数学的な解を与える． 生成元の集合から，イデアルを法とする正規形が一意になる完備な規則集合（被約グレブナー基底）を計算でき，得られる規則集合の停止性と合流性は定理として保証される． EgisonではBuchbergerのアルゴリズムが，ライブラリ関数groebnerBasisとしてEgison自身のパターンマッチで実装されている（lib/math/algebra/groebner.egi）．

declare symbol s2, s3, s6

groebnerBasis [s2^2 - 2, s3^2 - 3, s6 - s2 * s3]
-- [s2^2 - 2, s2 s3 - s6, s2 s6 - 2 * s3,
--  s3^2 - 3, s3 s6 - 3 * s2, s6^2 - 6]

ユーザーが与えたのは自明な3本だが，完備化により\(\{1, \sqrt{2}, \sqrt{3}, \sqrt{6}\}\)の乗法表にあたる6本が得られる． 各元は「先頭の単項式を残りの項（の符号反転）に書き換える」規則として読める（\(s_2 s_6 \to 2 s_3\)など）．

計算した基底は，関数polyNFで式に明示的に適用できる． polyNF gb eは式eのイデアルを法とする正規形を返す． 特に，結果が0になることは，eが関係式の帰結として0に等しいこと（イデアルへの所属）を意味する．

def gb := groebnerBasis [s2^2 - 2, s3^2 - 3, s6 - s2 * s3]

polyNF gb ((s2 + s3)^2) -- 2 * s6 + 5
polyNF gb (s2 * s3 - s6) -- 0

なお，polyNFは渡された多項式の集合をそのまま基底として使う（完備化しない）． 一意な正規形が欲しいときは，上のようにgroebnerBasisを通した基底を渡す．

規則集合として常時適用したい場合は，declare ideal文を使う． 生成元からグレブナー基底が宣言時に一度だけ計算され，各元が項レベルの自動規則として登録される． 以後は通常の簡約規則と同じように，算術演算のたびに自動で適用される．

declare symbol s2, s3, s6

declare ideal [s2^2 - 2, s3^2 - 3, s6 - s2 * s3]

s2 * s6 -- 2 * s3
(s2 + s3)^2 -- 2 * s6 + 5
(s2 + s3) * (s2 - s3) -- -1

実際に，標準ライブラリの1の原始立方根\(w\)の規則は，手書きの2本（\(w^3 = 1\)と\(w^2 = -1-w\)）からdeclare ideal [w^2 + w + 1]という1つの宣言に置き換えられている． 生成される規則\(w^2 \to -1-w\)が\(w^3\)の簡約も2段階で導くので，規則集合の完全性が慣習ではなく定理になる．

複合的な原子にもそのまま使える． 数式データのなかでsin θやcos θは因子（原子）として扱われるので（10.1節），変数への置き換えなしにピタゴラスの関係式を宣言できる．

declare symbol `$\theta$`

declare ideal [(sin `$\theta$`)^2 + (cos `$\theta$`)^2 - 1]

(sin `$\theta$`)^4 - (cos `$\theta$`)^4 -- 2 * 'sin `$\theta$`^2 - 1
(sin `$\theta$`)^2 + 2 * (cos `$\theta$`)^2 -- - 'sin `$\theta$`^2 + 2

正規形にどの原子が残るかは順序で決まっており，シンボルはdeclare symbolの宣言順，生成元のなかの複合原子は出現順で，先に現れたものほど正規形に残る． 上の例では生成元にsin θを先に書いたので，\(\sin\)が残って\(\cos\)の偶数冪が消える向きの規則が生成されている．

declare idealとpolyNFは，「常時適用するか，一度だけ適用するか」の使い分けである． 向き付けされた正規形がいつでも欲しいとは限らず，重い関係式を常時適用すると計算全体が遅くなることもある． たとえば座標の定義多項式のような，計算の最後の検算にだけ使いたい関係式は，polyNFで比較の時点に一度だけ適用するのがよい．

11.3数学関数の宣言

9.2節で紹介したsqrtやexpのような数学関数も，専用の宣言文で定義されている． declare mathfunc文は，適用がシンボリックな値として残る数学関数を宣言する． 宣言しただけの関数の適用は，簡約されずそのままシンボリックな値になる． これにdeclare apply文を組み合わせると，その関数の適用時に一度だけ実行される簡約を定義できる． たとえば，標準ライブラリの対数関数logは以下のように宣言されている．

declare mathfunc log
declare apply log x :=
  match x as mathValue with
    | #1 -> 0
    | #e -> 1
    | _ -> 'log x

declare applyの本体には任意のEgison式を書くことができ，簡約できない入力に対しては，シングルクオート（10.3節）を使って'log xのようにシンボリックな値を返す． 9.2節でみた\(\sqrt{8} \rightarrow 2\sqrt{2}\)のような簡約も，sqrtのdeclare applyで定義されている．

declare applyの簡約が関数の適用時に一度だけ実行されるのに対し，declare ruleの簡約規則は正規化のたびに収束するまで繰り返し適用される． \(\sqrt{8} \rightarrow 2\sqrt{2}\)のように引数の値を調べて計算するアルゴリズム的な簡約はdeclare applyで，\(i^2 = -1\)のように式の形に対する書き換えはdeclare ruleで定義する，という使い分けである．

さらに，declare derivative文を使うと，微分演算子d/d（9.5節）を新しい数学関数に拡張できる． 標準ライブラリの組み込みの微分公式も，この文で宣言されている．

declare derivative sin = cos
declare derivative cos = \z -> - sin z
declare derivative exp = exp
declare derivative log = \z -> 1 / z
declare derivative sqrt = \z -> 1 / (2 * sqrt z)

これらの宣言を組み合わせると，新しい数学関数を数行で数式処理システムに追加できる． たとえば，双曲線正割関数\(\mathrm{sech}\)は以下のように導入できる． 合成関数の微分（連鎖律）はd/dの側が処理するため，導関数の形だけを宣言すればよい．

declare symbol x

declare mathfunc sech
declare apply sech x :=
  match x as mathValue with
    | #0 -> 1
    | _ -> 'sech x
declare derivative sech = \z -> - sech z * tanh z

sech 0 -- 1
sech x -- 'sech x
d/d (sech (x^2)) x -- -2 * ('sech (x^2)) * ('tanh (x^2)) * x

11.4型による正規形の指定

同じ数式は，複数の異なるデータ構造で表現できる． たとえば，

は，原子\(\{i, x\}\)の上の平坦な多項式としても，係数がガウス整数\(\mathbb{Z}[i]\)であるような\(x\)の多項式としても保持できる． どちらの正規形が適切かは，つぎに何をしたいか（\(x\)について微分したいのか，\(\mathbb{Z}[i]\)の性質を使いたいのか）に依存するため，値だけからは決められない． Egisonでは，型注釈でこの正規形を指定する．

declare symbol i, x

def v := (2 + 3 * i) + (1 - i) * x + 4 * x^2

def flat : Poly Integer [i, x] := v
inspect flat
-- "4 * x^2 - i x + x + 3 * i + 2 : Poly Integer [i, x]"

def byX : Poly (Poly Integer [i]) [x] := v
inspect byX
-- "4 * x^2 + (- i + 1) * x + 3 * i + 2 : Poly (Poly Integer [i]) [x]"

型Poly Integer [i, x]は「原子集合\(\{i, x\}\)の上の整数係数多項式」を表す型である． Poly (Poly Integer [i]) [x]のように係数の位置に多項式型を入れ子にすると，「\(\mathbb{Z}[i]\)係数の\(x\)の多項式」という正規形を表す．

原子集合は，[i, x]や[x]のように具体的なシンボルを明示して書く（閉じた原子集合）ほかに，[..]と書いて開いたままにすることもできる． 開いた原子集合[..]は「原子は値から読み取る」という意味であり，どのシンボルが多項式の変数になるかを型の側では固定しない． 入れ子の多項式型の外側の原子集合も，同じように[..]にできる（内側を\(\mathbb{Z}[i]\)に固定したまま，外側の変数は値まかせにする）．

def byX3 : Poly (Poly Integer [i]) [..] := v
inspect byX3
-- "4 * x^2 + (- i + 1) * x + 3 * i + 2 : Poly (Poly Integer [i]) [x]"

この場合，外側の原子集合には値vに現れるxが使われ，観察型はPoly (Poly Integer [i]) [x]になる（\(x\)と\(y\)を含む値なら[x, y]のように変わる）． 次節の昇格タワーがPoly Integer [..]のように開いた原子集合で書かれているのも，特定のシンボルに縛られない一般の多項式を表すためである．

逆に，内側の原子集合を開くこともできる． 外側だけを固定すると，「指定したシンボルだけを多項式の変数として残し，それ以外の原子はすべて係数側に折り込む」という意味になる．

def byI : Poly (Poly Integer [..]) [i] := v
inspect byI
-- "(- x + 3) * i + 4 * x^2 + x + 2 : Poly (Poly Integer [x]) [i]"

ここでは\(i\)だけが外側の変数として残り，同じ値が今度は「\(\mathbb{Z}[x]\)係数の\(i\)の多項式」\((3 - x)i + (4x^2 + x + 2)\)に組み替えられている． ただし，ひとつの入れ子の多項式型（タワー）のなかに[..]を書けるのは高々1箇所である． 開いた原子集合が1つであれば，「閉じた集合に載っている原子はその段へ，残りはすべて開いた段へ」と各原子の行き先が一意に決まるが， 2箇所を開くと（Poly (Poly Integer [..]) [..]など）残りの原子の行き先が曖昧になるため，このような型は型エラーとして拒否される．

型注釈は値を分類するだけでなく，値の内部構造をその型のかたちに組み替える（reshape）． 組み替えは値を変えない． 実際，2つの正規形の差を計算すると\(0\)になる．

flat - byX -- 0

形の異なる表現同士の演算が正しく簡約されるのは，演算の結果は常に既定の平坦形で返るという規約があるためである． 入れ子の正規形は型注釈を書いた場所にだけ現れ，演算をまたいで勝手に伝播することはない．

上の例で使ったinspectは，値と一緒にその値から読み取れる型（観察型）を表示する． よく使う型にはdeclare cas-type文で別名をつけられる． 別名は透明であり，型の表示では展開されたもとの型が使われる．

declare cas-type GaussianPolyX := Poly (Poly Integer [i]) [x]

def byX2 : GaussianPolyX := v
inspect byX2
-- "4 * x^2 + (- i + 1) * x + 3 * i + 2 : Poly (Poly Integer [i]) [x]"

11.5昇格タワーとその拡張

CASの型は，値を保存する埋め込みによって順序づけられている． この順序の背骨は，代数学の包含\(\mathbb{Z} \subset \mathbb{Q} \subset \mathbb{Z}[x] \subset \mathbb{Q}[x] \subset \mathbb{Q}(x)\)をそのまま型の階段にした昇格タワー（promotion tower）である．

Integer                        -- integers
  <: Frac Integer              -- rationals
  <: Poly Integer [..]         -- integer-coefficient polynomials
  <: Poly (Frac Integer) [..]  -- rational-coefficient polynomials
  <: Frac (Poly Integer [..])  -- rational functions
  <: MathValue                 -- all mathematical expressions

タワーの各段は真の部分集合としての埋め込みであり，値を一切変えない． これに加えて，原子集合の包含（Poly Integer [x] <: Poly Integer [x, y]）と，係数位置を通じた埋め込みも順序に含まれる． 異なる型の値を混ぜて演算すると，タワーを上へ昇り，両方を含む最小の型（join）へ自動で昇格する．

def p : Poly Integer [x] := x + 1
def q : Frac Integer := 1 / 2

def r := p + q
inspect r -- "x + 3 / 2 : Poly (Frac Integer) [x]"

原子集合が異なる場合も，原子集合を合併した型へ昇格する．

declare cas-type GaussianInt := Poly Integer [i]
declare cas-type Zsqrt2 := Poly Integer [sqrt2]

def a : GaussianInt := 1 + i
def b : Zsqrt2 := 1 + sqrt2

def c := a + b
inspect c -- "sqrt2 + i + 2 : Poly Integer [i, sqrt2]"

\(\mathbb{Z}[i]\)の値と\(\mathbb{Z}[\sqrt{2}]\)の値の和が，注釈なしで\(\mathbb{Z}[i, \sqrt{2}]\)に着地している．

ここまでのタワーは組み込みだが，タワーは固定ではなく，ユーザーが拡張できる． 前節のdeclare cas-typeは正規形に名前を与え，declare cas-subtypeは新しい辺（埋め込み）をタワーに追加する． たとえば，組み込みの順序は，前節の平坦形（Poly Integer [i, x]）と入れ子形（Poly (Poly Integer [i]) [x]）をあえて関係づけていない． 両者は同じ値の集合の異なる正規形であり，どちらへ昇格すべきかはユーザーの選択だからである． まさにこの選択こそが，ユーザーがタワーに書き加える情報である．

declare cas-subtype Poly Integer [i, x] <: Poly (Poly Integer [i]) [x]

この宣言のあとは，平坦形と入れ子形が混ざる演算は入れ子形へ昇格するようになる．

勝手に辺を追加してもタワーが壊れないように，辺を宣言するたびに， 順序全体で任意の2つの型のjoinが一意に定まること（join半束性）が検査される． 一意性が壊れる宣言は，先に宣言すべき完備化辺の提案つきでエラーになる．

declare cas-subtype Poly Integer [x] <: Poly Integer [i, x]
-- Warning: this edge is already derivable (redundant edge);
--   its endpoints are still registered as nodes for the check

declare cas-subtype Poly Integer [i] <: Poly (Poly Integer [i]) [x]
-- Error: join would become ambiguous (D1 semilattice check).
--   pair (Poly Integer [i], Poly Integer [x]) would get
--   minimal upper bounds
--   {Poly Integer [i, x], Poly (Poly Integer [i]) [x]}
--   hint: declare the completing edge first:
--     declare cas-subtype Poly Integer [i, x]
--       <: Poly (Poly Integer [i]) [x]

\(\mathbb{Z}[i]\)を入れ子形の中に置こうとすると，\(\mathbb{Z}[i]\)と\(\mathbb{Z}[x]\)の共通の上界が 平坦形と入れ子形の2つに分裂してしまうため，宣言は拒否される． 提案される完備化辺は常に数学的に正しい埋め込みであり（平坦形は入れ子形に組み替えられる）， それを先に宣言すれば元の辺も受理される． このように，拡張後のタワーの上でもjoinは常に一意のままであり，暗黙の昇格は決定的であり続ける． なお，この検査はそれまでの宣言に現れた型の上で行われる （上記の1行目の冗長な辺は，Poly Integer [x]を検査対象に登録するために書いている）．

11.6商の型

\(\mathbb{Z}/7\mathbb{Z}\)（7で割った余りの世界）のような商は，これまでの型とは性質が異なる． \(12\)と\(5\)は\(\mathbb{Z}\)では異なる値だが，\(\mathbb{Z}/7\mathbb{Z}\)では等しい． つまり等しさそのものが型に依存するため，値を保存する埋め込みの順序（前節）には入れられない． Egisonでは，商の型はdeclare cas-quotient文で順序の外に宣言する．

declare cas-quotient Mod7 := Integer by (\n -> modulo n 7)

def a : Mod7 := projMod7 5
def b : Mod7 := projMod7 4

a + b -- 2
projMod7 12 == projMod7 5 -- True

宣言すると，整数からMod7への射影projMod7，代表元を取り出すreprMod7，環としての演算，等値判定が自動で導出される． 演算は毎回代表元を簡約するので，値は常に\(0\)から\(6\)の範囲に保たれる． また宣言時には，簡約関数が冪等であることと，加算・乗算と両立する（合同である）ことが，サンプル点の上で検査される．

Mod7の値と生の整数の混在（a + 10など）は型エラーになる． これは\(\mathbb{Z}\)の等しさと\(\mathbb{Z}/7\mathbb{Z}\)の等しさを暗黙に混同しないためであり，世界を横断するときはprojMod7・reprMod7を明示的に使う． 商の上に直接関数を定義することもできる． たとえば\(\mathbb{F}_7\)における逆元は，フェルマーの小定理（\(z^{-1} = z^5\)）を使って1行で書ける．

def inv7 (z : Mod7) : Mod7 := z * z * z * z * z

reprMod7 (inv7 (projMod7 3)) -- 5

商の底は整数に限らず，多項式環をとることもできる． これを使うと，\(x^3 = 0\)とみなして\(3\)次以上の項を捨てる商\(\mathbb{Z}[x]/(x^3)\) ——べき級数を\(3\)次の手前で打ち切った世界——を，ひとつの型として宣言できる． 簡約関数は，各項を走査して\(x\)の次数が\(3\)未満のものだけを残す．

declare symbol x

-- keep a term only when its x-degree is below 3
def dropHigh (t : MathValue) : MathValue :=
  match t as mathValue with
    | term _ ((#x, $k) :: []) -> if k < 3 then t else 0
    | _ -> t

declare cas-quotient Series3 := Poly Integer [x] by
  (\p -> match p as mathValue with
           | poly $ts -> sum (map dropHigh ts)
           | _ -> p)

def s : Series3 := projSeries3 (1 + x)

reprSeries3 (s * s) -- x^2 + 2 * x + 1
reprSeries3 (projSeries3 ((1 + x)^4)) -- 6 * x^2 + 4 * x + 1

\((1 + x)^4 = 1 + 4x + 6x^2 + 4x^3 + x^4\)から\(x^3\)と\(x^4\)の項が消え，\(6x^2 + 4x + 1\)になっている． 底が\(\mathbb{Z}[x]\)になった点を除けば，仕組みはMod7とまったく同じである． なお，この\(x^3 = 0\)は大域的な簡約規則declare rule auto term x^3 = 0でも表せるが， その場合はxが現れるすべての場所で打ち切りが起きる． 商として宣言すると，打ち切りはSeries3型の値だけに閉じ込められ， ふつうのPoly Integer [x]の値は\(3\)次以上の項を保ったままになる． これが，係数領域の商をタワーの外の独立した型として扱うことの利点である．

最後に，本章の道具立てが合流する例として，位数\(4\)の有限体\(\mathrm{GF}(4) = \mathbb{F}_2[\alpha]/(\alpha^2+\alpha+1)\)を作ってみよう． 必要な規律は2つある．係数を\(2\)で割った余りで数えること（係数の商）と，\(\alpha^2 + \alpha + 1 = 0\)という関係で\(\alpha\)の冪を落とすこと（11.2節のイデアル）である． ライブラリ関数finiteFieldReduceは，素数\(p\)と最小多項式の生成元からこの2つを合成した簡約関数を作る． グレブナー基底は宣言時に一度だけ計算され，体の除算にはフェルマーの小定理による逆元が使われる（\(p\)は素数に限る）．

declare symbol `$\alpha$`

declare cas-quotient GF4 := MathValue by finiteFieldReduce 2 [`$\alpha$`^2 + `$\alpha$` + 1]

def a : GF4 := projGF4 `$\alpha$`
def u : GF4 := projGF4 1

reprGF4 ((a + u) * (a + u)) -- `$\alpha$`
reprGF4 (a * (a + u)) -- 1
reprGF4 (a + a) -- 0

\((\alpha+1)^2 = \alpha\)，\(\alpha(\alpha+1) = 1\)（互いに逆元），\(a + a = 0\)（標数\(2\)）と，体の構造が演算のたびに維持される．

底がMathValueであることには意味がある． この型は体のスカラーだけでなく，\(\mathrm{GF}(4)\)係数の多項式も最初から含んでいる． 簡約関数は項の内側の係数にも規律を適用するからである．

declare symbol x, y

reprGF4 (projGF4 (x^2 + 3*x + `$\alpha$`^2)) -- x^2 + x + `$\alpha$` + 1

(projGF4 (`$\alpha$`*x + y)) * (projGF4 (`$\alpha$`*x + y))
  == projGF4 ((`$\alpha$`*x)^2 + y^2) -- True

1つ目では，係数\(3\)が\(1\)に，\(\alpha^2\)が\(\alpha + 1\)に，多項式の項の内側で簡約されている． 2つ目は標数\(2\)の体でだけ成り立つ恒等式\((u+v)^2 = u^2 + v^2\)である． 係数の商（本節）とイデアルによる規則生成（11.2節）という2つの直交した機構が，簡約関数の合成だけで有限体に組み上がる．