関数型言語の基礎 型なしl計算 型理論 構成的プログラミング GUIにあらわれる関数概念 PBD VL 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] この両辺を等しいものと考え と書く。等号=の公理は他に
l計算による算術プログラミング
数の表現 cn≡lfx . fn(x) ここで、 Mn(N) ≡ M(M(…(M N) …)) n個 c0≡lfx . xとする チャーチ数 (Church numeral)
算術演算 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
条件式 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
組 [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)(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)) 不動点コンビネータ Y ≡ lf.(lx . f(xx))(lx . f(xx)) とすると任意のl式Mについて M (Y M) = Y M このYを不動点コンビネータという。 不動点コンビネータはl式を関数とみたときの不動点演算子
帰納的定義 任意の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式で書け