Upgrade to Pro — share decks privately, control downloads, hide ads and more …

私を SKI に連れてって

Susisu
December 11, 2015

私を SKI に連れてって

Lazy K の紹介のつもりが型無しラムダ計算の説明から入ったので長くなりすぎたもの

Susisu

December 11, 2015
Tweet

More Decks by Susisu

Other Decks in Programming

Transcript

  1. λࣜ 変数 a, b, c, ..., x, y, z, ...

    λ抽象 λx.x, λx.λy.(x y), ... 関数適用 (f x)
  2. Quiz 1. λx.x y = λy.y y ? 2. (λx.λx.x

    y) y = λy.y y ? 3. λx.x = (λx y z.x z (y z)) (λx y.x) (λx y.x) ?
  3. Q. Ͳ͏ܭࢉ͢Δͷ 入力 x が与えられるとする 手続きを表すλ式 p をうまく選べば、 例えば y

    = p x で出力が得られる y を変換・簡約すれば解読できそう
  4. Church਺ 0 := λf x.x 1 := λf x.f x

    2 := λf x.f (f x) ...
  5. Church਺ 次の自然数を求める関数 Succ Succ := λn f x.f (n f

    x) 足し算 Add Add := λa b f x.a f (b f x) 掛け算はどうなるか考えてみよう
  6. Church਺ 前の自然数を求める関数 Pred Pred := λn f x. n (λg

    h.h (g f)) (λy.x) (λy.y) ただし Pred 0 = 0 キリがないのでこれ以上はやめる
  7. Churchਅཧ஋ AND, OR, NOT And := λp q.p q False

    Or := λp q.p True q Not := λp.p False True
  8. ड़ޠͷྫ Church数 n が 0 かどうか調べる 0 = λf x.x

    だった IsZero := λn. n (λx.False) True だんだんとプログラムが書ける気が してきませんか?
  9. Churchର リストや木構造は対 (pair) の連鎖 で表現できる [1, 2, 3] = (1,

    (2, (3, 空))) 対をλ式で表現できればいいよね
  10. Quiz 入力 x が 2 つのChurch数 a, b の Church対で与えられる

    出力 y = p x が、a = 0 なら y = b、 それ以外なら y = a * b となる p を書いてみよう Succ などこれまでに定義したものは 使ってもよい
  11. ܁Γฦ͠ॲཧ 繰り返し処理を関数で表現したい時 は、再帰的な関数を書けばいい f(0) = 1, f(n) = n *

    f(n - 1) けれどλ計算では"再帰的な定義"が できないので、単純には書けない
  12. Fix 関数 f を引数にとり、その不動点を 返す関数 Fix が存在したとする Fix f =

    f (Fix f) f = λx n. IsZero n True (x (Pred n)) Fix f n は n 回の空ループになる
  13. Fix できる! Fix := λf.(λx.f (x x)) (λx.f (x x))

    実際に Fix f = f (Fix f) となるか 確かめてみるとよいです
  14. ίϯϏωʔλͷྫ B x y z = x (y z) C

    x y z = x z y W x y = x y y
  15. ίϯϏωʔλͷྫ S x y z = x z (y z)

    K x y = x I x = x 実は I = S K K とも書ける
  16. SKI ͰChurch਺ 0 := KI 1 := I 2 :=

    S(S(KS)K)I ... Succ := S(S(KS)K)
  17. SKI ͷ·ͱΊ S, K, I という 3 つのコンビネータ と適用だけで計算をする チューリング完全

    λ抽象と相互に変換できる データも表せるし、繰り返し処理も できる
  18. ग़ྗ 入力 X とプログラム P に対して、 出力は Y = P

    X 出力も文字コードをChurch数で表現 したものの、Church対によるリスト 出力の終端も 256 以上のChurch数
  19. ه๏ Lazy K には 4 つの記法がある コンビネータ計算 …… S(KI)I unlambda

    …… ``s`kii Iota …… * と i だけ Jot …… 0 と 1 だけ
  20. Lazy K ॲཧܥ ためしになにか動かしてみる $ lazy eg/calc.lazy $ lazy -e

    SKK 中身を見るともっとたのしい SKI を組み合わせて、君だけの最強 プログラムを作ろう!