GALで量化子∀(任意の~)と∃(ある~)を用いて、表記をすることができます。
ただし、この場合、そこで扱われる変項は、いわばループして
該当の強度空間から要素として取り出される、と考えられます。
そこで、∀記号,∃記号を使用した表記を、
ループ表記と呼称します。
では、ループ表記の記述形式について、説明しましょう。
それは、以下のようなものです。
∀x.(x∈P)⇒f(x)
ここで、
∀：∀記号(任意の~)
x：変項
P：強度空間
f：関数
であり、｢任意のPに属する要素について、
fさせる｣と解釈されます。
また、
∃x.[x∈P].f(x)
ここで、
∃：∃記号(ある~)
x：変項
P：強度空間
f：関数
であり、｢あるPに属する要素について、
fさせる｣と解釈されます。
または配列の添え字(インデクサ)のような表記も可能です。
∀x.(x<=<N)⇒f(A[x])
ここで、
∀：∀記号(任意の~)
x：変項
N：数値を表す強度空間
A：グループを表す強度空間
f：関数
であり、｢任意のN以下番目のAの要素について、
fさせる｣と解釈されます。
また、
∃x.[x<=<N].f(A[x])
ここで、
∃：∃記号(ある~)
x：変項
N：数値を表す強度空間
A：グループを表す強度空間
f：関数
であり、｢あるN以下番目のAの要素について、
fさせる｣と解釈されます。
つまり、まず量化された変項を示し、
次に束縛変項の動く範囲の条件を示し、
最後に、条件に合致した場合の挙動を記述する、
というわけです。
その際に、∀記号に対し⇒記号,
∃記号に対し∧記号(さらにGAL風な記述で表現しています)を
使用しています。
勿論、上記の表記ではxが数詞の変項だと判別できるために、
A[x]で表記可能であり、その判別がつかない場合、
｢~番目｣を表すとすれば[~x~]と記述します。
さらに、ループ表記では、述語論理同様に、
多重量化を表記することもできます。
∀x∃y
∃x∀y
特に、以下の場合は、省略形を表記できます。
∀x∀y ⇒省略形: ∀xy
∃x∃y ⇒省略形: ∃xy
では、例として以下にクイックソートについて、
ループ表記してみましょう。
ただし、理解し易い様に、
ここではさらに、λ表記、世界表記、[]表記、{}表記や
インデントによるブロック記述も併用して見ます。
まず、ここでの記号として、以下を事前に定義しておきます。
｢A:=B｣AにBを代入する。
｢A++｣Aに1を足し、当該値を再度Aに代入する。
λQS(処理対象配列,左端開始位置,右端終了位置)
@λQSxlr⊃
i:=l
j:=r
pv=[get†(x.中央値)]T
@∀ij.{↓z}⇒
・(∀i.(x[i] << pv) ⇒ i++) ≡ (srch([pv <=<](x[i])))
・(∀j.(pv << x[j]) ⇒ j--) ≡ (srch([pv >=>](x[j])))
・i << j
swap({x[i],x[j]})
i++
j--
(l << i-1) ⇒ λQS(x,l,i-1)
(j+1 << r) ⇒ λQS(x,j+1,r)
ただし、｢∀ij｣は｢<i,j>λij.∀ij｣の省略形です。
この記述については、後を参照してください。
ここで、束縛変項の動く範囲の条件を以下のように分割して記述できます。
・束縛変項の動く範囲
・挙動に対する条件
それは、挙動に対する条件は元の位置のままで、
束縛変項の動く範囲をλ表記で書き換えます。
SQLのSELECT文をご存知であれば、以下のような記述となります。
例えば
SELECT * FROM tab1 WHERE a=1
に対しては
∀x.{↓z}⇒otpt(*)
otpt:出力させる
・x∈tab1
・(x.a)=1
と記述されるところで、
テーブルとwhere句の条件を以下のように分割します。
<↓>λx.∀x.((x.a)=1)⇒otpt(*)
・x∈tab1
これで、tab1のレコードxにおいて、
全てのa列に1があるレコードxは、
全列情報を表示する、と表記されます。
同様に、クイックソートも以下のように変更されます。
さらに加筆もします。
λQS(処理対象配列,左端開始位置,右端終了位置)
@λQSxlr⊃
(i.初期値):=l
(j.初期値):=r
pv=[get†(x.中央値)]T
<↓z>λij.@∀ij.i << j⇒
・(∀i.(x[i] << pv) ⇒ i++) ≡ (srch([pv <=<](x[i])))
・(∀j.(pv << x[j]) ⇒ j--) ≡ (srch([pv >=>](x[j])))
swap({x[i],x[j]})
i++
j--
(l << i-1) ⇒ λQS(x,l,i-1)
(j+1 << r) ⇒ λQS(x,j+1,r)
こうしてクイックソートが記述できましたので、
以下の数列を具体例として、該当の記述を説明します。
2349156087
これが、λQS(処理対象配列,左端開始位置,右端終了位置)における
｢処理対象配列｣となります。
ここではコンピュータ言語っぽく表記して
｢λQS(処理対象配列,左端開始位置,右端終了位置)｣ですが、
GALは日常言語の記述であり、この関数が表現したいのは、
ソート結果としての｢処理対象配列｣なので、
本当は、｢[λQS(,左端開始位置,右端終了位置)]処理対象配列｣と
記述するべきです。
この時、｢左端開始位置｣は1で、｢右端終了位置｣は10です。
λ表記の世界表記で、｢@λQSxlr⊃｣とすることで、
｢処理対象配列｣,｢左端開始位置｣,｢右端終了位置｣をそれぞれ
変項x,l,rに代入しているわけです。
さらに、｢(i.初期値):=l｣などで、i,jの初期値として代入します。
この時、iはインデクサですから、
ここで｢i=Indexer｣と丁寧な表記もいいかもしれません。
ここでxの真ん中辺りの数値として(中央値)、pv=9とします。
9:2349156087
と表記します。
ここで、ループ表記が世界表記としてブロックで記述されています。
まず、各インデクサは配列の添え字として何番目の数値かを指摘します。
それがpv以下や以上の場合、動くことになります。
｢∀i.(x[i] << pv) ⇒ i++｣の箇所です。
これは結局、｢srch([pv <=<](x[i]))｣のこととなるわけです。
つまり、
左端からはpv9以上の値、右端からpv9以下の値を探します。
すると
・{9,7}
を交換することが判明します。
それが｢i << j⇒swap({x[i],x[j]})｣です。
9:2349156087
S:i________j
E:___i_____j
9:2347156089
そして、元の場所の１つ内側から探索を再開します。
｢i++｣,｢j--｣がそれにあたります。
すると、
・{8,9}
が見つかりますが、｢i << j｣の条件をクリアしないので、
ループがこれ以上、進みません。
それは条件をクリアしないために、｢i++｣,｢j--｣に到達しないからです。
一方、同じくインデクサを動かす
｢(∀i.(x[i] << pv) ⇒ i++)｣,｢(∀j.(pv << x[j]) ⇒ j--)｣の挙動は、
既に終了していることも上記の表記から判明します。
つまり、1回目のクイックソートが終わっていることになるのです。
9:2347156089
S:____i___j
E:________ji
D:234715608/9
すると8の右端で再帰関数を呼び出す分割が起こります。
これが、以下の記述です。
・(l << i-1) ⇒ λQS(x,l,i-1)
・(j+1 << r) ⇒ λQS(x,j+1,r)
これで、上記｢E:________ji｣に対し、
同一箇所｢i-1｣,｢j+1｣で分割していることが分かります。
したがって、要素が１つで交換対象がないため、
再帰的な関数呼び出しがない9の位置は確定されます。
これが、｢(j+1 << r)｣の記述になります。
次は、｢234715608｣で再帰的に考えます。
これが、｢λQS(x,l,i-1)｣の記述です。
ここでxの真ん中辺りの数値として(中央値)、pv=1とします。
1:234715608/9
左端からは1以上の値、右端から1以下の値を探します。
以下の箇所です。
・｢∀i.(x[i] << pv) ⇒ i++｣
・｢∀j.(pv << x[j]) ⇒ j--｣
後は同様ですね。
すると
・{2,0}
を交換することが判明します。
1:234715608/9
S:i_______j
E:i______j
1:034715628/9
そして、元の場所の１つ内側から探索を再開しますと、
・{3,1}
を交換することが判明します。
1:034715628/9
S:_i____j
E:_i__j
1:014735628/9
そして、元の場所の１つ内側から探索を再開しますと、
・{1,4}
が見つかりますが、｢i << j｣の条件をクリアしないので、
ループがこれ以上、進まないことになります。
つまり、2回目のクイックソートが終わります。
1:014735628/9
S:__i__j
E:_ji
D:01/4735628/9
すると1の右端で再帰関数を呼び出す分割が起こります。
次は、｢01｣と｢4735628｣で考えます。
｢01｣側が次のクリックソートで確定されます。
説明を割愛します。
次は、｢4735628｣で考えます。
ここでpv=5とします。
01/5:4735628/9
左端からは5以上の値、右端から5以下の値を探します。
すると
・{7,2}
を交換することが判明します。
01/5:4735628/9
___S:i_____j
___E:_i___j
01/5:4235678/9
そして、元の場所の１つ内側から探索を再開しますと、
・{5,5}
が見つかりますが、｢i << j｣の条件をクリアしないので、
ループがこれ以上、進まないことになります。
つまり、3回目のクイックソートが終わります。
01/5:4235678/9
___S:__i_j
___E:___i
01/D:423/5/678/9
ここで、5の両端で再帰関数を呼び出す分割が起こります。
記述ではこの箇所です。
・(l << i-1) ⇒ λQS(x,l,i-1)
・(j+1 << r) ⇒ λQS(x,j+1,r)
次は、｢423｣と｢678｣で考えます。
｢678｣側が次のクリックソートで確定されます。
説明を割愛します。
次は、｢423｣で考えます。
ここでpv=2とします。
01/2:423/5/678/9
左端からは2以上の値、右端から2以下の値を探します。
すると
・{4,2}
を交換することが判明します。
01/2:423/5/678/9
___S:i_j
___E:ij
01/2:243/5/678/9
そして、元の場所の１つ内側から探索を再開しますと、
ijがjiとなりそこで、｢i << j｣の条件をクリアしないので、
ループがこれ以上、進まないことになります。
つまり、4回目のクイックソートが終わります。
01/2:243/5/678/9
___S:ji
___E:ji
01/D:2/43/5/678/9
すると2の右端で再帰関数を呼び出す分割が起こります。
したがって、要素が１つで交換対象がないため、
再帰的な関数呼び出しがない2の位置は確定されます。
次は、｢43｣で考えます。
ここでpv=4とします。
01/2/4:43/5/678/9
左端からは4以上の値、右端から4以下の値を探します。
すると
・{4,3}
を交換することが判明します。
01/2/4:43/5/678/9
_____S:ij
_____E:ij
01/2/4:34/5/678/9
そして、元の場所の１つ内側から探索を再開しますと、
ijがjiとなりそこで、｢i << j｣の条件をクリアしないので、
ループがこれ以上、進まないことになります。
つまり、5回目のクイックソートが終わります。
01/2/4:34/5/678/9
_____S:ji
_____E:ji
01/2/D:3/4/5/678/9
すると2の右端で再帰関数を呼び出す分割が起こりますが、
次は要素が1つずつのため、再帰関数は呼び出されず、
ここで全てのクイックソートが終わります。
01/2/3/4/5/678/9
確かに、ループ表記でクリックソートは記述されているようです。