このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

高階関数を持たないが型の順序を持つラムダ計算

雑記／備忘

ラムダ計算の強力さの理由（のひとつ）は、任意の高階関数が定義可能なことでしょう。しかし、1階の関数があれば高階関数は必要ない状況もあります。α、βがデータ型だとして、関数の型 α->β は必要だが、(α->β)->γ なんてのは要らない、って設定です。

これから“値”と“1階の関数”を持つが、高階関数は持たない型付きラムダ計算を考えます。高階関数があるときは、α->(β->γ) により、「2引数の関数の型 (α, β)->γ」を代用できます（カリー化）が、高階関数がないとそうはいかないので、最初から複数の引数を許しておきます。引数の型は (α1, α2, ..., αn) であり、戻り値の型がβである関数の型が、(α1, α2, ..., αn)=>β と書くことにします。イコールを使い太い矢印にしたのは、「これ以上は矢印を使えないぞ」ということを暗示するためです。

さて、今回考える型付きラムダ計算は、型のあいだに順序関係があるとします。多くの型システムは型階層（type hierarchy）を持つので、この仮定は自然だと思います。型階層があって任意の高階関数を許すとハナシがややこしくなるので、型階層（順序構造）あり／高階関数なしの状況で考えよう、というわけです。

内容：

  1. 型の順序集合
  2. 構文的な素材と型付け
  3. 項の構成規則
  4. 項の型付けのまとめ
  5. ユーザー定義関数の導入
  6. let式
  7. その他もろもろのこと

型の順序集合

型の集合をTとします。「型とはなんぞや」という問題は棚上げします。構文的な型表現（type expression）を型だと思っても、意味論的なデータ領域（data domain）を型だと思っても、どっちでもいいです*1。集合Tの要素、つまり型をα、βなどのギリシャ小文字で表します。

Tは単なる集合ではなくて、順序関係⊆が入っているとします。任意の α, β∈T に対して、α⊆β かどうかが定まっています。ただし、順序⊆は線形順序（全順序）とは限りません。α⊆β も β⊆α も成立しない（真とはならない）可能性があります。

α1, α2, ..., αn, β∈T に対して、(α1, α2, ..., αn)=>β という形の複合記号の全体を Tn=>T とします。特に、()=>β の全体が T0=>T 、(α)=>β の全体が T1=>T です。

n≠m のとき Tn=>T と Tm=>T は共通部分がないので、(T0=>T) + (T1=>T) + (T2=>T) + ... という無限直和を作ることができます。この無限直和を Σk(Tk=>T) あるいはより短く T*=>T と書き表すことにします。

Tに順序がある前提で、T*=>T に順序を入れることができます。n≠m のとき、((α1, α2, ..., αn)=>β)∈(Tn=>T) と ((α1, α2, ..., αm)=>β)∈(Tm=>T) のあいだに順序関係はない（比較不能）とします。同じ“形状”をした (α1, α2, ..., αn)=>β と (α1', α2', ..., αn')=>β' のあいだでは次のように順序を定義します。

((α1, α2, ..., αn)=>β)⊆((α1', α2', ..., αn')=>β') であるとは：

  1. α1'⊆α1, α2'⊆α2, ..., αn'⊆αn がすべて成立する。
  2. β⊆β'

αi⊆αi' ではないので十分注意してください。引数型に関しては反変、戻り値型に関しては共変になっているのです。この定義が、実際に T*=>T 上の順序関係になることは練習問題として確認してみてください。今定義した T*=>T 上の順序はすごく便利ですよ、知っていると使う機会があると思います。

構文的な素材と型付け

ラムダ計算の項（term）を組み立てるために、素材となる記号の集合を準備します。

  1. 定数記号の集合 Const。集合Constの要素は a, b, c などとします。
  2. 変数記号の集合 Var。集合Varの要素は x, y, z などとします。
  3. 関数記号の集合 Func。集合Funcの要素は f, g, h などとします。

型付きラムダ計算を考えるので、記号に型を割り当てます。typeConst:Const→T、typeFunc:Func→(T*->T) は前もって与えられているとします。でも、Varには事前の型付けをしません。変数への型の割り当ては文脈ごとにします。

その文脈を型コンテキストと呼びましょう。具体的には、Varの部分集合V上で定義されたT値関数が型コンテキストです。型コンテキストを大文字 A, B, C などで表すことにします*2。V⊆Var で、A:V→T のとき、Aの域であるVを|A|と書くことにします。したがって、A:|A|→T 。Aは写像なので、x∈|A| に対して A(x) という書き方が許されますが、混乱しがちなので、type(A, x) と書くことにします。A(-) と type(A, -) は同じ意味です。

変数と型のペア x:α （x∈Var, α∈T）を型注釈と呼びます。変数（の名前）が重複しない型注釈の集合 {x1:α1, x2:α2, ..., xn:αn} を考えると、これは {x1, x2, ..., xn} 上で定義された型コンテキストを定義します。以後、変数名が重複しない型注釈の集合と型コンテキストを区別しないことにします。

変数名が重複しない型注釈のリスト（タプル） (x1:α1, x2:α2, ..., xn:αn) をラムダリストと呼びます。ラムダ束縛（ラムダ抽象）に使う心積もりがあるからです。ラムダリストと型コンテキストはよく似てますが、ラムダリストには変数の並び順がある点が異なります。

Xがラムダリストのとき、Xから自然に定義される型コンテキストを TC[X] と書くことにします。X := (x1:α1, x2:α2, ..., xn:αn) のとき、TC[X] = {x1:α1, x2:α2, ..., xn:αn} です。TC[-]は、並び序を忘れるだけの写像です。

項の構成規則

項と関数項は次のように定義します。項／関数項の構成と共にその型の定義も一緒にします。

  1. 定数記号は項である。定数記号aの型は、typeConst(a) で与えられる。
  2. 変数記号は項である。変数記号xの型は、型コンテキストAのもとで、type(A, x) で与えられる。
  3. fが、型が (α1, ..., αn)=>β の関数記号のとき、fは同じ型の関数項である。
  4. (x1:α1, ..., xn:αn) がラムダリスト、Eが型βの項のとき、後で述べる条件を満たすなら、λ(x1:α1, ..., xn:αn).E は、型が (α1, ..., αn)=>β の関数項である。
  5. Fが、型 (α1, ..., αn)=>β の関数項で、E1, ..., En が項のとき、後で述べる条件を満たすなら、F・(E1, ..., En) は型βの項である。

λ(x1:α1, ..., xn:αn).E はラムダ抽象（あるいは単に抽象）、F・(E1, ..., En) は適用と呼びます。適用のナカグロ記号「・」は冗長ですが、適用を表す演算子を明示的に表しています。

ラムダ抽象と適用を構成するときの条件を述べましょう。そのためには、自由変数の概念が必要です。項Eに対して、Eの自由変数の集合 FV[E] を次のように定義します。

  1. FV[a] = {} when a∈Const
  2. FV[x] = {x} when x∈Var
  3. FV[f] = {} when f∈Func
  4. FV[λ(x1:α1, ..., xn:αn).E] = FV[E]＼{x1, ..., xn} （記号「＼」は集合差）
  5. FV[F・(E1, ..., En)] = FV[F]∪FV[E1]∪...∪FV[En]

ここで注意すべきは、ラムダ抽象によって、そのラムダリスト（ラムダ束縛するパラメータのリスト）に出現する変数は自由変数ではなくなることです。

では、ラムダ抽象を構成するときの条件を述べます； 変数の型付けは型コンテキストで与えられるので、型コンテキストAのもとで考えることにします。ラムダ束縛に使うラムダリストを X := (x1:α1, ..., xn:αn) として、TC[X] は対応する型コンテキストだとします。|TC[X]| = {x1, ..., xn} ですね。この記号法のもとで、次が目的の条件となります。

  • x∈|TC[X]| かつ x∈FV[E] ならば、type(TC[X], x)⊆type(A, x)

変数xは、ラムダリストに登場するEの自由変数です（それが「ならば」の前の部分）。ですから、変数xに関して実際の束縛が生じます。この束縛の際に、ラムダリスト（束縛するパラメータのリスト）で宣言された型と、前もって型コンテキストAにより決められた変数の型が整合することが条件となります。

さらに、適用 F・(E1, ..., En) を構成するときの条件は次のようになります。Fの型は (α1, ..., αn)=>β だとして：

  • (Ei の型)⊆αi （i = 1, 2, ..., n）

この条件も、置換（substitution）のときの型の整合性を主張しています。

項の型付けのまとめ

項を構成するときに、条件をチェックしながら組み立てれば、項の型付けは単純な規則になります。Aは型コンテキストとします。

  1. 定数記号aの型は、typeConst(a) 。
  2. 変数記号xの型は、type(A, x) 。
  3. 関数記号fの型は、typeFunc(f) 。
  4. ラムダ抽象 λ(x1:α1, ..., xn:αn).E の型は、Eの型をβとして (α1, ..., αn)=>β 。
  5. 適用 F・(E1, ..., En) は型は、Fの型を (α1, ..., αn)=>β としてβ。

この型付けでは、値の型αと関数の型 ()=>α が別物として登場します。この2つの型は同一視してもいいものなので、2つとも扱うのは冗長ですが、現実には定数と引数0の関数を別物にすることもあるので、このまま別扱いとしておきます（ちょっとカッコワルイですけど）。

ユーザー定義関数の導入

集合Constに属する記号は決まった値を表すものです。、当然に前もって型も決まっています。それに対して集合Varに属する記号は、値も型も後から決める用途に使います。集合Funcに属する記号は前もって型が決まっていたので、いわば“組み込み関数”の記号です。後から決めるられる関数記号、つまりユーザー定義関数のための記号がありませんでした。そこで、ユーザー定義関数のための記号の集合FVarを導入します。FVarの要素を関数変数（の記号）と呼びます。

u∈FVarに対して、u:(α)=>β のような関数型注釈を使うことになります。型コンテキストには、関数型注釈を入れてもいいとします。Aが型コンテキストであるとき、A:(V + W)→(T + T*=>T) とみなせます。ここで、V⊆Var、W⊆FVar です。

ユーザー定義関数を入れても、ラムダ項全体の構成方法は特に変わりません。

let式

ラムダ計算のなかに、通常の代入文に近い構文を導入しましょう。let式です。代入文（代入式、割り当て式）は、x = E または u = F の形です。xは変数（x∈Var）、uは関数変数（u∈FVar）です。let式の全体は次の形になります。

  • let 代入文の並び in 項／関数項

代入文*3を構成するときも型の制約が入ります。Aが与えられた型コンテキストだとして、次の2つの場合を考えます。

  1. 代入文の左辺の変数はAに含まれる。
  2. 代入文の左辺の変数はAに含まれない。

二番目のケースのとき、その変数は（型コンテキストAに対して）フレッシュだといいます。

変数に限らず、任意の項Eに対して type(A, E) を、型コンテキストAに対する型付けの結果とします。関数項Fであっても type(A, F) を定義できます。ただし、フレッシュな変数などは型が決められないので、type(A, -)は部分関数となります。type(A, -) の値の領域は、T + (T*=>T) です。

代入文を構成する際の型に関する条件は次のようになります。

  • type(A, 左辺) ⊆ type(A, 右辺)

順序関係⊆は、関数型も含めた T + (T*=>T) 上て定義されているので、この不等式は意味を持ちます。

左辺がフレッシュ変数であるときは特に条件はありませんが、値の項はVarの変数に、関数項はFVarの変数に代入する、という制限はあります。

let式に出現するすべての代入文が条件を満たすなら、let式全体も合法な構文となります。

その他もろもろのこと

let式により、ユーザーによる値と関数の定義（項／関数項への名前付け）をシミュレートできます。再帰的な定義まで扱うにはletrec式が要ります（let, letrecを区別しない流儀もありますが）。

let/letrec式まで定義できれば構文的にはそれでOKですが、ラムダ式（ラムダ項）は計算の対象なので計算の方法も必要です。ラムダ式の計算とは、アルファ変換とベータ変換です。変数／関数変数の系統的なリネーミングと置換（substitution）の手法が必要です。再帰が入ると難しくなります。現実的な計算系では、組み込みや神託の機能に相当するデルタ変換や、外延性の表現であるイータ変換を使うかもしれません。

使いやすい計算系の条件として、停止性と合流性（チャーチ／ロッサー性）があります。停止して合流する計算系なら、項の正規形がハッキリと定義できます。今定義した、型が順序を持つラムダ計算でも、正規形までちゃんと定義しないと安心して使えませんね。ちゃんと示すのは疲れるけど。

構文的に定義された計算系を具体的な状況で使うには、その状況に即した意味論も必要です。型表現（type expression）に実際の領域（集合）を割り当て、定数には値（集合の要素）を割り当てます。Funcに属する記号には、なんらかの写像を割り当てます。必ずしも集合と要素を使う必要はありませんが、各種の記号と式に対して、意味領域内の意味対象を割り当てる作業が必要です。構文的な表現や操作（変換、書き換え）が、意味領域上の対応する現象としてうまく説明できれば、不安なく計算系を使えます。

「高階関数を持たないが型の順序を持つラムダ計算」の構文論と意味論を一式準備しようと思ったのは、Catyの型システムにおける型計算がそのような計算系を要求しているからです。事後的正当化なので、あんまり美しくないなー、とか思いながらやっています。参考までに「美しくない」ところを挙げると：

  1. 値の型Tと、引数なし関数の型 T0=>T が両方ある。混乱を避けるため、T0=>T のほうを人為的（恣意的）に禁止している。
  2. 値の変数（Varの要素）と関数の変数（FVarの要素）の区別がない。名前が値を表すのか関数を表すのかを構文では判断できない。
  3. letとletrecの区別がないので、再帰的な定義になっているかどうかは即座には分からない。

まー、この程度のことはしょうがないと言えるでしょう。でも、計算系として本質的な欠陥があるとエライことなので、形式化して確認しているわけです、疲れるけど。

*1:今回の話では、型＝構文的型表現 という前提が強いですが。

*2:一般に、σ、ρなどを使うことが多いようです。

*3:ここで代入は、破壊的なデータ更新操作ではなくて、名前と値の束縛を作ることです。