lambda

Ichiro Satoh

計算モデル特論

型なし

λ計算

国立情報学研究所 所長補佐／教授

佐藤一郎

E-mail: [email protected]

（型なし）ラムダ計算

1. はじめに 2. 関数と型 3. ラムダ記法 4. ラムダ計算 5. 変換例 6. チャーチロッサ性 7. 正規形の求め方 8. ラムダ計算の計算能力

Ichiro Satoh

ラムダ計算

_{(Lambda Calculus)}

n １９３０年代に数学基礎論の研究から生まれた（Ａ．Ｃｈｕｒｃｈ） n 一般に数学で扱われる関数概念に伴う計算的要素を抽出して作られ る計算体系 n 関数型プログラミング言語の基礎理論 n Lisp、Scheme、ML、Haskellなど n プログラムの意味論、型理論の基礎の一つ

Javaのプロジェクトラムダ

n JDK 8に導入されたラムダ計算風の記述 inc = #(int x) (x+1); （λ計算の場合、λx:int.(x+1)) n Javaにラムダ式を導入するメリット n クラス単位のモジュールから、細粒度のコードの再利用が可能になる n 細粒度な（関数型）コードによる並列処理

Ichiro Satoh

Javaラムダ式

n 「関数型インターフェース」（1つのインターフェースに実装が必要なメソッド を1つだけ持つインターフェース）のメソッドを容易に実装

n 従来記法

Button button = new Button();

button.addActionListener(new ActionListener(){ public void actionPerformed(ActionEvent e) {

System.out.println("ボタンが押された"); }

});

n Javaラムダ式による記法

Button button = new Button();

button.addActionListener(e -> System.out.println(" ボタンが押された"));

Javaラムダ式の例

Javaラムダ式の例 備考 (int n) -> { return n + 1; } 引数が1個の場合の基本形 (int n) -> n + 1 文が1つだけの場合、波括弧（と return）を省略可能 (n) -> n + 1 引数の型を省略 n -> n + 1 引数が1個の場合は丸括弧を省略可 能

(int n1, int n2) -> { return n1 + n2; } 引数が2個の場合の基本形 (int n1, int n2) -> n1 + n2 文が1つだけの場合、波括弧（と

Ichiro Satoh

関数と型

n 関数：与えられた引数に適用して値を得るための操作 n f(x): 関数 f を x に適用して得られた値 n x のとりうる値の領域A（定義域と呼ぶ） n f(x) のとりうる領域B（値域と呼ぶ） n このような関数の集合は“Ａ→Ｂ”と書き、f の型と呼ぶ n 例: square(x) = x * x n x のとりうる領域は自然数Ｎのとき、square の型は Ｎ→Ｎ であ る。これを、square∈Ｎ→Ｎとかく

疑問

n Ｎ→（Ｎ×Ｎ）はどんな関数か？ n １つの自然数を与えると関数が得られる関数 n ｆ_ｘ（ｙ）＝ｘ・ｙで、ｘをある値ｋに決めれば、ｆ_ｋ（ｙ）＝ｋ・ｙで、Ｎ→ Ｎの型を持つ関数となる n （Ｎ×Ｎ）→（Ｎ×Ｎ） はどんな関数か？ n 関数を引数として、関数が得られる関数 n ｔｗｉｃｅ ｆ（ｘ）＝ｆ（ｆ（ｘ）） なる関数 ｔｗｉｃｅ を考える n ｆ（ｘ）のところにｓｑｕａｒｅを引数として与えれば、 n ｔｗｉｃｅ ｓｑｕａｒｅ（ｘ）＝ｓｑｕａｒｅ（ｓｑｕａｒｅ（ｘ）） n として関数を作り出す n f: (N₁×・・・×N_m) →（M₁×・・・×M_k）に関数名fはいるのか n 関数名がなくても関数

Ichiro Satoh

高階関数

_{(higher-order function)}

n

関数を引数とする関数や関数を結果とする関数

n

例：

twice (f (x)) = f(f(x))

関数を引数とする関数

n 関数の関数などを取り扱っていくうえで、関数を値と同様に取り扱え ると便利 n 例：関数の関数 ｔｗｉｃｅ ｆ（ｘ）＝ｆ（ｆ（ｘ）） を考える n ｆ（ｘ）のところにｓｑｕａｒｅを引数として与えれば、 ｔｗｉｃｅ ｓｑｕａｒｅ（ｘ）＝ｓｑｕａｒｅ（ｓｑｕａｒｅ（ｘ））＝ｘ・ｘ・ｘ・ｘ 従って、値域はＮの型を持つ。

Ichiro Satoh

例：

_{Google MapReduce}

n Googleの検索エンジンを支える超大規模分散処理技術 n 関数型計算モデルがベース。大規模データを多数のサーバーで処理 n 入力ファイルとmap(), reduce() の二つの関数を定義して MapReduce システムに処理を依頼 n MapReduce が入力ファイルに対して複数サーバーに分散させて map() → reduce() を処理 n 実装はC++で記述された並列分散システム（関数型言語ではない） n Hadoop (MapReduce互換システム)はJavaで記述 nMapReduceはWeb検索、DNA解析 では極めて有効 n（関数型）計算モデルの考え方を理解 できないとMapReduceは使えない nAmazonのMapReduceサービスなら サーバ1000台×1時間でも1万円強

ラムダ記法の必要性

n 関数として計算を扱うため、余計なものは取り除く n 例：f(x) = x * x とするとき、f(x)とは n xを変数とする関数fを表すのか、それとも n 関数fのxにおける値を表しているのかが不明確

n 関数に名前を付けず、関数も一つのモノ(first class object)として扱う λx.(x*x)

Ichiro Satoh

ラムダ式

n ラムダ式 λx.M を関数とみると n xは仮引数、Mが関数本体 n ラムダ式 N M （N と M ラムダ式、例えばNは例えば λx.M ）を n N M はNの仮引数をMに置き換える（N を M に適用する読む） n 例： n (λx.x+1)2 は「(λx.x+1)を2に適用する」となり、2+1 となる

ラムダ記法の例

n 例：f(x) = x２_{+2y+1のラムダ記法}

n λx.(x２_{+2y+1) 関数(x}２_{+2y+1)の引数はxであり、yは固定値と扱う}

n c.f.

n λy.(x２_{+2y+1) 関数(x}２_{+2y+1)の引数はyであり、xは固定値と扱う} n λx.(λy.(x２_{+2y+1)) 関数(x}２_{+2y+1)の引数はxとyであること}

Ichiro Satoh

ラムダ抽象

(Lambda Abstraction)

n

式

Mの中の固定値を表す名前を変数にすること

λx.M

n

Mはxを変数とする関数となる（

ラムダ抽象

）

n ラムダ抽象の逆操作 n ラムダ適用、 n 部分計算 n 定数畳み込み

ラムダ適用

(Lambda Application)

n 関数M中の変数 x に値（または関数） d を代入すること

((λx.M)d)

引数Nに関数Mを適用する（ラムダ適用）

(M N)

n 例： n ((λx.(x２+2y+1))3) → 3２+2y+1 n ((λy.(x２+2y+1))4) → x２+2・4+1 n ((λx.(λy.(x２+2y+1))4)3) →3２+2・4+1

Ichiro Satoh

関数の自己適用

n 関数ｔｗｉｃｅのラムダ記法 ｔｗｉｃｅ＝λｆ．（λｘ．ｆ（ｆ ｘ）） n 関数ｔｗｉｃｅに関数ｇを引数として適用すると、 ｔｗｉｃｅ ｇ ｎ＝（λｆ．（λｘ．ｆ（ｆ ｘ））ｇ）ｎ ＝（λｘ．ｇ（ｇ ｘ））ｎ ＝ ｇ（ｇ ｎ） n ｇをｔｗｉｃｅに置き換えてみる ｔｗｉｃｅ ｔｗｉｃｅ ｇ ｎ ＝（（ｔｗｉｃｅ ｔｗｉｃｅ）ｇ）ｎ ＝（ｔｗｉｃｅ（ｔｗｉｃｅ ｇ））ｎ＝（ｔｗｉｃｅ ｇ）（（ｔｗｉｃｅ ｇ）ｎ） ＝（ｇ（ｇ（（ｔｗｉｃｅ ｇ）ｎ）））＝ｇ（ｇ（ｇ（ｇ ｎ）））

ラムダ式

n BNF文法による定義

M ::= x | (λx.M) | (M

₁

M

₂

)

n ラムダ計算とは規則に従って、ラムダ式を順次変形していくこと

ラムダ抽象

ラムダ適用

Ichiro Satoh

ラムダ式の例

n

x

n

(λx.x)

n

(λx.y)

n

(λx. (λy.x))

n

((λx.(x x)) y)

n

((λx.(x x)) (λy.y))

ラムダ式

n ラムダ式の定義 n （１）変数ｘ，ｙ，ｚ．．．，定数１，２，３，．．．はラムダ式 n （２）Ｍがラムダ式、ｘが変数なら、λｘ．Ｍもラムダ式（ラムダ抽象） n （３）Ｍ，Ｎがラムダ式なら、ＭＮもラムダ式（関数適用） n 表記（括弧の省略） n

λｘ

１

ｘ

２

・・・ｘ

ｎ

．Ｍ＝

λｘ

１

．（

λｘ

２

．（・・・（

λｘ

ｎ

．Ｍ）・・・））

n

Ｍ

１

Ｍ

２

Ｍ

３

・・・Ｍ

ｎ

＝（・・・（（Ｍ

１

Ｍ

２

）Ｍ

３

）・・・）Ｍ

ｎ （括弧表記が自然に補えるようになる頃には、ラムダ計算は詳しくなっているはず）

Ichiro Satoh

ラムダ式の省略形

n 省略の規則： n 一番外側の括弧は外してよい n

(λx

₁

.(λx

₂

...(λx

_n

.M)...))

は

λx

₁

x

₂

...x

_n

.M

と書いてよい

n

(...(M

₁

M

₂

)...M

_n

)

は

M

₁

M

₂

... M

_n

と書いてよい

n 例題： (λx.(λy.((xy)(zu)))) = λx.(λy.((xy)(zu))) = λxy.((xy)(zu)) = λxy.xy(zu)

自由変数

n

ラムダ式

Mに含まれる自由変数の集合FV(M)

FV(x) = {x}

FV(M

₁

M

₂

) = FV(M

₁

) ∪ FV(M

2

)

FV(λx.M) = FV(M) - {x}

n

自由変数でない変数を束縛変数

Ichiro Satoh

変数

n 束縛変数 n ラムダ式のxを変数としてラムダ抽象 n 自由変数 n 式に含まれる変数と抽象化の対象が結びついているかどうか ｘ（λｘｙ．ｘｙｚ）ｘｙ このとき、青字変数は自由変数、赤字変数は束縛変数 n ラムダ式Ｍ_１，Ｍ_２，・・・Ｍ_ｎで、それらの束縛変数と自由変数が重ならない ように置き換えができる。 n 重なりがない状態＝「変数条件を満たす」という

変換規則

n α-規則（束縛変数の名前を置換）

(λx.M)=(λy.[y/x]M)

ただし、yがMの自由変数ではないとする n β-規則（ラムダ式における計算）

((λx.M) N)

→ [N/x]M

ここで、[b/a]MとはM中の自由変数aをbで置き換える n β変換によるラムダ式の書き換えをリダクションという。 n リダクションが可能な部分をリデックスと呼ぶ。 n リデックスが含まれていないとき、そのラムダ式は正規形であるという

Ichiro Satoh

α変換の例

n

(λx.x) = (λy.y)

n

((λx.x) (λx.xy)) = ((λy.y) (λz.zw))

n

(λx. (λx.x)) = (λy. (λz.z))

リダクションの練習問題

n

（１）

(λｘｙ．ｙ）３ ２

n

（２）（

λｘｙ．ｘｙ）（λｗ．ｗ・ｗ）９

n

（３）

（

λｘｙ．ｘ）

（

λｘ．ｘｘ）（λｚ．ｚ）

n

（４）

（

λｘｙ．ｙ）

（

λｘ．ｘｘ）（λｚ．ｚ）

n

（５）

（

λｘ．ｘ（λｘｙ．ｘ））

（

λｘ．ｘ）

n

（６）（

λｘ．ｘ（λｘｙ．ｘ））

（

λｘ．ｘ（λｘｙ．ｙ））（λｘ．ｘ）

Ichiro Satoh

リダクションの練習問題（解答）

（１）（

λｘｙ．ｙ）３ ２ → （λｙ．ｙ）２ → ２

（２）（

λｘｙ．ｘｙ）（λｗ．ｗ・ｗ）９

→（λｙ．（λｗ．ｗ・ｗ）ｙ）９→（λｙ．ｙ・ｙ）９→９・９

（３）（

λｘｙ．ｘ

）（

λｘ．ｘｘ）（λｚ．ｚ）

→（λｙ．（λｘ．ｘｘ））（λｚ．ｚ）→λｘ．ｘｘ

（４）（

λｘｙ．ｙ

）（

λｘ．ｘｘ）（λｚ．ｚ）

→（λｙ．ｙ）（λｚ．ｚ）→λｚ．ｚ

リダクションの練習問題（解答）

（５）（λｘ．ｘ（λｘｙ．ｘ））（λｘ．ｘ） →（λｘ．ｘ）（λｘｙ．ｘ）→（λｘｙ．ｘ） （６）（λｘ．ｘ（λｘｙ．ｘ））（λｘ．ｘ（λｘｙ．ｙ））（λｘ．ｘ） →（λｘ．ｘ（λｘｙ．ｙ））（λｘｙ．ｘ）（λｘ．ｘ） →（λｘｙ．ｘ）（λｘｙ．ｙ）（λｘ．ｘ） →（λｙ’．（λｘｙ．ｙ））（λｘ．ｘ） →（λｘｙ．ｙ）

Ichiro Satoh

変換（リダクション）の例

（１）自由変数と束縛変数が衝突する場合は、書き換えておく （λｘｙ．ｘ）ｙｚ → （λｙ．ｙ）ｚ → ｚ （誤り） （λｘｙ．ｘ）ｙｚ → （λｘｙ’．ｘ）ｙｚ → （λｙ’．ｙ）ｚ→ｙ （２）リダクションを行うと複雑になってしまう例 （λｘ．ｘｘｘ）（λｘ．ｘｘｘ） →（λｘ．ｘｘｘ）（λｘ．ｘｘｘ）（λｘ．ｘｘｘ） →（λｘ．ｘｘｘ）（λｘ．ｘｘｘ）（λｘ．ｘｘｘ）（λｘ．ｘｘｘ） →・・・・

変換（リダクション）の例（続き）

（３）自分に戻ってしまうリダクション （λｘ．ｘｘ）（λｘ．ｘｘ） → （λｘ．ｘｘ）（λｘ．ｘｘ） （４）異なる部分から始めて同じ結果が出るリダクション Ｉ≡λｘ．ｘとする Ｉ（Ｉ ｘ）は二つのリデックスＩ（Ｉ ｘ）とＩ ｘを持つ Ｉ（Ｉ ｘ）→ Ｉ ｘ → ｘ Ｉ（Ｉ ｘ）→ Ｉ ｘ → ｘ

Ichiro Satoh

①

②

正規形の求め方

n

正規形を計算する戦略

n

２つのリデックスがあるとき、どちらを選ぶか？

n

Ｍ

≡（λｘ．ｙ）（（λｘ．ｘｘ）（λｘ．ｘｘ））

n

①では、Ｍ

→Ｍ→・・・の無限のリダクションが続く

n

②では、Ｍ

→ｙとなり、１回で完了

n

リダクション戦略

n

（１）ラムダ式がＭ正規形を持つならば、

最も左側

のリ

デックスを常にリダクションすることで、必ず正規形が

得られる。

n

（２）最も左側のリデックスとは、

最も外側

のリデックス

のうちで、最も左側のものであること

Ｍ

Ｑ

Ｐ

Ｎ

＊

＊

＊

＊

Ｍ

→Ｎ、Ｍ→Ｐのとき、

（０回以上のリダクションで ＭからＮに到達する意味） （ＭからＰ）

適当なリダクションで、

Ｑに合流できる。

* *

チャーチ・ロッサ性

n ラムダ式にリデックスが複数あるとき、そのどれに注目するかにより、 何通りかのリダクションの可能性がある。 n 場合によっては、正規形にならないリダクションもある。 n 複数のリダクション列ができるとき、その結果得られる正規形は途中 のリダクションの道筋によらず一意に決まる。

Ichiro Satoh n リダクションの順序に気を使う必要がない n どんな方法でリダクションを行っても、得られた結果（正規形）が唯一 であることが保証される n （通常の並列計算や、非決定的な計算では、計算の順序を保つため、 同期が必要となる）

チャーチ・ロッサ性の利点

コード化：論理値

n 論理値の真（ｔｒｕｅ）と偽（ｆａｌｓｅ）は次のようなラムダ式に対応 n

「ｔｒｕｅ」≡λｘｙ．ｘ

（Ｔと略記することもある） n

「false」≡λｘｙ．ｙ

（Ｆと略記することもある） n 条件判定式に対応するラムダ式（ＡとBはプログラム分に相当）

n

「cond」≡λb λA. λB．bAB

Ichiro Satoh

コード化：論理値の例

n 定義：

true = λxy.x (λx.(λy.x)) false = λxy.y (λx.(λy.y)) if cond then P else Q = cond P Q

n 例：if true then A else B = (λxy.x) A B

→ (λy.A) B → A

n 例：if false then A else B = (λxy.y) A B → (λy.y) B → B

コード化：論理値の取り扱い

n AND (λxy.xy)False n OR (λxy.y True x) n NOT (λx.x False True)

n 例：AND True False

((λxy.xy)False)True False → True False False = (λxy.x)False False → False

参考：ゼロ判定 （自然数についてはこのあと）

Ichiro Satoh

コード化：自然数

n 自然数ｎに対応するλ式 n 「０」と「次の自然数」という概念からコード化

「０」≡λf．λｚ．ｚ

「１」≡λf．λｚ．ｆ ｚ

「２」≡λf．λｚ．ｆ (ｆ ｚ)

．．．

「Ｎ」 ≡ λf． λｚ．ｆ

ｎ

ｚ

n _{次の自然数を求める関数のコード化}

Succ≡ λn． λf． λｚ．ｆ(ｎ ｆ ｚ)

コード化：自然数演算

n 自然数演算に対応するλ式 n 足し算のコード化

Add≡ λm． λn．m Succ n

n かけ算のコード化

Mul≡ λm． λn．m (Add n) 「０」

n _{ゼロ判定関数のコード化}

Ichiro Satoh

不動点定理

n 任意のλ項Hに対して、 n HX=X n これを満たすX として n H (λx.H (x x)) (λx.H (x x))をとると n X は H Xとなる n H を X に作用させて X となることから、X をHの不動点という f = g (f) となるような関数を g の不動点と呼ぶ n 不動点は不動点コンビネータとして知られるものに よってラムダ計算 で表現することができる

不動点オペレータ

n ループは再帰呼び出しとして表現 n ただし、再帰呼び出し構文がないので、不動点コンビネータYを導入

Y ≡ λf.(λx.f (x x)) (λx.f (x x))

n 例： Ｙを任意のラムダ式Ｆに適用すると ＹＦ → （λｘ．Ｆ（ｘ ｘ））（λｘ．Ｆ（ｘ ｘ）） → Ｆ（（λｘ．Ｆ（ｘ ｘ））（λｘ．Ｆ（ｘ ｘ））） → Ｆ（ＹＦ） β変換を等式とみなすと、 Ｆ（ＹＦ）＝ＹＦ ・・・・ラムダ式Ｆの不動点はＹＦとなる （関数ｆの不動点とは、ｆ（ｘ）＝ｘとなるｘのこと）

Ichiro Satoh

ループと再帰

n ループは基本的に再帰呼出しで書く。ただし、再帰呼出しの構文は 無いことから、不動点コンビネータ(fixed-point combinator)を使う n 不動点コンビネータの例：Yコンビネータ Y = λf.(λx.f (x x)) (λx.f (x x)) n 再帰関数は第1引数に自分自身が渡されるとして定義 F = λf.λx. ... (f x) ... # (f x)は再帰呼出し n (Y F)とすると、fが(Y F)自身に置き換わった再帰関数となる n (Y F)を引数に適用したものを簡約して正規形が得られるならば, F (Y F)を引数に適用したものも同じ正規形に簡約される性質を利用

再帰計算と

_{Yコンビネータ}

n fac(n) := 1, if n = 0; and n × fac(n - 1), if n > 0 をλ式に基づくと

fac = λn. If (IZERO n) 1 (Mult n (fac (Sub n 1)))

n facを未知とするλ式に変えると

H = λfn. If (IZERO n) 1 (Mult n (f (Sub n 1)))

n Hを抽象化したλ式を導入する、不動点コンビニネータYを利用して

Y = λg. (λx. g (x x)) (λx. g (x x)) をおくと、g (Y g) は Y g となる

Ichiro Satoh n ラムダ計算モデルによるプログラム n 各自然数ｋを正規形のラムダ式「ｋ」で表す。 ｇ：Ｎｎ_{→Ｎに対して、} ｇ（ｋ_１，ｋ_２，・・・，ｋ_ｎ）＝ｋ ⇔ Ｇ「ｋ_１」「ｋ_２」・・・「ｋ_ｎ」→「ｋ」 を満たすラムダ式Ｇを、関数ｇを計算するためのプログラムとみな す n 「ｋ_１」，「ｋ_２」，・・・，「ｋ_ｎ」はこのプログラムの入力とみなす。 n このプログラムＧを入力「ｋ_１」，「ｋ_２」，・・・，「ｋ_ｎ」に対してβ変換を 次々と行うことを、計算過程としてとらえる n 変換が終結して「ｋ」が得られたとき、プログラムの計算結果がｋ であると考える。変換が終結しない場合、プログラムの計算結果 は未定義となる

ラムダ計算の計算能力

計算モデル特論

型つき

λ計算

国立情報学研究所 所長補佐／教授

佐藤一郎

E-mail: [email protected]

Ichiro Satoh

型とは

n プログラミングにおけるデータ型

Pascal:

var x,y: integer, a:real

型の必要性

n

プログラム設計を明確化

n

プログラムの誤り防止

n

関数やモジュールの仕様

n

コンパイラ最適化への補助情報

n

プログラム停止性への補助保証

n

可読性の向上

Ichiro Satoh

プログラミング言語の型

n 基本データ型 n 整数、浮動小数点、文字、真偽値 n 構造データ型 n 配列、直積型、直和型、レコード型、ストラクチャ型 n ユーザ定義型

型付プログラミング言語

n 型なしプログラミング言語 n プロトタイピング、×インタープリタ実行 n 弱い型付プログラミング言語 n 手っ取り早く設計・記述、×信頼性が低い n 強い型付プログラミング言語 n 安全なプログラム、×慎重な設計と冗長な記述 n 型検査 n 静的検査 n 動的検査

Ichiro Satoh

型推論

n 強い型付プログラミング言語を利用しながら簡潔な記述を実現するには n 型は文面から推定可能 n 例：f(x) = if x == 0 then 1 else x * f(x-1) n 推定により冗長な記述を現象 n 形式的な体型により型を厳密に決定

型推論の例

n 式要素の型と式全体の型 n 例： if e0then e1else e2 「もしe0が真偽値型（bool型）で、e1とe2がT という型を持つことが示 されれば、if e0then e1else e2はT という型を持つ（ことがわ かる）」 n 型推論の目的 n 与えられた式がある型を持つことを証明する n 与えられた式がもつ型を求める

Ichiro Satoh

型理論体系

n 項（term） n 型（type） n 判定（judgment） n 推論規則（inference）

型付ラムダ式（基本）

n BNF文法による型

τ ::=

b | (τ→τ)

ここで b は基底型、 τ×・・・×τは組、 τ→τは関数 n BNF文法による型付ラムダ式

M ::=

c

τ

_{| x | (λx:τ.M) | (M}

1

M

2

)

Ichiro Satoh

型付ラムダ式

n 型

τ ::=

b | (τ×・・・×τ) | (τ→τ)

ここで b は基底型、 τ×・・・×τは組、 τ→τは関数 n 型付ラムダ式

M ::=

c

τ

_{| x | (λx:τ.M) | (M}

1

M

₂

)

|

(M

₁

,...,M

₂

) | M.i

型付ラムダ式

n BNF文法による型 n

基本型:

b

n

直積型：

(τ×・・・×τ)

n

関数型：

(τ→τ)

n 括弧の省略 n 型における矢印は右結合 n 例: (τ1→(τ2 →(τ3→τ4) = τ1→τ2→τ3→τ4

Ichiro Satoh

型付ラムダ式の直感的意味

n 基本式：

n

(M

₁

M

₂

)

関数M1に引数M2を与えたときの値

n

(λx:τ.M)

型がτである仮引数 x をもつ、関数本体をMと定義される関数

型付きラムダ式の例

n

f(x)=x+1なる関数fは

λx:int.x+1

n

fに実引数3を与えた式f(3)は

(λx:int.x+1)(3

int

₎

Ichiro Satoh

自由変数

n

ラムダ式

Mに含まれる自由変数の集合FV(M)

FV(c) = 0

FV(x) = {x}

FV(M

₁

M

₂

) = FV(M

₁

) ∪ FV(M

2

)

FV(λx:t.M) = FV(M) - {x}

FV((M

₁

,..,M

₂

)) = FV(M

₁

) ∪ .. ∪ FV(M

2

)

FV(M.i) = FV(M)

n

自由変数でない変数を束縛変数と呼ぶ

型付ラムダの計算

n 簡約規則

[N/x]c = c

[N/x](M

₁

,...,M

_n

) = ([N/x]M

₁

,...,[N/x]M

_n

)

[N/x](M.i) = ([N/x]M).I

(λx:τ.M)=(λy:τ.[y/x]M)

((λx:τ.M) N:τ) → [N/x]M

Ichiro Satoh

記法

n 前提（assumption）：

e:t

n ある式eが型tを持つこと n 判定（judgement）:

A ├ e:t

n （０個以上の）前提A（型環境）から、ある式eが型tを持つことが示される n 推論（inference）： 式Miがそれぞれの前提Aiにおいて型τを持つならば、結論が示される

A

1

├ M

1

:τ

1

・・・・・ A

n

├ M

n

:τ

n

A├ M:τ

型推論規則

n 型推論規則

τ

τ

_:

c

├

Γ

)

)

(

(

:

τ

Γ

=

τ

Γ

├

x

x

2 1 1 2 1

:

.

:

:

}

:

{

τ

τ

τ

λ

τ

τ

→

Γ

+

Γ

M

x

M

x

├

├

2 2 1 1 2 2 1 1

:

:

:

τ

τ

τ

τ

M

M

M

M

├

├

├

Γ

Γ

→

Γ

n n n n

M

M

M

M

τ

τ

τ

τ

×

×

Γ

Γ

Γ

!

"

!

1 1 1 1

:

)

,

,

(

:

:

├

├

├

)

1

(

:

.

:

₁

_i

_n

i

M

M

i n

_≤

_≤

Γ

×

×

Γ

τ

τ

τ

├

├

_!

(const) (var) (abs) (app) (prod) (proj)

Ichiro Satoh

型推論規則の記法

n 前提への操作と表記

Γ+{x:τ}

n _{前提Γに x:τ を追加、ただし、 Γに変数xに関する勝たし体があっ} た場合は、もっとも右側を優先する

Γ(x)=τ

n _{前提Γのもとで、定数あるいは変数xが型τを持つことをあわす。}

型推論規則（詳細）

n 型推論規則

τ

τ

_:

c

├

Γ

)

)

(

(

:

τ

Γ

=

τ

Γ

├

x

x

:

}

:

{

_τ

_τ

+

Γ

x

├

M

(const) (var) 関数λx:τ1.Mが関数型τ1→τ2を持つ

Ichiro Satoh

型推論規則（詳細）

n 型推論規則 2 2 1 1 2 2 1 1

:

:

:

τ

τ

τ

τ

M

M

M

M

├

├

├

Γ

Γ

→

Γ

n n n n

M

M

M

M

τ

τ

τ

τ

×

×

Γ

Γ

Γ

!

"

!

1 1 1 1

:

)

,

,

(

:

:

├

├

├

)

1

(

:

.

:

₁

_i

_n

i

M

M

i n

_≤

_≤

Γ

×

×

Γ

τ

τ

τ

├

├

_!

(app) (prod) (proj) 関数は、関数がその定められた値 にのみ適用可能であり、その結果 は関数の値の型を持つこと 関数の組(M1,...,M2)はM1,...,M2の 直積となる 関数の組(M1,...,M2)からI番目の 要素を取り出したときはM1の型 となる

型推論の例

n 型推論では推論規則により変形していく n 型付ラムダ式

K=λx.(λy.x)

)

(

:

)

.

:

.(

:

:

.

:

}

:

{

:

}

:

{

1 2 1 2 1 1 2 2 1 1 1

τ

τ

τ

τ

λ

τ

λ

τ

τ

τ

λ

τ

τ

τ

→

→

Γ

→

x

y

x

x

y

x

x

x

├

├

├

Ichiro Satoh

型推論の性質

n 健全性 n 型推論できるならば、その結果が正しい（型安全）ことを意味する n 完全性 n 正しいことはすべての型において推論することができる n 有用性 n 決定可能かつ効率がよいこと

多相型

n プログラム中に現れる同一の式やデータが複数の型をもつこと n L.CardelliとP.Wegnerによる分類 n アドホックな多相型 n 文脈によって型を決定。例、等号、オーバーローディング演算 子 n 系統的な多相型 n 共通の性質をもった型に作用。例：パラメトリック多相型