2005/10/19 志村先生

前回は、「計算可能とは何か」という観点から、帰納的関数と、チューリングマシンの
話をした。今回は、\lambda-calculus

λ-calculus (λ-計算) Curry, Church

	# 非常に特殊な考え方をしている
	# 基本的概念は、次の二つ

	1. 全てのものは「関数」である。
		# 「関数」なのは、ここでの関数が、数学の関数と概念が異るから
		#	何でも「関数」
		#		普通の関数は定義域や値域を决める必要がある
		#			λ-calculus では、それらが「何でも」

	2. 計算とは代入である。

# λ-calculus の説明に入る前に、少し、準備

	o 記法について
		「f(x)」 という表現には、二通りの意味がある
			関数 f そのもの
			関数 f の x における値
				この二つを区別するために、λ-記法を導入する

		関数そのものを表す場合
			λx.f(x)	# x を放り込むと f(x) が与えられる
			f(x)		# 関数 f の x における値

		# λ-calculus では、余り等号を使わないが..

		(λx.f(x))(a)	=	f(a)
		(λy.f(y))(a)	=	f(a)

			# λx.f(x) と λy.f(y) は同じ物

	# () について..
	## λ-calculus では、何でも関数なので、「多変数関数」というのもない
	## 引数の個数の概念もない ( 適用の順序は必要だが.. )

		f(x) の代わりに f x とかく

	## λ-calculus では、何でも関数なので、関数とその他の物を区別する必要もない

		f x の代わりに M N とかく

[λ-calculus の定義]
	[def] λ-項
		1. 変数は、λ-項である。
			x, y, z, a, b, c, ...

		2. M, N が、λ-項
			=> MN も λ-項		# 関数適用

		3. M が、λ-項, x が変数
			=> λx.M は λ-項	# λ抽象

	# λ-calculus では、λx.f(x) と λy.f(y) は同じ物とは言うが、勝手にはできない

	[def] α conversion ( 変換 )

		λx.M : λ-項
		y が、λx.M に現れない変数の時

			       α
			λx.M ----> λy.M [y/x]
				#.M [y/x] は M の中の x を全て y に置き換えたもの


	[def] β reduction ( 簡約 )
		λx.M : λ-項
				    β
			(λx.M)(N) ----> M[N/x]
					 M[x := N]
				#.M [N/x] は M の中の x を全て N に置き換えたもの
				# ただし、N は、M と N に含まれる変数が互いに異るように予めα変換しておく。

	[λ-項の例]
		x		変数なのでλ-項

		λy.x		λ-項に λy を付けたのλ-項
				  β
			(λy.x)N ----> x
				常に、値 x を返す「定値関数」となっている。

		λx.(λy.x)
				      β
			λx.(λy.x)N ----> λy.N
				何かを与えると、それ値をとする「定数関数」を返す関数
					# ここで N の中に変数 y が現れると都合が悪いので、予め N の中に変数 y が現れる場合は、他の変数α変換して置く
					## 他にも細かい規則があるがここでは、「いい加減」に話す

		λx.λy.λz.((xz)(yz))
			# λ が続く場合が多いので、省略記法を考える。
		λxyz.((xz)(yz))	# 上と同じ
			# かっこも大変なので、「左優先」と考えてできるだけ省略
		λxyz.xz(yz)		# 上と同じ

# λ-項を使って、「自然数」を考えてみよう !!

	f : X -> X の時..
		f^n(x) = f(f(...f(x)...))
			# x に f を n 回適用する
	を考える。
	# この適用回数 n を自然数だと思う (同一視する)

	自然数 n を f に f^n に対応付ける関数で表す。

		0 -> f^0(x) = x		λxy.y
			# 関数 f として何が入ってきても、x 即ち恒等変換になる
			# 実際
				(λxy.y)f = λy.y	# これは恒等変換

		1 -> f^1(x) = f(x)	λxy.xy
		2 -> f^2(x) = f(f(x))	λxy.x(xy)
				(λxy.x(xy))f = λy.f(fy) = f(f(x)) = f^2(x)
		3			λxy.x(x(xy))
			(以下同様)

	# 自然数が定義されたので、自然数上での演算 ( 例えば足し算 ) を定義する

	## 足し算の意味は、 f^{m+n}(x) = f^m(f^n(x)) という意味なので..

		f^{m+n}(x) = f^m(f^n(x))
			   = (λy.f^m(y))(f^n(x))
				であることを意味するので..

		λuvw.uw(vw)
				が、足し算を行う関数となる。
				実際..

		λuvw.uw(vwz) N = λvw.Nw(vwz)
		λuvw.uw(vwz) NM = λvw.Nw(vwz)M = λw.Nw(Mwz)
		λuvw.uw(vwz) NMf = λvw.Nw(vwz)Mf = Nf(Mfz)
		ここで、Nf は λx.f^N(x), Mf が λx.f^M(x) とすれば、
			Nf(Mfz) = (λx.f^N(x))(λy.f^M(y))z
				= f^N(f^M(z))
				= f^{M+N}(z)
		となるので、
			λuvw.uw(vwz)
		 は、M,N から M+N を計算していることになる

	[def] 自然数上の n 変数関数
		f : N^n -> N
	がλ-計算可能
		<=>
			λ-項 M が存在し、全ての自然数 a_1,..,a_n に対して
				M a_1 a_2 .., a_n ---> f(a_1,..,a_n)
			となること。

	λ-計算は、非常に単純なことしか行っていない ( 主に、代入しか行っていない )
	ところが、かなり色々なことができる。

		# λ-計算では、足し算より掛け算の方が簡単
		#	λ.xyz((xy)z) ????

==

# ここまで、三つの「計算可能」の定義 ( 帰納的関数、チューリングマシン、
# λ計算 ) を紹介したが..、実は、これらは同じ意味を持つ

	[定理] n 変数関数 f : N^n -> N に対して、次の条件は全て同値
		1. f は一般帰納的関数
		2. f は Turing 計算可能
		3. f はλ-計算可能

		# 1 から 2, 1 から 3 は簡単だが、逆は面倒
		#	1 は自然数だけからなるので、それを、2., 3.でエミュレートできる
		#		=> 大変だが、対応を作るだけ
		#	1 には、λや、Turing の状態を表す概念がない
		#		=> 自然数で、λ等を表現するための「技術」が必要
		#		# この「技術」に関しては、他の所でふれる

「Church の提唱」
	計算の概念 ( というあやふやな物 ) を、数学的に定式化を行った結果が、実は ( 幸いか、必然か .. ? ) 同じだった..
		この三つの概念をもって、「計算可能」と呼ぶことにしよう (提唱)

==

[次回予告]
	帰納的関数の理論の詳細を kleene のまとめに従って解説する
		[目標]
			Kleene の T 述語を作る
			# T 述語 = 万能関数
				# 関数の中で、もっとも「偉い」関数
				## この関数に関して理解れば、他の関数のことが解る

		# 万能関数 : 万能 Turing マシンに対応する
		##	万能 Turing マシン : 任意の Turing マシンをエミュレーション可能な Turing マシン