最近の話題から

HOList with HOL Light
https://sites.google.com/view/holist/home

TacticToe with HOL4
https://www.thibaultgauthier.fr/tactictoe.html

さらに
http://aitp-conference.org/2019/
http://arg.ciirc.cvut.cz/teaching/mlr19/index.html
http://ai4reason.org/demos.html

CoqGym with Coq
https://github.com/princeton-vl/CoqGym

MetaGen with MetaMath
https://openreview.net/pdf?id=BJxiqxSYPB


PVS は...
https://github.com/nasa/vscode-pvs

数理論理3:構文論

今回は
・言語に対して,その言語の定理式の全体が定まること
をLKと呼ばれる流儀で述べます.

以下,言語,その言語の論理式の集合Σを任意に固定します.

(定義3-1)論理式の任意の集合の対(Ψ,Ω)をシーケントと呼び,Σから導出可能なシーケントの全体は,次の1.から16.(3.から16.を推論規則と呼びます)を満たす最小の集合です.以下,この集合に(Ψ,Ω)が属することを Ψ \longrightarrow Ω で表します.

xが変数記号,tが項,A,Bが論理式,CがΣの元,X,Yが論理式の(空でもよい)有限列ならば

1.{}\longrightarrow{C}
2.{A}\longrightarrow{A}

3.{X}\longrightarrow{Y}ならば{X}\longrightarrow{A,Y}かつ{A,X}\longrightarrow{Y}
4.{X}\longrightarrow{A,Y}かつ{A,X}\longrightarrow{Y}ならば{X}\longrightarrow{Y}

5.{A,X}\longrightarrow{Y}ならば{X}\longrightarrow{¬A,Y}
6.{X}\longrightarrow{A,Y}ならば{¬A,X}\longrightarrow{Y}

7.{A,B,X}\longrightarrow{Y}ならば{A∧B,X}\longrightarrow{Y}
8.{X}\longrightarrow{A,Y}かつ{X}\longrightarrow{B,Y}ならば{X}\longrightarrow{A∧B,Y}

9.{X}\longrightarrow{A,B,Y}ならば{X}\longrightarrow{A∨B,Y}
10.{A,X}\longrightarrow{Y}かつ{B,X}\longrightarrow{Y}ならば{A∨B,X}\longrightarrow{Y}

11.{A,X}\longrightarrow{B,Y}ならば{X}\longrightarrow{A→B,Y}
12.{X}\longrightarrow{A,Y}かつ{B,X}\longrightarrow{Y}ならば{A→B,X}\longrightarrow{Y}

13.{X}\longrightarrow{A,Y}ならば{X}\longrightarrow{∀xA,Y}
  ただし,X,Yの各論理式にxの自由出現はないとします(これを固有変数条件と呼びます).
14.{A内のxの全ての自由出現をtに置き換えたもの,X}\longrightarrow{Y}ならば{∀xA,X}\longrightarrow{Y}
  ただし,置き換えにより新たな束縛は生じないとします(これを代入可能条件と呼びます).

15.{A,X}\longrightarrow{Y}ならば{∃xA,X}\longrightarrow{Y}
  ただし,固有変数条件は満たされているとします.
16.{X}\longrightarrow{A内のxの全ての自由出現をtに置き換えたもの,Y}ならば{X}\longrightarrow{∃xA,Y}
  ただし,代入可能条件は満たされているとします.

なお,(定義3-1)も(定義1-2)のように「適当な・・・によって・・・と表せるもの」という表現も可能です.そして

・ {X}\longrightarrow{Y}を X \longrightarrow Y 或いは Σ \vdash\longrightarrow Y と書きます.また,とくに Σ \vdash \longrightarrow A を Σ \vdash A(Σが空集合ならば \vdash A)と書き,これを「AはΣの構文論的帰結」或いは「AはΣの定理式」或いは「AはΣから証明可能」(Σ が空集合ならば「Aは定理式」或いは「Aは証明可能」)と読みます.
・ (定義3-1)の集合は帰納的に定義されているので,1.または2.から{X}\longrightarrow{Y}に至る過程に現れるΣの元は有限個です.従って,Σ \vdash\longrightarrow Yならば,Σの有限部分集合Σ’が存在して Σ’ \vdash\longrightarrow Y となります.
・ 固有変数条件を満たさない代入を許すと,例えば,xが変数記号,pが1項述語記号ならば,px→∀xpx が定理式になってしまいます.
・ 代入可能条件を満たさない代入を許すと,例えば,xが変数記号,pが1項述語記号ならば,∀xpxx→∃x∀ypxy が定理式になってしまいます.

(例3-1)x,yが異なる変数記号,pが1項述語記号ならば
 \longrightarrow(¬(∀xpx))→∃x(¬px)
となるには,11. により
 ¬(∀xpx)\longrightarrow∃x(¬px)
となればよく,それには,6. により
 \longrightarrow∀xpx,∃x(¬px)
となればよく,それには,13. により
 \longrightarrowpy,∃x(¬px)
となればよく,それには,16. により
 \longrightarrowpy,¬py
となればよく,それには,5. により
 py\longrightarrowpy
となればよく,2. により,(¬(∀xpx))→∃x(¬px)は定理式です.

(例3-2 https://en.wikipedia.org/wiki/Drinker_paradox )シーケントは集合の対なので,その集合の要素を複製することが可能です.したがって,x,yが異なる変数記号,pが1項述語記号ならば
 \longrightarrow∃x(px→∀xpx)
となるには
 \longrightarrow∃x(px→∀xpx),∃x(px→∀xpx)
となればよく,それには
 \longrightarrowpx→∀xpx,∃x(px→∀xpx)
となればよく,それには
 px\longrightarrow∀xpx,∃x(px→∀xpx)
となればよく,それには
 px\longrightarrowpy,∃x(px→∀xpx)
となればよく,それには
 px\longrightarrowpy,py→∀xpx
となればよく,それには
 px,py\longrightarrowpy,∀xpx
となればよく,それには
 py\longrightarrowpy,∀xpx
となればよく,それには
 py\longrightarrowpy
となればよいので,∃x(px→∀xpx)は定理式です.

こうした手続きを上下を逆にして次のツールが生成するような図で表したものをその定理式の証明図と呼びます.http://bach.istc.kobe-u.ac.jp/seqprover/

(参考)
https://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK

数理論理2:意味論

今回は
・言語,構造,割り当てに対して,その言語の項,論理式の値が定まること
そして
・言語に対して,その言語の valid な論理式の全体が定まること
を述べます.

以下,言語を固定します.

(定義2-1)構造は空でない集合D(domainと呼びます)と次のような写像I(解釈と呼びます)の対です.
 fがn項関数記号ならば
  n>0ならば,I(f)はD^nからDへの写像
  n=0ならば,I(f)∈D
 pがn項述語記号ならば
  n>0ならば,I(p)はD^nから{0,1}への写像
  n=0ならば,I(p)∈{0,1}
また,Dの濃度#Dを構造の濃度と呼びます.

なお,構造のことを解釈,或いは,モデルと呼ぶ流儀もあります.

次に,構造(D,I)を固定します.

(定義2-2)割り当てsは変数記号全体からDへの写像です.x,y,...が変数記号,d,e,...∈Dならば,sのx,y,...の像をそれぞれd,e,...に改めた割り当てをs[x→d,y→e,...]で表します.

(定義2-3)付値は(関数,述語,論理記号の出現の個数に関する帰納法により定義される)次のような写像||です.
 sが割り当て,xが変数記号ならば,|x|=s(x)
 gがn項関数または述語記号,t1,...,tnが項ならば
  n>0ならば,|g(t1,...,tn)|=I(g)(|t1|,...,|tn|)
  n=0ならば,|g|=I(g)
 A,Bが論理式ならば
  |¬A|=1-|A|
  |A∧B|=|A|×|B|
  |A∨B|=1-(1-|A|)×(1-|B|)
  |A→B|=1-|A|×(1-|B|)
 sが割り当て,xが変数記号,Aが論理式ならば
  |∀xA|={s[x→d]に対して定義された||による|A|:d∈D}の元の積
  |∃xA|={s[x→d]に対して定義された||による|A|:d∈D}の元の和

この定義において,付値による各元の像を元の値と呼びます.各項の値はDに属し,各論理式の値は{0,1}に属します.また,各割り当てに対して,付値は項と論理式全体の集合からD∪{0,1}への準同型写像になっています.

以下,言語のみを固定します.

(例2-1)A,Bが論理式ならば,任意のS,sに対して
  |((A→B)→A)→A|
 =1-|(A→B)→A|×(1-|A|)
 =1-(1-|A→B|×(1-|A|))×(1-|A|)
 =1-(1-(1-|A|×(1-|B|))×(1-|A|))×(1-|A|)
であり,|A|∈{0,1}により,この値は1です.

(例2-2)xが変数記号,Aが論理式ならば,任意のS,sに対して
  |¬(∀xA)|
 =1-|∀xA|
 =1-({s[x→d]に対して定義された||による|A|:d∈D}の元の積)
 ={1-(s[x→d]に対して定義された||による|A|):d∈D}の元の和
 ={s[x→d]に対して定義された||による|¬A|:d∈D}の元の和
 =|∃x(¬A)|
となります.

(定義2-4)Sが構造,sが割り当て,||が付値,A,Bが論理式,Σが論理式の(有限とは限らない)集合ならば
1.|A|=1を(S,s)|=Aと書き,「S,sはAを充足」と読み,そうしたS,sが存在するようなAを「充足可能」と呼びます.
2.任意のsに対して(S,s)|=AをS|=Aと書き,「AはSにおいてvalid」或いは「SはAのモデル」と読みます.
3.任意のBに対して,B∈ΣならばS|=BをS|=Σと書き,「SはΣのモデル」と読みます.
4.任意のSに対して,S|=ΣならばS|=AをΣ|=Aと書き,「AはΣの意味論的帰結」と読みます.
5.任意のS,sに対して,|A|=|B|をA≡Bと書き,「A,Bは同値」と読みます.

(定義2-4)において

・ Aが閉論理式ならば,|A|は割り当てによらないので,|A|=1はS|=Aであり(単に「SはAを充足」と読みます),Aが充足可能とAがモデルを持つは等価です.
・ Σが有限集合ならば
   {A1,...,An}|=AはA1,...,An|=A
   {}|=Aは|=A
のように{ }を略して書くことがあり
   |=Aを「Aは valid」と読みます.
   A|=Bは|=(A→B)と等価であり,これをA⇒Bと書きます.
   A|=BかつB|=Aは|=(A→B)∧(B→A)と等価であり,これをA⇔Bと書きます.
   A⇔BはA≡Bと等価です.
・  |=Aは,任意のS,sに対して,(S,s)|=Aつまり|A|=1つまり|¬A|=0と書けるので,入力されたAにおいて束縛されない全ての変数記号を定数記号とみなし,それがvalidであることを確かめよう,或いは,|¬A|=1となるS(これをAのカウンターモデルと呼びます)を見付けてvalidでないことを確かめようとする https://www.umsu.de/trees/ のようなツールがあります.
・ 論理式全体は,適当なS,sに充足される(充足可能といいます)論理式全体と,そうでない(充足不可能といいます)論理式全体に分割され,前者の部分集合として適当なSにおいて valid な論理式全体があり,さらにその部分集合として valid な論理式全体があります.

(例2-1)により
 |=((A→B)→A)→A つまり (A→B)→A|=A つまり (A→B)→A⇒A
(例2-2)により
 ¬(∀xA)≡∃x(¬A) つまり ¬(∀xA)⇔∃x(¬A)
となります.

なお,(定義2-4)において,より強く

4.任意のS,sに対して,「任意のBに対して,B∈Σならば(S,s)|=B」ならば(S,s)|=AをΣ|=Aと書き,「AはΣの意味論的帰結」と読みます.

とする流儀もあります.この場合,Σ∪{A}|=B ならば Σ|=A→B(意味論的な演繹定理 )がAが閉論理式でなくても成り立つ(つまり,pが1項述語記号,x,yが変数記号であっても{p x}|=p yとならない)など,構文論との対応が失われますが,閉論理式に限定するなら差異はありません.

nfsplitting(*,,2);

私が案出した Galois 群の計算方法を PARI の開発メンバーの方にお伝えしたところ,それに基づいた nfsplitting さらに galoisinit の改良版を作成してくださいました. 試用方法は
https://pari.math.u-bordeaux.fr/cgi-bin/gitweb.cgi?p=pari.git;a=tree;h=refs/heads/bill-nfsplitting;hb=refs/heads/bill-nfsplitting
の snapshot のリンクをクリック,保存,展開して

./Configure;make all;./gp

で,PARI が起動します.以下,実行例です.

? #
   timer = 1 (on)
? galoisinit(nfsplitting(x^17-2)); \\ 従来の方法
  *** galoisinit: Warning: increasing stack size to 16000000.
  *** galoisinit: Warning: increasing stack size to 32000000.
  *** galoisinit: Warning: increasing stack size to 64000000.
time = 1h, 3min, 8,876 ms.
? galoissplittinginit(x^17-2); \\ 新作
  *** galoissplittinginit: Warning: increasing stack size to 16000000.
  *** galoissplittinginit: Warning: increasing stack size to 32000000.
  *** galoissplittinginit: Warning: increasing stack size to 64000000.
time = 20,935 ms.
? g=nfsplitting(f=x^17-2);nfisincl(f,g); \\ 従来の方法
  *** nfisincl: Warning: increasing stack size to 16000000.
  *** nfisincl: Warning: increasing stack size to 32000000.
time = 20,210 ms.
? nfsplitting(x^17-2,,1); \\ 処理の共通部分をまとめたもの.出力は分解体の定義多項式と入力の全ての根の分解体上での表示です.
  *** nfsplitting: Warning: increasing stack size to 16000000.
  *** nfsplitting: Warning: increasing stack size to 32000000.
time = 16,544 ms.
? nfsplitting(x^17-2,,2); \\ 出力は分解体の定義多項式とその Galois 群の写像表示です.
  *** nfsplitting: Warning: increasing stack size to 16000000.
  *** nfsplitting: Warning: increasing stack size to 32000000.
time = 16,846 ms.

数理論理1:言語

ちょっとした経緯があり,数理論理(古典一階論理)の基本事項を少し書きます.

今回は
・言語に対して,その言語の項,論理式の全体が定まること
を述べます.

(定義1-1)言語は,次のような互いに区別できる記号の集合です.
 n項関数記号 (各nは非負整数)
 n項述語記号 (1個以上,各nは非負整数)
 変数記号 x1 x2  … (可算個)
 論理記号 ¬ ∨ ∧ → (結合子とも呼びます) ∀ ∃ (量化子とも呼びます)
 補助記号 ( , )

ここで,関数記号,述語記号は言語を特徴付けるもので
・それぞれの全体(と各記号に上記のnを対応させる関数)の組をその言語のシグネチャーと呼びます.
なお
・関数記号,述語記号を非論理記号,その他(つまり,全ての言語に共通するもの)を論理記号と呼ぶ流儀,また,等号=を論理記号に含める流儀もあります.

言語を固定すると,その言語の項,論理式が以下のように定まります.

(定義1-2)項は
 0項関数記号 (定数記号とも呼びます)
 変数記号
 適当なn(>0)項関数記号f,n個の適当な項t1,...,tn,補助記号によってf(t1,...,tn)と表せるもの
のいずれかです.

(例1-1)xが変数記号,cが定数記号,fが2項関数記号ならば,f(x,c)は項です.

なお,(定義1-2)では「逆にこれらはいずれも項です.」を略しており,正確には,現れる定数記号でない関数記号の個数に関する帰納法により

 T(0)=変数記号の全体と定数記号の全体との和集合
 任意の非負の整数jに対して
  T(j+1)=∪_{n≧1}{f(t1,...,tn):fはn項関数記号,t1,...,tnはそれぞれT(m_1),...,T(m_n)の元.ただし,m_1,...,m_nは和がjである非負の整数.}
と定め,項全体を
 ∪_{j≧0}T(j)
と定めます.

そして,f(t1,...,tn)は,項の個数に関する帰納法により

 f(t1,...,t1)=f(t1)
 任意の正の整数jに対して
  f(t1,...,t(j+1))=f(t1,...,tj)の最後の ")" を ",t(j+1))" に置き換えたもの
と定めます.

同様に(定義1-3),(定義2-3)は関数,述語,論理記号の出現の個数,(定義3-1)は推論規則を適用した回数に関する帰納法による定義です.

(定義1-3)論理式は
 0項述語記号 (命題記号とも呼びます)
 適当なn(>0)項述語記号f,n個の適当な項t1,...,tn,補助記号によってp(t1,...,tn)と表せるもの
のどちらか(これらを原子論理式と呼びます),或いは,適当な変数記号x,論理式A,Bおよび論理記号,補助記号によって
 ¬(A)
 (A)∧(B)
 (A)∨(B)
 (A)→(B)
 (∀x)(A) (この∀xのx,および,A内の各xをxの(全称)束縛出現といいます)
 (∃x)(A) (この∃xのx,および,A内の各xをxの(特称)束縛出現といいます)
のいずれかと表せるものです.

ここで
・論理式に現れる個々の変数記号をその変数記号の出現
・束縛出現でない変数記号の出現を自由出現
・各変数記号の出現がすべて束縛出現である論理式を閉(じた)論理式,そうでない論理式を開(いた)論理式
そして
・閉論理式以外の元をもたない集合を理論
と呼びます.

なお,A,Bが論理式ならな
 (A)\leftrightarrow(B)は((A)→(B))∧((B)→(A))
の略記とします.

また,言語の定義において,論理記号は,例えば ¬ ∧ ∃ のみとして
 (A)∨(B)は ¬((¬(A))∧(¬(B)))
 (A)→(B)は ¬(A∧(¬(B)))
 (∀x)(A)は ¬((∃x)(¬(A)))
それぞれの略記と定義する流儀もあります.

(例1-2)x,yが変数記号,fが1項関数記号,pが1項述語記号,rが2項述語記号ならば
 r(f(x),y)
 ((∀x)(p(x)))→(p(x))
はどちらも論理式,そして
 (∃x)((p(x))→((∀x)(p(x))))
は閉論理式です.

(例1-2)の論理式をそれぞれ
 rfxy
 (∀xpx)→px 或いは (∀x(p(x)))→p(x)
 ∃x(px→∀xpx) 或いは ∃x(p(x)→∀x(p(x)))
などのように記すこともあり,本稿もその作法に従います.

(定義1-4)Aが論理式,x,y,..がAに現れる束縛されていない全ての変数記号ならば,Aの全称閉包は閉論理式∀x∀y...(A)です.

論理式を"閉じる"方法としては,各変数の自由出現を各変数ごとに新たな定数記号に置き換えるというものもあり,本稿のメタ論理でも暗にそれを採用しています.

(参考)
https://www.encyclopediaofmath.org/index.php/Formalized_language

代数体上の線型方程式系の求解

今回の冪根拡大の構成では,中間体上の線型方程式系(連立一次方程式)を解くことが一つの柱となっています( http://ehito.hatenablog.com/entry/2019/04/11/193241 ).それは例えば,定義多項式

c5^4+c5^3+c5^2+c5+1,
e1^2+10,
e2^5+((-3750*c5^3)-3750*c5^2-1875)*e1-3125*c5^3+9375*c5^2+6250*c5+3125

である体 Q(c5,e1,e2) 上で

(((10*a4-2*a3+30*a2-70*a1+360)*e1-10*a4-20*a3-150*a2-100*a1-600)*c5^3
         +((10*a4-14*a3+30*a2-90*a1+360)*e1-30*a4-20*a3-50*a2-100*a1-1000)
          *c5^2+(((-16*a3)-160*a1)*e1-40*a4-200*a2-1600)*c5
         +(5*a4-8*a3+15*a2-80*a1+180)*e1-240*e2-20*a4-10*a3-100*a2+250*a1-800)
         /240,
        (((2*a4-20*a3-10*a2-140*a1+40)*e1-20*a4-60*a3-100*a2+100*a1-800)*c5^3
         +((4*a4-20*a3-20*a2-140*a1+80)*e1-20*a4-100*a2+200*a1-800)*c5^2
         +((6*a4-30*a2+120)*e1-60*a3+300*a1)*c5
         +(3*a4-40*a3-15*a2-120*a1+60)*e1-48*e2^2-60*a4-30*a3-100*a2+150*a1
         -2000)
         /48,
        -(((125*a4+10*a3+575*a2+750*a1+4900)*e1
         +150*a4-450*a3+250*a2-2750*a1+5000)
         *c5^3
         +((125*a4-30*a3+575*a2-250*a1+4900)*e1
          -250*a4-450*a3-1750*a2-2750*a1-11000)
          *c5^2+(((-20*a3)+500*a1)*e1-100*a4-1500*a2-6000)*c5
         +(100*a4-10*a3+100*a2+250*a1+3200)*e1+48*e2^3-50*a4-600*a3-750*a2
         -4000*a1-3000)
         /48,
        -(((450*a4+1000*a3+3750*a2+3000*a1+21000)*e1
         -1500*a3-5000*a2-7500*a1-10000)
         *c5^3
         +((400*a4+1000*a3+3000*a1+12000)*e1-5000*a3-5000*a2-10000*a1-10000)
          *c5^2+((850*a4+3750*a2+33000)*e1-6500*a3-17500*a1)*c5
         +(425*a4-1000*a3+1875*a2-1000*a1+16500)*e1+48*e2^4-2500*a4-3250*a3
         -12500*a2-8750*a1-100000)
         /48

の零点 [a4,a3,a2,a1] を(少なくとも一つ)求めるといった処理であり,ツールとしては,Nemo/Julia シリーズ AbstractAlgebra.jl の solve_left ( https://nemocas.github.io/AbstractAlgebra.jl/latest/matrix/#AbstractAlgebra.Generic.solve_left-Union{Tuple{T},%20Tuple{MatElem{T},MatElem{T}}}%20where%20T%3C:RingElem )

Welcome to Nemo version 0.14.1

Nemo comes with absolutely no warranty whatsoever


Welcome to 

    _    _           _        
   | |  | |         | |       
   | |__| | ___  ___| | _____ 
   |  __  |/ _ \/ __| |/ / _ \
   | |  | |  __/ (__|   <  __/
   |_|  |_|\___|\___|_|\_\___|
    
Version 0.6.2 ... 
 ... which comes with absolutely no warranty whatsoever
(c) 2015-2019 by Claus Fieker, Tommy Hofmann and Carlo Sircana


julia> MXl2=MXl[2];

julia> MX=matrix(MXl[4],MXl2,MXl2,MXl[1]);

julia> cx=matrix(MXl[4],1,MXl2,MXl[3]);

julia> @time xx=solve_left(MX,cx);
  1.407416 seconds (611.78 k allocations: 29.782 MiB, 1.75% gc time)

および,maxima の algebraic モードでの linsolve と fast_linsolve

(%i11) (map(lambda([s],tellrat(s[1])),DP),algebraic:on,linsolve(sAL1,AL0))$
Evaluation took 0.0040 seconds (0.0040 elapsed) using 1.843 MB.

(%i12) (map(lambda([s],tellrat(s[1])),DP),algebraic:on,fast_linsolve(sAL1,AL0))$
Assuming entries of type ANY-MACSYMA
Starting to solve.  There are 4 equations with 4 unknowns occurring.
The value of (SP-TYPE-OF-ENTRIES SP-MAT) is ANY-MACSYMA
The dimension of the solution space is 0
Evaluation took 0.0040 seconds (0.0040 elapsed) using 1.186 MB.

があります.

これらのうち solve_left は最近公開されたもので,高速 arithmetic で知られる Nemo シリーズゆえ相応のパフォーマンスが期待され,従来の hnf_with_transform と can_solve_left_reduced_triu の組み合わせよりは高速化していますが,サイズの大きな問題に対する処理速度は maxima の fast_linsolve が優位であり,例えば,47 分多項式を入力とする処理に現れる,文字列としてのサイズが 405801 バイト(上記の例は 1087 バイト)の方程式系の場合,

julia> @time xx=solve_left(MX,cx);
80.273864 seconds (65.62 M allocations: 31.598 GiB, 1.47% gc time)

に対し,無印の linsolve では

(%i14) (map(lambda([s],tellrat(s[1])),DP),algebraic:on,linsolve(sAL1,AL0))$
Evaluation took 458.1150 seconds (472.1600 elapsed) using 92401.623 MB.

そして,

(%i15) (map(lambda([s],tellrat(s[1])),DP),algebraic:on,fast_linsolve(sAL1,AL0))$
Assuming entries of type ANY-MACSYMA
Starting to solve.  There are 22 equations with 22 unknowns occurring.
The value of (SP-TYPE-OF-ENTRIES SP-MAT) is ANY-MACSYMA
The dimension of the solution space is 0
Evaluation took 54.8670 seconds (56.4100 elapsed) using 20716.948 MB.

となります.

位数の取得

前回も触れたように,nfsplitting の処理時間は結果の多項式の次数を第二引数として与えることで一般に短縮されます.この性質を利用するため本プログラムでは,その次数,つまり,入力多項式 f\mathbb{Q} 上の Galois 群 G の位数を,予め用意したある範囲内の全ての cycle index polynomial (https://en.wikipedia.org/wiki/Cycle_index) の中から G の cycle index polynomial Z(G) を特定することで取得しています.

置換群の cycle index polynomial とは,その群に属する元の cycle type ( https://groupprops.subwiki.org/wiki/Cycle_type_of_a_permutation ) の頻度を変数名と次数,そして係数により,一つの多変数多項式で表したもので,群の位数の逆数は(1個しかない)単位元の cycle type の頻度(対応する単項式の係数)として現れます.参照する cycle index polynomial のデータは,次数が 37 以下の f の Galois 群 を全て含む,GAP の Transitive Groups Library transgrp ( https://www.gap-system.org/Packages/transgrp.html ) から抽出したもので,その制約から次数が 38 以上の f についてはノーヒントで nfsplitting を実行しています.なお,同型でない群でも同じ cycle index polynomial を有するものが存在するため,群自体の特定には至らないことはよく目にする注意です.

実際の f から Z(G) を特定するには,前回も引用した「正の数 M 以下で f の判別式の因数ではない素数 p を法とする f の既約因子の次数型(どのような次数の因子がいくつずつあるか)の密度が,M\to+\infty のとき,G の同じ型の cycle type の頻度に収束する」という Chebotarev's density theorem を踏まえ,p が値の小さいほうから 10^3 個目の素数となる,または,単位元の cycle type が 3 回現れるまで,既約分解を繰り返し,各次数型と密度から cycle index polynomial と同じ書式の多項式を作り,用意したデータのうち,この多項式との差の係数ベクトルの l_2 ノルムが最小となるものを Z(G) としています.

以下,この処理を組み込んだ関数 nfsplitting2 と標準の nfsplitting の実行例です.

? for(i=1,30,nfsplitting2(x^i-2));
[0,1,1]
[0.03125000000,2,1]
[0.004801097394,6,1]
[0.001226218787,8,1]
[0.0008579881657,20,1]
[0.002494223903,12,1]
[0.0007927650227,42,1]
[0.002837500000,16,1]
[0.0004409526648,54,1]
[0.003434499314,40,1]
[7.133182736E-5,110,1]
[0.001070169231,48,1]
[0.0004472513280,156,1]
[0.002071109694,84,1]
[0.0006910009183,120,1]
[0.001790521626,64,1]
[0.001964397853,272,1]
[0.001106438745,108,1]
[0.0002551165675,342,1]
[0.001759224398,160,1]
[0.001657411051,252,1]
[0.0006244174148,220,1]
[0.001948888552,506,1]
[0.0008731821745,500,1]
[0.0008779652962,312,1]
[0.0003889834061,486,1]
[0.002439757082,336,1]
[0.0008391018743,812,1]
  *** nfsplitting: Warning: increasing stack size to 16000000.
time = 10,490 ms.

? for(i=1,30,nfsplitting(x^i-2));
  *** nfsplitting: Warning: increasing stack size to 16000000.
  *** nfsplitting: Warning: increasing stack size to 32000000.
  *** nfsplitting: Warning: increasing stack size to 64000000.
time = 3min, 24,135 ms.

GAP の組み込み関数 ProbabilityShapes は同じ原理で作動し,例えば

gap> ProbabilityShapes(x^16-x^15-x^14+4*x^13-3*x^12-x^11+5*x^10-7*x^9+2*x^8+4*x^7-5*x^6+5*x^5-x^4-2*x^3+2*x^2-2*x+1);time;
[ 1947 ]
111832
gap> TransitiveGroup(16,1947);
t16n1947
gap> Size(last);
7962624

のように位数を得ることも可能ですが,一般に

? galoisord(x^16-x^15-x^14+4*x^13-3*x^12-x^11+5*x^10-7*x^9+2*x^8+4*x^7-5*x^6+5*x^5-x^4-2*x^3+2*x^2-2*x+1)
time = 90 ms.
%2 = [0.006932446267,7962624,1]

のような高速処理は望めません.