型解析：型ユニフィケーションの分類結果と処理順番

左側分類と右側分類の番号が微妙にずれてしまった。が、もう直すのが手間だから、ずれた番号をそのまま使うことにする。

ちと不恰好だが、もう勘弁してくれ。これで一応の結果としたい（間違いが発見されなければ）。後で元気があるときに、番号付けと順番を再考するかもしれない。

左側分類

1. never
2. any
3. LIT
4. SCA
5. [,]
6. {,}
7. @
8. x (var)
9. ?
10. join

右側分類

1. never
2. any
3. LIT
4. SCA
5. [,]
6. {,}
7. @
8. ? （ここでずれた、変数が最後になっている）
9. xunion
10. &
11. y (var)

順番

10*11 = 110 の欄を持つマトリックスを、次の順番で塗りつぶす（網羅する）。この順番が絶対というわけではないし、効率は考えてない。が、とりあえず「うまくいく」であろう順番。

順番	左側	右側	分類番号	事後処理
1	join	-	10*[1-11]	進行=>join
2	never	-	1*[1-11]	成功終了
3	-	never	[2-9]*1	完全失敗終了
4	-	&	[2-9]*10	条件出力 and 進行=>inter
5	?	?	9*8	進行=>b-opt
6	-	?	[2-8]*8	進行=>r-opt
7	?	-	9*[2-7,9,11]	条件出力 and 進行=>l-opt
8	-	any	[2-8]*2	判定 or 条件出力(8*2)
9	any	-	2*[3-7,9,11]	条件出力
10	-	y	[3-8]*11	条件出力
11	x	-	8*[3-7,9]	条件出力
12	-	xunion	[3-7]*9	完全失敗 or 進行=>xunion
13	LIT	-	3*[3-7]	判定
14	SCA	-	4*[3-7]	判定
15	[,]	-	5*[3-7]	進行=>array
16	{,}	-	6*[3-7]	進行=>object
17	@	-	7*[3-7]	完全失敗 or 進行=>tag

構文的な正規化により、ユニフィケーションの左側（プロファイルの右側）では、∪を項の一番外側に移動できることもある。具体的には、Caty式にeachが含まれてなければ、∪を一番外まで移動できる。

∪を外に出せることはおおむね次のようにして分かる： never, any, LIT = {スカラーリテラルの全体}, SCA = {integer, number, string, boolean}, Var = {変数の全体} として、これらをベースにして、次の項構成子（コンストラクタ）によって、帰納的に項を定義する。

1. [-, ..., -*] （配列の構成）
2. {α₁:-, ..., *:-}　（オブジェクトの構成）
3. @α - （タギング）
4. -? （オプショナル）
5. -∪- （合併／ジョイン）

次の公式が示せる。

1. [A∪B, ..., X*] = [A, ..., X*]∪[B, ..., X*]
2. {α₁:A∪B, ..., *:X} = {α₁:A, ..., *:X} ∪ {α₁:B, ..., *:X}
3. @α (A∪B) = (@α A) ∪ (@α B)
4. (A∪B)? = A?∪B?

ただし、eachが入ると、(A∪B)* = A*∪B* とはならないのでうまくいかない。次は成立しない。

1. {α₁:A, ..., *:(X∪Y)} = {α₁:A, ..., *:X} ∪ {α₁:B, ..., *:Y}
2. [A, ..., (X∪Y)*] = [A, ..., X*]∪[A, ..., Y*]

また、次に事実にも注意する必要がある。

• (A∪B)? = A?∪B = A∪B? = A?∪B?

これを使うと、∪を外に出すか、?を外に出すかを選べる。結論を言うと、?を外に出さないと、後の処理がうまくいかない。

型解析：ユニフィケーションの進行と成功／完全失敗

証明ターゲット S⊆T が完全失敗とは、S∩T = never が証明できてしまうこと。以下、S∩T = never を、S⊥T を書くことにする。

• S⊆T が成功 ⇔ S⊆T が成立（健全性より）
• S⊆T が完全失敗 ⇔ S⊥T が成立
• S⊆T が条件付きで成功 ⇔ S⊆T は成立しない（その意味では失敗）が、S⊥T ではない。

トップダウン・ユニフィケーションのとある過程（実行の途中）で成功／完全失敗したとき、その成功／完全失敗が、より上位に伝搬していく状況は以下のとおりである。

1. joinのすべての成分で成功すれば、そのjoinは成功。joinのすべての成分で完全失敗すれば、そのjoinは完全失敗。その他は成功でも完全失敗でもない。
2. interの進行先で成功しても完全失敗しても、inter全体は成功も完全失敗もしない。なぜなら、interは必ず変数を含むから。
3. b-optの進行先で成功すれば成功。b-optの進行先で完全失敗してもb-optは完全失敗しない。条件 not_exist が残る。
4. r-optの進行先で成功すれば成功。r-optの進行先で完全失敗すればr-optは完全失敗。
5. l-optの進行先で成功しても成功ではない。l-optの進行先で完全失敗すればr-optは完全失敗。
6. xunionの進行先で成功すれば成功。xunionの進行先で完全失敗すれば完全失敗。
7. arrayのすべての進行先で成功すれば成功。arrayの進行先のひとつで完全失敗すればarrayが完全失敗。
8. objectのすべての進行先で成功すれば成功。objectの進行先のひとつで完全失敗すればobjectが完全失敗。
9. tagの進行先で成功すれば成功。tagの進行先で完全失敗すればtagが完全失敗。

完全失敗に注目すると：

1. joinのすべての成分で完全失敗すれば、そのjoinは完全失敗。ALL条件
2. （interは完全失敗しない。）
3. （b-optは完全失敗しない。）
4. r-optの進行先で完全失敗すればr-optは完全失敗。
5. l-optの進行先で完全失敗すればr-optは完全失敗。
6. xunionの進行先で完全失敗すれば完全失敗。
7. arrayの進行先のひとつで完全失敗すればarrayが完全失敗。SOME条件
8. objectの進行先のひとつで完全失敗すればobjectが完全失敗。SOME条件
9. tagの進行先で完全失敗すればtagが完全失敗。

join(ALL), r-opt, l-opt, xunion, array(SOME), object(SOME), tagの7つのケースで、ボトムアップに完全失敗の可能性がある。