あどけない話

Internet technologies

賢人鳥

分かった! 分かった! 分かった!

自己言及

ものまね鳥(M)は、自己言及する鳥なんだ!

Haskell では、型推論がジャマして、ものまね鳥を実現できない。

-- Mx = xx
m x = x x -- エラーになる

ヒバリ(L)も実現できない!

-- Lxy = x(yy)
l x y = x (y y) -- エラーになる

当然の帰結として、Haskell では再帰を使わないと賢人鳥(Y)を実現できない!

賢人鳥1

wikipediaの Y コンビネーターに書かれている最初の賢人鳥はこう。

(define Y
  (lambda (f)
    ((lambda (x) (f (lambda (y) ((x x) y))))
     (lambda (x) (f (lambda (y) ((x x) y)))))))

これは SLL だ!

;; Sxyz = xz(yz)
(define S (lambda (x) (lambda (y) (lambda (z) ((x z) (lambda (w) ((y z) w)))))))
;; Lxy = x(yy)
(define L (lambda (x) (lambda (y) (x (lambda (z) ((y y) z))))))
;; Y = SLL
(define Y ((S L) L))

賢人鳥2

wikipediaの Y コンビネーターに書かれている二番目の賢人鳥はこう。

(define Y
  ((lambda (x) (lambda (y) (y (lambda (z) (((x x) y) z)))))
   (lambda (x) (lambda (y) (y (lambda (z) (((x x) y) z)))))))

説明にあるように、これはチューリング鳥を使った UU。

;; Uxy = y(xxy)
(define U (lambda (x) (lambda (y) (y (lambda (z) (((x x) y) z))))))
;; Y = UU
(define Y (U U))

賢人鳥3

The Little Schemer に出てくる賢人鳥はこう。

(define Y
  (lambda (le)
    ((lambda (f) (f f))
     (lambda (f) (le (lambda (x) ((f f) x)))))))

これは BML だ!

;; Bxyz = x(yz)
(define B (lambda (x) (lambda (y) (lambda (z) (x (lambda (w) ((y z) w)))))))
;; Mx = xx
(define M (lambda (x) (x x)))
;; Lxy = x(yy)
(define L (lambda (x) (lambda (y) (x (lambda (z) ((y y) z))))))
;; Y = BML
(define Y ((B M) L))

面倒だけど、代入すれば、ちゃんと変形できる。

The Little Schemer (The MIT Press)

The Little Schemer (The MIT Press)

HaskellでScheme

ついに、Write Yourself a Scheme in 48 Hoursをやりました。

分ったこと

以下のことが、なんとなく分ったり、少なくともどう使うのかを体験できました。

  • エラー処理
    • 正常系の値と異常系の値を包含する型を作って、Scheme の関数はそれを返すようにする
  • モナド変換子
  • クロージャの実装

コードの問題点

ファイルとして置いてあるコードですが、以下のような小さな問題があります。

  • 2箇所Texのコマンドが残っている
parseString = do char ;\textcolor{string}{\texttt{'"'}};
  • cdr の定義が間違っている
cdr [DottedList (_ : xs) x] = return $ DottedList xs x
cdr [DottedList [xs] x] = return x

は誤りで、正しくはこう。

cdr [DottedList [xs] x] = return x
cdr [DottedList (_ : xs) x] = return $ DottedList xs x

でも、こう書く方が、もっと分りやすいと思います。

cdr [DottedList [_] x] = return x
cdr [DottedList (_ : xs) x] = return $ DottedList xs x
  • Haskell 98 にない forall が使われている

ghci を使う場合は、ファイルの先頭に以下を入れるといいです。

{-# LANGUAGE ExistentialQuantification #-}

独自拡張

大域の環境とクロージャの環境を表示する Scheme の関数を作ってみました。それぞれ、(show) と (closure "関数名") です。

eval env (List [Atom "show"]) = do pairs <- liftIO $ readIORef env
                                   return $ String $ unwords $ map fst pairs

eval env (List [Atom "closure", String name]) =
    do func <- getVar env name
       pairs <- liftIO $ readIORef $ closure func
       return $ String $ unwords $ map fst pairs

以下のようにクロージャを作って、

(define acm (lambda (n) (lambda (m) (+ n m))))
(define plus1 (acm 1))

以下のようにクロージャの環境を表示してみると

(closure "plus1") 

n が積まれていることが分ります。

おまけ

Hugs では動かないことが分りました。素直に GHC を使いましょう。

The Little Schemer

最近、Scheme がちょっとした流行になっているようです。

Scheme を勉強しようと思っている人に、僕が声を大にして薦めたい本は、「The Little Schemer」です。

The Little Schemer (The MIT Press)

The Little Schemer (The MIT Press)

1章から7章にかけて、たくさんの例題とともに「再帰」が説明されています。「再帰再帰」も勉強できます。実際、「この本を読んで人生が変わった」という感想を何回か聞いたことがあります。なぜなら、物事を再帰で考えられるようになるからです。再帰が分らない人は、ぜひ読んで下さい。

8章は、「クロージャ」や「継続」が出て来て、毛色が変わります。まぁ、なんとかついて行けるでしょう。

しかし、9章で「Yコンビネータ」が出てくると、もう大変です。実際、「Yコンビネータ」が何なのか知っていないと、内容の難しさに興味が保てず挫折してしまいます。

10章では、SchemeSchemeインタープリタを実装する話です。Lisp 1.5 Programmer's Manual を読んだことのない人には、「ふーん」で終わってしまうかもしれません。

という訳で、9章と10章について、ちょっとだけ解説しておきます。挫折した人が、再び興味を取り戻すのに役に立てば嬉しいです。

9章

Y コンビネータは、関数名を使わずに再帰を実現するための補助関数です。こんな感じです。

(lambda (le)
  ((lambda (f) (f f))
   (lambda (g) (le (lambda (x) ((g g) x))))))

たとえば、リストの長さを算出する関数を再帰で定義したいとします。しかし、関数名は使ってはいけません。どうしますか? Y コンビネータに与えることを前提にすると、次のように書けます。

(lambda (length)
  (lambda (l)
    (cond
     ((null? l) 0)
     (else
      (add1 (length (cdr l)))))))

length は、関数名ではなく、引数名であることに注意して下さい。

これを Y コンビネータに与えると、ちゃんと再帰します。

(((lambda (le)
    ((lambda (f) (f f))
     (lambda (g) (le (lambda (x) ((g g) x))))))
  (lambda (length)
    (lambda (l)
      (cond
       ((null? l) 0)
       (else
	(add1 (length (cdr l))))))))
 '(boo foo woo))
 3

すごいですね!

10章

Lispインタープリタは、データを読み、評価し、結果を出力するという作業を繰り返します。それらを実現する関数は、read、eval、print です。この繰り返しを REPL (read-eval-print loop) と呼ぶことがあります。

10章は、read と print は Scheme に任せ、eval の部分を実装してみようという話です。作る関数名は、eval ではなく、value になっていますけど。

evlis や evcon という関数が出てきますが、これは Lisp 1.5 Programmer's Manual に出てくる由緒正しい関数です。:)

実装する value がどの程度の能力があるのかよく理解していませんでしたが、今日コードを入力して実験したところ、上記の Y コンビネータも動きました。

(value 
 '(((lambda (le)
      ((lambda (f) (f f))
       (lambda (g) (le (lambda (x) ((g g) x))))))
    (lambda (length)
      (lambda (l)
	(cond
	 ((null? l) 0)
	 (else
	  (add1 (length (cdr l))))))))
   '(boo foo woo)))

いやー、びっくりです。

コードを入力するのは僕だけで十分ですから、参考までそのコードを載せておきます。いろんなところに、print を挿入して、いろいろ実験してみて下さい。(apply は apply1、:atom? は *atom? に変更しています。)

(define first car)
(define second
  (lambda (p) (car (cdr p))))
(define third
  (lambda (p) (car (cdr (cdr p)))))

(define atom?
  (lambda (x)
    (and (not (pair? x)) (not (null? x)))))

(define build
  (lambda (s1 s2) (cons s1 (cons s2 '()))))
(define new-entry build)

(define add1 (lambda (n) (+ n 1)))
(define sub1 (lambda (n) (- n 1)))

(define lookup-in-entry
  (lambda (name entry entry-f)
    (lookup-in-entry-help
     name
     (first entry)
     (second entry)
     entry-f)))

(define lookup-in-entry-help
  (lambda (name names values entry-f)
    (cond
     ((null? names) (entry-f name))
     ((eq? (car names) name)
      (car values))
     (else
      (lookup-in-entry-help
       name
       (cdr names)
       (cdr values)
       entry-f)))))

(define extend-table cons)

(define lookup-in-table
  (lambda (name table table-f)
    (cond
     ((null? table) (table-f name))
     (else
      (lookup-in-entry
       name
       (car table)
       (lambda (name)
	 (lookup-in-table
	  name
	  (cdr table)
	  table-f)))))))

(define expression-to-action
  (lambda (e)
    (cond
     ((atom? e) (atom-to-action e))
     (else
      (list-to-action e)))))

(define atom-to-action
  (lambda (e)
    (cond
     ((number? e) *const)
     ((eq? e #t) *const)
     ((eq? e #f) *const)
     ((eq? e (quote cons)) *const)
     ((eq? e (quote car)) *const)
     ((eq? e (quote cdr)) *const)
     ((eq? e (quote null?)) *const)
     ((eq? e (quote eq?)) *const)
     ((eq? e (quote atom?)) *const)
     ((eq? e (quote zero?)) *const)
     ((eq? e (quote add1)) *const)
     ((eq? e (quote sub1)) *const)
     ((eq? e (quote number?)) *const)
     (else *identifier))))

(define list-to-action
  (lambda (e)
    (cond
     ((atom? (car e))
      (cond
       ((eq? (car e) 'quote)
	*quote)
       ((eq? (car e) 'lambda)
	*lambda)
       ((eq? (car e) 'cond)
	*cond)
       (else 
	*application)))
     (else
      *application))))

(define value
  (lambda (e)
    (meaning e '())))

(define meaning
  (lambda (e table)
    ((expression-to-action e) e table)))

(define *const
  (lambda (e table)
    (cond
     ((number? e) e)
     ((eq? e #t) #t)
     ((eq? e #f) #f)
     (else
      (build 'primitive e)))))

(define *quote
  (lambda (e table)
    (text-of e)))

(define text-of second)

(define *identifier
  (lambda (e table)
    (lookup-in-table e table initial-table)))

(define initial-table
  (lambda (name)
    (car '())))

(define *lambda
  (lambda (e table)
    (build 'non-primitive
	   (cons table (cdr e)))))

(define table-of first)
(define formals-of second)
(define body-of third)

(define evcon
  (lambda (lines table)
    (cond
     ((else? (question-of (car lines)))
      (meaning (answer-of (car lines)) table))
     ((meaning (question-of (car lines)) table)
      (meaning (answer-of (car lines)) table))
     (else
      (evcon (cdr lines) table)))))

(define else?
  (lambda (x)
    (cond
     ((atom? x) (eq? x 'else))
     (else #f))))
(define question-of first)
(define answer-of second)

(define *cond
  (lambda (e table)
    (evcon (cond-lines-of e) table)))

(define cond-lines-of cdr)

(define evlis
  (lambda (args table)
    (cond
     ((null? args) '())
     (else
      (cons (meaning (car args) table)
	    (evlis (cdr args) table))))))

(define *application
  (lambda (e table)
    (apply1
     (meaning (function-of e) table)
     (evlis (arguments-of e) table))))

(define function-of car)
(define arguments-of cdr)

(define primitive?
  (lambda (l)
    (eq? (first l) 'primitive)))

(define non-primitive?
  (lambda (l)
    (eq? (first l) 'non-primitive)))

(define apply1
  (lambda (fun vals)
    (cond
     ((primitive? fun)
      (apply-primitive (second fun) vals))
     ((non-primitive? fun)
      (apply-closure (second fun) vals)))))

(define apply-primitive
  (lambda (name vals)
    (cond
     ((eq? name 'cons)
      (cons (first vals) (second vals)))
     ((eq? name 'car)
      (car (first vals)))
     ((eq? name 'cdr)
      (cdr (first vals)))
     ((eq? name 'null?)
      (null? (first vals)))
     ((eq? name 'eq?)
      (eq? (first vals) (second vals)))
     ((eq? name 'atom?)
      (*atom? (first vals)))
     ((eq? name 'zero?)
      (zero? (first vals)))
     ((eq? name 'add1)
      (add1 (first vals)))
     ((eq? name 'sub1)
      (sub1 (first vals)))
     ((eq? name 'number?)
      (number (first vals))))))

(define *atom?
  (lambda (x)
    (cond
     ((atom? x) #t)
     ((null? x) #f)
     ((eq? (car x) 'primitive) #t)
     ((eq? (car x) 'non-primitive) #t)
     (else #f))))

(define apply-closure
  (lambda (closure vals)
    (meaning (body-of closure)
	     (extend-table
	      (new-entry
	       (formals-of closure)
	       vals)
	      (table-of closure)))))

Scheme でλ計算(2)

昨日の続き。今日はチャーチ数です。

ZERO と ONE

ZERO と ONE の定義は簡単です。

;; 0 := λf x. x
(define ZERO (lambda (f x) x))
;; 1 := λf x. f x
(define ONE (lambda (f x) (f x)))

SUCC

SUCC の定義も、昨日の CONS が分れば、同じようにできます。

;; SUCC := λn f x. f (n f x)
(define SUCC (lambda (n) (lambda (f x) (f (n f x)))))

難しいのは、ONE と (SUCC ZERO) が等しいか調べることです。二つの理由により、equal? では比較できません。

  • そもそも Scheme の仕様では、equal? で lambda 式を比較したときの動作は定義されていません。
  • SUCC は二重に lambda を使っているので、帰ってくるのはクロージャです。n は展開されません。

Scheme の仕様には、関数の本体を取り出す関数が用意されてないようです。そこで、MIT Scheme の pp を使って ONE を表示してみます。

(pp ONE)
;; >> (lambda (f x) (f (n f x)))

期待した (lambda (f x) (f x)) という形にはなっていません。

しょうがないので、f に 1+、x に 0 を代入することで比較することにしました。

(ONE 1+ 0) ;; => 1
((SUCC ZERO) 1+ 0) ;; => 1

PLUS

PLUS は以下のように定義できます。

;; PLUS := λm n f x. m f (n f x)
(define PLUS (lambda (m n) (lambda (f x) (m f (n f x)))))

うまく動くか、実験してみます。

(define TWO (SUCC ONE))
(define THREE (SUCC TWO))
((PLUS TWO THREE) 1+ 0) ;; => 5

うまくいきました。\^^/

追記

MIT/GNU Scheme には 1+ がありますが、MzScheme や Gauche にはありませんので、以下の定義が必要です。

(define 1+ (lambda (x) (+ x 1)))

Scheme でλ計算

Wikipedia のラムダ計算にある例を Scheme で実行して理解してみます。

TRUE と FALSE

TRUE と FALSE は簡単です。

;; TRUE := λx y. x
(define TRUE (lambda (x y) x))
;; FALSE := λx y. y
(define FALSE (lambda (x y) y))

AND、OR、NOT

難しいのは、本体に x y z のように複数の変数が出てきたときです。これは、Scheme でいうと (x y z) という関数呼び出しのことらしいです。という訳で、AND、OR、NOT が定義できます。

;; AND := λp q. p q FALSE
(define AND (lambda (p q) (p q FALSE)))
;;; OR := λp q. p TRUE q
(define OR (lambda (p q) (p TRUE q)))
;; NOT := λp. p FALSE TRUE
(define NOT (lambda (p) (p FALSE TRUE)))

うまく動くか実験してみましょう。

(AND TRUE FALSE) ;; => FALSE
(AND TRUE TRUE) ;; => TRUE
(NOT TRUE) ;; => FALSE

IFTHENELSE

ここまでできれば、IFTHENELSE は簡単でした。

;; IFTHENELSE := λp x y. p x y
(define IFTHENELSE (lambda (p x y) (p x y)))
(IFTHENELSE TRUE 'THEN 'ELSE) => 'THEN
(IFTHENELSE FALSE 'THEN 'ELSE) => 'ELSE

CAR、CDR、CONS

さて、次の問題は CONS です。2つしか引数を取らないはずなのに、3つ取るようになっています。試行錯誤の上、こうしてみました。

;; CONS := λf s b. b f s
(define CONS (lambda (f s) (lambda (b) (b f s))))
;; CAR := λp. p TRUE
(define CAR (lambda (p) (p TRUE)))
;; CDR := λp. p FALSE 
(define CDR (lambda (p) (p FALSE)))

試してみると、うまくいきます。

(CAR (CONS 'A 'B)) ;; => 'A
(CDR (CONS 'A 'B)) ;; => 'B

ふぅ

疲れたので、今日はここまで。