Document

関数型言語の基礎
1.
2.
3.
4.
型なしl計算
型理論
構成的プログラミング
GUIにあらわれる関数概念
1. PBD
2. VL
3. VSL (Visual Scripting Language)
l計算
手続き型言語では
add1(x)=x+1
(1)
によって関数add1を定義する。これはadd1の関数としての
振る舞いは定義するが、関数そのもの表現を与えない。
「xをもらってx+1を返す関数」そのものの表現として
lx.x+1
をもちいる。関数を構成する操作をl抽象とよぶ。
これにより、(1)は
add1= lx.x+1
と等価で、add1を単独でデータとして用いることができる。
関数適用
実引数3を渡して値を計算するのに
add1(3)
のよう表現するのと同様、
(lx.x+1)(3)
のように表す。この（関数呼び出しの）操作を関数
適用という。
実際に実引数を関数本体に代入する操作
(lx.x+1)(3) ⇒ 3+1
をb簡約 (b-conversion あるいはb-reduction)
という。
高階関数
n引数関数 f(x1,…,xn) は
lx1.(lx2.(…(lxn. f(x1,…,xn))…))
とあらわせる。（カリー化 Currying）
問い（2項演算の）足し算を高階関数で表せ。
l計算の構文
Var ::= v | Var ’
Term ::= Var | (Term Term) | (l Var. Term)
Termはl項(lterm)という。
略記法
M1 M2 M3… Mn は ((…((M1 M2) M3 ) …) Mn)
l x1 x2 … xn . Mは (l x1. (l x2 . ( …( xn . M )…)))
の略記法
例： l xyz . xz(yz)は
( l x . ( l y . ( l z . (( xz)(yz)))))
束縛変数と自由変数
lx . y(ly . xy)
1
23
1のyは自由変数
2,3のx,yは束縛変数
a同値と代入
束縛変数の名前だけが違うものは同一視する
（a同値）。またa同値なものに置き換える操作を
a変換(a-conversion)という。
l項Mの自由変数xをl 項 Nでおきかえる操作を代
入という。結果をM[x:=N]と書く。
おきかえの際、 Nが自由変数yをもち、
Mの束縛変数yのl束縛のスコープに自由変数x
があれば、あらかじめMの束縛変数yをべつの名
前に換える。
問： l y.xy [x:=lx . xy]
b-簡約の定義
代入をつかってb-簡約の定義の定義を書くと
(lx.M)N ⇒ M[x:=N]
この両辺を等しいものと考え
(lx.M)N = M[x:=N]
と書く。等号=の公理は他に
M N
M N
M N
,
,
lx.M  lx.M ML  NL LM  LN
l計算による算術プログラミング
1. 数の表現
cn≡lfx . fn(x)
ここで、
Mn(N) ≡ M(M(…(M N) …))
n個
c0≡lfx . xとする
チャーチ数 (Church numeral)
2. 算術演算
A+ ≡ lxypq . xp(ypq)
A* ≡ lxyz . x (yz)
Aexp ≡ lxy . yx
とすると、
A+ cm cn = cm+n
A* cm cn = cm* n
A^ cm cn= cm^ n
3. 条件式
true ≡ lxy . x
false≡ lxy . y
if L then M else N ≡LMN
とすると、
if true then M else N = M
if false then M else N = N
4. 組
[M, N] ≡ lz . zMN
fst ≡ lx . x true
snd ≡ lx . x false
とすると
fst [M, N]=M
snd [M, N]=N
不動点演算子
階乗をもとめる関数factの再帰的定義：
fact(n) = if n=0 then 1 else n*fact(n-1)
高階関数Fの定義：
F(f)(n) = if n=0 then 1 else n*f(n-1)
とすると、 factは f に関する方程式
F(f) = f
の解。このときf はFの不動点という。関数にたい
してその不動点を求める関数（不動点演算子）
をFixと書くと、
Fix(F) = F(Fix(F))
不動点コンビネータ
Y ≡ lf.(lx . f(xx))(lx . f(xx))
とすると任意のl式Mについて
M (Y M) = Y M
このYを不動点コンビネータという。
不動点コンビネータはl式を関数とみたとき
の不動点演算子
5. 帰納的定義
任意のl式Mにたいして、
H = lx1…xn.M[h:=H]
を満たすl式Hが存在する。
証明： H ≡ Y (lhx1…xn.M)とせよ。
算術関数
「0」 ≡ lx.x
「n+1」 ≡ [false, 「n」]
succ ≡ lx .[false, x]
pred≡ lx.x false
iszero ≡ lx.x ture
Church数に対する算術関数
succC ≡ lxyz.y(xyz)
predC ≡ lxyz.x(lpq.q (py))(lv.z)(lv.v)
iszeroC ≡lx.x succ 「0」 true
関数の表現
fact をl式で書け

Download Report