本論文では，関数的プログラムに関して或る種の部分正当性を表現できる不等式の 形の表明を仕様記述の手段として許す詳細化型をCardelli and WegnerのFunに導 入する事で，仕様とプログラムとを同一の言語で記述する為の広帯域言語 Funiqを 構成し，その性質を様々な側面から検討している．
2) 2004年3月29日に慶應大学へ来られたMartin-Lofに，ITTで型付け判別式を等式判別式と 独立に扱っている理由が体系の形式的性質に基づくものか否かをお尋ねした所，「純形式的には必要な いが，等式判別式e1
=e
2
: の概念は左右両辺の式に対する型付けe1 : , e
2
:を前提としている．
従って，概念的あるいはmeaning-theoreticalには型付けの方が等式よりも基本的であるので，型付 け判別式を等式判別式とは独立なものとして導入した」との答を頂いた．
[S-ALL
F
]
C .
1
<:
1
C[t<:
1 ] .
2
<:
2
C . 8t<:1:2<:8t<:1:2
(t62FTV (C))
[S-EXIST
F
]
C . 1<:1 C[t<:1] . 2<:2
C . 9t<:
1 :
2
<:9t<:
1 :
2
(t62FTV (C))
図 3.1 F 固有の部分型関係に関する推論規則
その場合，基本的な問題として浮かび上がるのは，Funという型付き関数的プロ グラミング言語をベース言語として不等式表明に基づく詳細化型を導入し広帯域言語 を得る，という本論文での広帯域言語の構成方法が様々なベース言語に適用できる一 般的な方法なのか，それとも，ベース言語がFunという特定の言語のみでしか通用 しない普遍性に欠ける方法に過ぎないのか，という事である．
本節では，3.2節での保存性拡大定理の証明を再検討し，本論文での詳細化型の導 入による広帯域言語の構成方法がベースの型付き関数的プログラミング言語を選ばな い一般性の高い方法だという事を幾つかの例を用いて示す．
最初の具体例として，一見しただけではFunと非常に良く似ているが型の体系が 持つ性質がFunとは全く異なる型理論に対して，本論文での詳細化型による拡張を 試みる．その体系とはCurien and Ghelli (1991, 1992)でのF（\F sub"と読む）
という型理論である（以下，その言語も F と呼ぶ）．Cardelli, Martini, Mitchell
andScedrov(1991)での類似の体系F<: も本節の議論の範囲ではF と等価である．
言語としてのF はFunと全く同じである．即ち，図2.1で\(*)"が付いていな い生成規則のみを用いて生成される言語である（オリジナルのF には，オリジナル のFunと同様，不動点再帰式は存在せず，またレコード型や可変型も含まないが，
ここでは追加されているものとして扱う．但し，それらの追加は本節の議論には全く 影響しないので，それらの構文がないと考えても一向に差し支えない）．
さて，その型システムを定式化した型理論としてのFは判別式の種類と形式に関 してはFUNと全く異ならない．即ち，判別式に関しては部分型と型付けとの2種類 があり，型付け判別式での実現変数に対する型付け基底は空でなければならない．
また，型付けに関する公理と推論規則に関してもFはFUNと全く同一である．
即ち，図 2.3で\(*)"が付いていないものである．
FUNのそれら|図2.3で\(*)"が付いていないもの|の中から多相型と抽象型と に関する[S-ALL] と[S-EXIST]を除き，代わりに，上の図 3.1に示した二つの推論 規則[S-ALLF
]と[S-EXISTF
]とを加えたのがFの部分型関係に関する規則群で ある．[S-ALLF
]と[S-ALL]との違いは，多相型同士の部分型関係に於いて束縛型
変数の上限の型の間に部分型関係を許すか上限の型は同一な場合に限るか，という点 である．[S-EXISTF
]と[S-EXIST]との違いも同様である（但し，前提での上限の
型1 と1 との間の部分型関係の向きが[S-ALLF
]とは逆）．
以上のF とFUNとの違いは，一見しただけでは非常に些細な差に過ぎない．し かも部分型に関する新しい推論規則の[S-ALLF
]と[S-EXISTF
]とでの上限の型
1
;
1間の部分型関係を許す事は，その直感的意味からは極めて自然である．
しかし， Pierce (1992)が証明した通り，型理論F は決定不能な体系である．
Howard (1969)の「命題 = 型」的観点からは，F がFUNIQの詳細化型の如き述 語論理レベル相当の内容を一切含まず内容的には命題論理レベルの型の体系に過ぎぬ 事を考えれば驚くべき性質である．この事は，言語としてはF はFunと同一であ るにも拘らず，型理論としてのFはFUNとは全く異質である事を示している．
そこで，FUNとは非常に性質の違うF に詳細化型を導入した型理論|FUNに 対するFUNIQ相当のもの|を考え，FIQ
と呼ぶ．言語としてのFiq
はFuniqと同 一である．型理論としてのFIQ
は，判別式の種類と形式に関してはFUNIQと同一 であり，公理／推論規則については図 2.2 図2.4 での FUNIQの規則の中で，
[S-ALL]と[S-EXIST]とを，各々，[S-ALLF
]と[S-EXISTF
]とに差し替えて得ら れる．この時，次の定理が成立する．
定理 3.26（保存的拡大定理|FIQ
版）
型理論FIQ はその部分型理論F の保存的拡大である．即ち，FIQ の任意の 表明無し判別式6に対して，
j0
F IQ
6 () j0
F
6:
[T-TABS
FB ]
C[t<:];0;1 . e:
C ;0;1 . (3t<::e):8t<::
(t62FTV (C ;0;1))
[A-TABS
FB ]
C[t<:];0;1. e6e 0
:
C ;0;1 . (3t<::e)6(3t<::e 0
):8t<::
(t62FTV (C ;0;1))
図 3.2 F-限定Fun特有の型付け規則とF-限定Funiq特有の表明規則
この証明は，3.2節での系 3.22の証明と全く同一である．つまり，FUNとは全 く性質の異なる型理論F に対してもFUNに対する拡張と同じ様に詳細化型を導入 できる事が，この定理から理解できる．
以上のF に対する詳細化型の導入が保存的拡大性を保つ事は，型理論としての
F
はFUNとは全く性質が異なるとは言えどもベースの言語がFunと同一であった ので当然と感じるかも知れない．そこで，次はベースの言語自体がFunとは異なる 場合を取り上げる．
新しいベース言語はF-限定Funという言語3)である．この言語はFunの多相型で の全称限量化8の上限型にCanning,Cook,Hill,OrthoandMitchell(1989)で提案 されているF-限定という形の拡張を導入した4) 2階の型付き-計算の体系である．
この拡張されたF-限定Funという言語は，BNFの生成規則として表現可能な文 脈自由言語としては図 2.1で定まるFunと同一であるが，実際に良形と認められる ストリングの集合としての言語としてはFunとは異なっている．その違いは図3.2 に示した型付け規則で表わされている．同図の[T-TABSFB]が図 2.3でのFunオリ
ジナルの[T-TABS]と異なる点は，束縛対象となる型変数tに関する制約条件である．
オリジナルの[T-TABS]では束縛対象の型変数tはそれに対する上限型中に自由 に現れる事が許されないのに対して，[T-TABSFB]ではt 2FTV()である事が許
3) これもFunのバリエーションに過ぎないではないか，と思われるかも知れないが，Funが2階 の型付き-計算の体系として充分に一般的で豊かな言語機能を提供しているので，2階の型付き-計 算の体系への詳細化型の導入に関して議論しようとする以上，Funやそのバリエーションがベース言 語となるのは必然的である．
4) 全くの形式的な立場からは抽象型での存在限量化9の方も同じ形で拡張して良いと思われるが，
存在限量化でのF-限定の計算機科学的な意義は全く不明である|Canning達の論文でも9での上限 型に対するF-限定化は全く検討されていない|ので，ここでは，Canning達の原論文通り，8の 上限型に対してのみF-限定による拡張を考える．
由に出現可能だという事を強調する為に，F[t]|ここで，F[t]はtを含み得る型の 表式|という形で書き表わす．これが\F-限定"という名称の由来である．
この型変数の出現に関する違いは，実用的に見ると非常に大きな差をもたらす．
実際，上のCanning達の論文では，Funでは充分には成功しなかったオブジェクト 指向での継承を2階の型付き-計算での部分型関係として捉える事に関して，この
F-限定による拡張だけで相当な成功を収めた．
そこで，図3.2の[T-TABSFB]則で[T-TABS]則を置き換えて定まるF-限定Fun の為の型理論を F-限定 FUN と呼ぶ事とし，詳細化型を導入した言語をF-限定
Funiq，その型理論として，FUNIQの[A-TABS]則を図 3.2の[A-TABSFB
]則に変 更したものをF-限定FUNIQと呼ぶ．やはりこの場合も，次の保存的拡大定理が成 立する．
定理 3.27（保存的拡大定理|F-限定FUNIQ版）
型理論F-限定FUNIQはその部分型理論F-限定FUNの保存的拡大である．
即ち，F-限定FUNIQの任意の表明無し判別式6に対して，
j0
F-限定FUNIQ 6 () j0F-限定FUN 6:
この証明も系 3.22の証明と全く同一である．
上で参照したCanning達の論文にもある通り，実は，F-限定という言語拡張は，
少なくとも直感的な意味では再帰型の概念を隠れた形で言語の中に導入した事に相当 する．そこで，詳細化型の導入の具体的な事例の最後として，再帰型をコッソリとで はなく堂々とベース言語に導入する5)場合を考える．
5) 但し，意味論的には詳細化型を含む再帰型は大いなる問題を生じ，第5章で述べる通り，詳細化 型を含む再帰型に対して表示的意味を与える事は未解決である．本節では，あくまでも詳細化型の証明 論的な側面のみを議論している．
::=:::
j t: 再帰型．
図 3.3 FunnYの再帰型の構文
[T-FOLD]
C ;0;1 . e:[t:=t:]
C ;0;1 . e:t:
[T-UNFOLD]
C ;0;1 . e:t:
C ;0;1 . e:[t:=t:]
[A-FOLD]
C ;0;1 . e6e 0
:[t:=t:]
C ;0;1 . e6e 0
:t:
[A-UNFOLD]
C ;0;1 . e6e 0
:t:
C ;0;1 . e6e 0
:[t:=t:]
図 3.4 FUNNY特有の型付け規則とFUNIQY特有の表明規則
型に関する再帰的定義を許す言語FunnYは図 3.3に示す型に関する不動点演算子 の形6)として再帰型をFunに追加したものである．この言語の型理論FUNNY は，
FUNに図 3.4に示した[T-FOLD]則と [T-UNFOLD]則とを追加したものとする．
なお，再帰型に関しては部分型関係に関する推論規則は存在しない．
なお，Funや同系統の2階の型付き-計算の体系に再帰型を導入する場合の推論 規則に関しては幾つかの選択肢が存在する．そこで，再帰型の為の推論規則の代表的 な選択肢に関して，簡単に纏めておく．
まず第一の選択肢としては，再帰型に対する型付け規則の選び方である．上の 図 3.4に示した規則はCardone (1989, 1991)で与えられたものであるが，これらの 代わりに，再帰型の定式化に於いて，式にfoldeとunfoldeという二つの構文を追
6) 但し，型に関しては式での関数抽象に相当する型変数を束縛する構文がないので，再帰型の構文 自身で不動点としての再帰型を表わす型変数tを束縛せねばならない．