関数型言語の基礎 型なしl計算 型理論 構成的プログラミング GUIにあらわれる関数概念 PBD VL

Presentation on theme: "関数型言語の基礎 型なしl計算 型理論 構成的プログラミング GUIにあらわれる関数概念 PBD VL"— Presentation transcript:

1 関数型言語の基礎 型なしl計算 型理論 構成的プログラミング GUIにあらわれる関数概念 PBD VL
VSL (Visual Scripting Language)

2 l計算 手続き型言語では add1(x)=x+1 (1)
によって関数add1を定義する。これはadd1の関数としての振る舞いは定義するが、関数そのもの表現を与えない。「xをもらってx+1を返す関数」そのものの表現として lx.x+1 をもちいる。関数を構成する操作をl抽象とよぶ。 これにより、(1)は add1= lx.x+1 と等価で、add1を単独でデータとして用いることができる。

3 関数適用 実引数3を渡して値を計算するのに add1(3) のよう表現するのと同様、 (lx.x+1)(3)
のように表す。この（関数呼び出しの）操作を関数適用という。 実際に実引数を関数本体に代入する操作 (lx.x+1)(3)　⇒　 3+1 をb簡約 (b-conversion あるいはb-reduction) という。

4 高階関数 n引数関数 f(x1,…,xn) は lx1.(lx2.(…(lxn. f(x1,…,xn))…))
とあらわせる。（カリー化　Currying） 問い　 （2項演算の）足し算を高階関数で表せ。

5 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)))))

6 束縛変数と自由変数 lx . y(ly . xy) 1のyは自由変数 2,3のx,yは束縛変数

7 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]

8 b-簡約の定義 代入をつかってb-簡約の定義の定義を書くと (lx.M)N ⇒ M[x:=N] この両辺を等しいものと考え
と書く。等号=の公理は他に

9 l計算による算術プログラミング

10 数の表現 cn≡lfx . fn(x) ここで、 Mn(N) ≡ M(M(…(M N) …)) n個 c0≡lfx . xとする
チャーチ数 (Church numeral)

11 算術演算 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

12 条件式 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

13 組 [M, N] ≡ lz . zMN fst ≡ lx . x true snd ≡ lx . x false とすると
fst [M, N]=M snd [M, N]=N

14 不動点演算子 階乗をもとめる関数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))

15 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式を関数とみたときの不動点演算子

16 帰納的定義 任意のl式Mにたいして、 H = lx1…xn.M[h:=H] を満たすl式Hが存在する。
証明：　H ≡ Y (lhx1…xn.M)とせよ。

17 算術関数 「0」 ≡ lx.x 「n+1」 ≡ [false, 「n」] succ ≡ lx .[false, x]
pred≡ lx.x false iszero ≡ lx.x ture

18 Church数に対する算術関数 succC ≡ lxyz.y(xyz)
predC ≡ lxyz.x(lpq.q (py))(lv.z)(lv.v) iszeroC ≡lx.x succ 「0」 true

19 関数の表現 fact をl式で書け