今日は、計算可能関数と型付きラムダ計算の関係について語りましょうか。といっても、主題は「型付きラムダ計算の内部で表現できる関数は計算可能関数であるかどうか」なのですが。
この記事は「 \( \mathrm{pCIC} \) を巨大数論の根本に据える」という考えの元に書かれています。これは私がブログ記事を最初に投稿した時から考えていることなのですが、英語圏で活動していた Emlightened 氏も Definition of Googology を見るに似たようなことを考えていたようです。
型付きラムダ計算[]
計算可能関数については巨大数論に触れている読者なら既にご存知だと思いますが、流石に型付きラムダ計算までは知っていないと思います。ここで触りだけを解説しておきます。
型付きラムダ計算 (typed lambda calculus) とは、型が付いたラムダ計算 (lambda calculus) のことです。まずは、ラムダ計算のことについて説明します。
ラムダ計算 (lambda calculus) とは、型無しラムダ計算 (untyped lambda calculus) のことを普通は指します。ただし、ラムダ計算に類似するものを全て指す言葉として使われることがあるかもないかもしれません。
型無しラムダ計算とは「引数を取る」「一つの値をもう一つの値に適用する」という二つの操作だけで成り立つ計算模型（計算モデル）です。すなわち、チューリング完全です。型無しラムダ計算の式は \( \lambda x \ldotp x ( x ) \) というようなものです。これは引数 \( x \) を取り、 \( x \) に \( x \) を適用するというものです。ラムダ計算の式を形式化するには色々な方法がありますが、私はだいぶ前に de Bruijin index を型安全にしたものを Coq で実装してベータ簡約まで示したことがあります[1]。そこから定義を引っ張ると以下のようなものです[2]。
Inductive fin : nat -> Type := | fin_O : forall n, fin n | fin_S : forall n, fin n -> fin (S n). Inductive lambda : nat -> Type := | var : forall n, fin n -> lambda (S n) | abs : forall n, lambda (S n) -> lambda n | app : forall n, lambda n -> lambda n -> lambda n.
lambda は一つの自然数を受け取る依存型であり、 lambda n は n 個の自由変数を内部に含むラムダ計算の式です。また、その構成子である abs が「引数を取る」という部分に対応します。 abs n t と書いたとき λx. t になぞらえることができます。そのため、 t の中にある自由変数の数は abs n t よりも一つ増えます。さらに、別の構成子である app は単純に「適用する」に対応します。
一つだけ仲間はずれなのが var なのですが、これはある変数を表します。 fin n としたとき、それは n + 1 個の値が存在する型となり[3]、 var は環境に存在する自由変数の一つを表すことになります。ここで何番目の値がどの自由変数を表すかには自由度がありますが、ここでは de Bruijin index であるため \( \lambda z \ldotp ( \lambda y \ldotp y ( \lambda x \ldotp x ) ) ( \lambda x \ldotp z x) \) が abs _ (app _ (abs _ (app _ (var _ 0) (abs _ (var _ 0)))) (abs _ (app _ (var _ 1) (var _ 0)))) となります。
de Bruijin index はラムダ計算の式を表すための方法の一つです。変数の名前を使う方法よりも優れている点は、アルファ変換を考えなくてもいいこと、「自由変数に x が含まれていない」というような Coq で扱うには面倒くさい条件を考えなくてもいいこと、その他です。さらに、ベータ簡約をする際にも de Bruijin index の利点があります。たとえば t という lambda 0 となる自由変数がない式を考えましょう。それを使った式 s t をベータ簡約しようと思ったら s の中に t をそのままはめ込んで s の index を振り直せばいいだけなのです。ただし、変数の名前で変数の意味を表現するということが出来きず、可読性が悪いのが欠点となります。
型無しラムダ計算の定義について説明してきましたが、次は他の概念との関連を説明したいと思います。
まず、関数型言語とラムダ計算は強く関連しています。関数型言語の基礎にはラムダ計算があり、チューリングマシンやレジスタマシンやスタックマシンが基礎にある命令型言語とは対照的です。命令型言語の計算は文を実行することであり、その順番は定まっていますが、関数型言語の計算とは式を評価することであり、評価の順番は様々です。それでいて関数型言語は命令型言語と遜色ない表現力を持っています。関数型言語はラムダ計算の表現力を示している良い一例でしょう。
次に、型無しラムダ計算は SKI コンビネータ計算と直接的に関連しています。ラムダ計算の全ての式は SKI コンビネータ計算において対応する項を持ちます。クサイ関数において使われていることで知られている SKI コンビネータ計算ですが、その本質は型無しラムダ計算を単純化したものです[4]。
さて、型付きラムダ計算の説明に入りましょう。型付きラムダ計算は、ラムダ計算の引数に型が付き、さらに適用も \( A \then B \) と型付けられた値と \( A \) と型付けされた値の間に制限されたりしたものです。型無しラムダ計算でも Church encoding によって疑似的な型を仮想することが出来ますが、意図しない値が与えられると簡単に壊れます。型が組み込まれているとそのようなことがなくなります。また、型無しラムダ計算には簡約が停止しない式が存在します。そのような一例は (λx. x x) (λx. x x) という式です。それが型付きラムダ計算になると、全ての項についての簡約が停止するような体系が存在するようになります。
型付きラムダ計算には様々な種類があり、例をあげると、単純型付きラムダ計算 (simply typed lambda calculus, λ, λ→, \( \lambda \), \( \lambda ^ \rightarrow \)) 、システム・エフ[5]・二階ラムダ計算・（ジラール＝レイノルズ）多相ラムダ計算 (System F, second-order lambda calculus, (Girard–Reynolds) polymorphic lambda calculus, λ2, \( \lambda 2 \)) 、システム・ティー[6] (System T) 、システム・ユー[7] (System U) 、システム・エフ・サブ[8] (System F-sub, System F<:) 、構成計算[9] (calculus of constructions, λC, CoC, CC, \( \lambda C \), \( \mathrm{CoC} \), \( \mathrm{CC} \)) 、帰納構成計算[10] (calculus of inductive constructions, CIC, \( \mathrm{CIC} \)) 、可述的帰納構成計算[11] (predicative calculus of inductive constructions, pCIC, \( \mathrm{pCIC} \)) 、純粋型体系[12] (pure type system, PTS, \( \mathrm{PTS} \)) 、などがあげられます。
カリー＝ハワード対応[]
カリー＝ハワード対応は論理と計算を結び付ける対応関係です。たとえば \( A \then A \) という恒真式である論理式があったとしましょう。これをカリー＝ハワード対応を通して移すと \( [A] \then [A] \) となります。ただし、型 \( [A] \) は命題 \( A \) に対応するものだと考えてください。また、この型は \( \lambda x \ldotp x \) という値を持ちます。これは移す前の論理式に証明が存在するという事実に対応します。
すなわち、ある型付きラムダ計算の体系は、ある論理の体系と対応します。型が付いていることが必要なのは、命題が型と対応するという所が根本的であるからかもしれません[13]。
明確に矛盾している体系として System U があります。この体系が矛盾することはジラールのパラドックス (Girard's paradox) と呼ばれます。具体的な証明を知りたい方は A Simplification of Girard's Paradox という論文の第 3 章を読むのがお勧めです。
型付きラムダ計算はカリー＝ハワード対応により論理と見なすことができます。そのような論理の中には強力なものがあります。私が知る最も強力な例は \( \mathrm{pCIC} \) が \( \mathrm{ZFC} + \textrm{“There are countably many inaccessible cardinals”} \) と無矛盾性が等しいというものです。直観主義的かつ構成的である[14]体系としてはとても強いように見えます[15]。
強正規化性[]
型付きラムダ計算は、式の簡約を項の書き換えとしてみなすことができます。そのため、項書き換え系として解釈できます。
項書き換え系に対して、それが強正規化性 (strong normalization property) を持つとは、その全ての項が強正規化することです。ある項が強正規化する (strongly normalizing) とは、その項をどのような手順で書き換えても最終的には書き換えできない項になることです。すなわち、書き換えが必ず停止することと言い換えられます。
これはただの私の推測なのですが、おそらく、ある型付きラムダ計算が強正規化性を持つことは、それに対応する論理が無矛盾であること、あるいはもっと強くカット除去定理が成り立つことに対応すると思います。
実際に強正規化性が証明されている例としては、単純型付きラムダ計算や System F と、そして Calculus of Constructions などがあげられます。 predicative Calculus of Inductive Constructions についても証明がないか探したのですが無いようです。
計算可能関数[]
ある程度強い型付きラムダ計算ではペアノの公理を満たす三つ組 \( ( \Nat, \zero, \succ ) \) が構成できます。では、任意の \( \Nat \then \Nat \) と型付けされる項 \( f \) が計算可能関数を表現することは言えるでしょうか？ これが言えるのであれば、ある関数がその体系の中で定義できるのであれば、その関数は計算可能だと言えます。
私の答えは「その体系が強正規化性を持っていて、簡約の結果がただ一つしかなくて[16]、 \( \Nat \) で型付けされる項が \( \zero, \succ ( \zero ), \succ ( \succ ( \zero ) ), \ldots \) しかなければ、言える」です。
\( \Nat \then \Nat \) と型付けされる項 \( f \) から計算可能関数 \( \hat{f} \colon \mathbb{N} \rightarrow \mathbb{N} \) を構成するアルゴリズムを与えることを考えてみましょう。
- \( \hat{f} ( n ) \) の値を定める。
- まず、自然数 \( n \) を項 \( \bar{n} \) に変換する。これは \( \zero \) などの項を使えばよい。
- \( f ( \bar{n} ) \) を簡約する。その結果を \( m \) とする。
- 項 \( m \) を自然数 \( \hat{m} \) に変換する。これは \( \zero \) と \( \succ \) のみで構成されていれば可能である。
- \( \hat{f} ( n ) = \hat{m} \) である。
ここではいくつかの問題になりうる箇所があります。一つ目は、簡約が終わらないことです。これは強正規化性により排除できます。二つ目は、簡約の過程によって複数の結果が出てしまうことです。これは簡約の結果がただ一つしかないことを課したことにより排除できます。三つめは、出てきた結果が自然数に戻せないことです。これは \( \Nat \) に余計な要素が含まれないことを条件にしたことにより排除できます。
では、これらの条件はどのくらい厳しいのでしょうか。私の予想になりますが、二つ目と三つ目の条件は証明するのは比較的簡単だと思います。しかし、一つ目の条件、つまり強正規化性を証明することは困難だと思います。
脚注[]
- ↑ https://github.com/Hexirp/coq-gist/blob/a12d169956fb77b189d1d55dfc03e96d7c32ef3c/lambda.v
- ↑ この定義は私のオリジナルではなく、どこかのインターネットの上でアップされていたスライドショーのための PDF に記載されていたものなのですが、なにぶん 2017 年のことなので探そうとしても見つかりませんでした。情報を提供していただければ記事がより正確になるのでありがたいです
- ↑ 本来なら
n個の値というのが自然なのですが、なぜか当時の私はこう実装していたようです - ↑ この記述は https://en.wikipedia.org/w/index.php?title=SKI_combinator_calculus&oldid=943366279 で a reduced version of the untyped lambda calculus と書かれていることに由来していますが、ウィキペディアは出典にならないので、この部分は私の独自の考えだと思ってください
- ↑ 訳語を確認できなかったので音読を記載しました
- ↑ 訳語を確認できなかったので音読を記載しました
- ↑ 訳語を確認できなかったので音読を記載しました
- ↑ 訳語を確認できなかったので音読を記載しました
- ↑ 訳語を確認できなかったので独自に訳語を作成しました。中国語で「构造演算」と訳されていることを参考にして construction が「建設」「構築」「構造」と訳されることから「建設計算」「構築計算」「構造計算」などを考案しましたが建設業界の用語と被ってるため没としました。その後 construction から連想した constructor が「構成子」と訳されることから「構成計算」を考案して採用しました
- ↑ 訳語を確認できなかったので CoC と同様に独自に訳語を作成しました
- ↑ 訳語を確認できなかったので CoC と同様に独自に訳語を作成しました
- ↑ 訳語を確認できなかったので独自に訳語を作成しました
- ↑ ただし、型無しラムダ計算にカリー＝ハワード対応を適用する研究も探せばあるかもしれません
- ↑ ここでの「直観主義的」と「構成的」という表現は私の主観です
- ↑ ここでの「構成的なのにとても強い」という表現は構成的集合論の一つである CZF の強さが ZF と比べて弱いことに由来する私の主観です
- ↑ 項書き換え系としては合流性と呼ばれる性質です