Haskell でラムダ式を簡約させてみる - 3

Haskell でラムダ式を簡約させてみる - 1 - pragma666の日記
Haskell でラムダ式を簡約させてみる - 2 - pragma666の日記


前回は自由変数の判定を行う関数を定義した。次はβ簡約の中心的な役割を担う、λ項の置換を定義する。

置換の定義

再び Hindley の教科書からの引用。置換を以下のように定義している:

定義 1.12 置換
[N/x] M について、M に含まれる x を N に置換した結果を以下に定義する：

(a) [N/x] x       = N
(b) [N/x] a       = a                   ; a は x 以外の変数、または定数
(c) [N/x] (P Q)   = ([N/x]P [N/x]Q)
(d) [N/x] (λx.P) = λx.P
(e) [N/x] (λy.P) = λy.P               ; if x /= FV(P)
(f) [N/x] (λy.P) = λy.[N/x]P          ; if x <= FV(P) && y /= FV(N)
(g) [N/x] (λy.P) = λz.[N/x][z]y]P     ; if x <= FV(P) && y <= FV(N)

ここで (e)〜(g) において y != x であり、(g) における z は FV(N P)に含まれない(新しい) 変数である。

置換はλ計算の中心的な役割を担う重要な定義である。多くの数学の論文と同じく、一連の定義、定理が続いて最後にアルゴリズムの全貌が示される、というのが Hindley の教科書のスタイルである。しかしそれでは置換の意味を理解するのがしんどいので少し先走って説明すると、

(λx.x)

というλ項は、C 言語風に書くなら

int func( int x )
{
    return x;
}

つまり入力をそのまま返す関数を示す。
C 言語では

func(y);

などして関数を呼び出す。関数 func() は y をそのまま返すので実行すると、この式は

y;

と意味的に同じである。
λ式で入力をそのまま返す処理(無名関数)を表現しようとすると (λx.x) となる。λの直後に続く x は仮引数の名前で、ドットの後に処理が書かれる。処理は x だけなので、すなわち x が返る、と読める。
func(y) に相当する関数の"呼び出し" (適用) は以下のように無名関数の後に実引数を書く：

(λx.x)y

このλ式を計算すると (λx.x) の引数 x に y が代入され、代入された値すなわち y が返るので計算結果は y となる。
ここで計算というキーワードを使ったが、単一のλ項を考えた場合、簡約とは要は、仮引数の実引数への置換である。以降、簡約を (λx.x)y -> y のように矢印 -> で示す。

さて、置換の定義に戻ると、

(a) [N/x] x = N

(a) は単純に、M = x なので、x を N に置換すれば N である。(λx.x) N -> N となる例。

(b) [N/x] a = a

(b) は M (= a) にそもそも x が含まれない。よって a のまま。(λx.a) N -> a となる例。

(c) [N/x] (P Q) = ([N/x]P [N/x]Q)

(c) は定義 1.1 ラムダ項に出てくる application に置換を適用した話をしている。P と Q それぞれに置換を実施して、application してね、という定義。

(d) [N/x] (λx.P) = λx.P

(d) は少し難しい例。λx.P における x とは、関数の仮引数名のようなものである、と先ほど述べた。例えば引数に +1 した数を返す関数を C 風に書くなら

int suc( int x ) { return x + 1 }

ここで x という名前は(所詮は仮の引数なので) 別に y でも z でも N にしても、関数としての意味は変わらない。

int suc( int N ) { return N + 1 }

しかし、意味は全く変わらないので x を N に置換する意味は無い。置換を行う意味が無いので (d) では置換を行わない。

(e) [N/x] (λy.P) = λy.P

(e)〜(g) は前提として M にあたるλ式の仮引数が x ではなく y である点に注意である。
(e) は、条件として x が P の自由変数では無い、としている。つまり x は P の中にまったく出現しないか、または束縛変数として出現するかのどちらかである。まず、まったく出現しない場合は置換の必要が無い。次に x が P の束縛変数の場合を考える。ここで、x を置換するべきか、しないべきか。定義 (e) は置換しない、と言っている。束縛されている、ということは既に独立したスコープを持つことを示している。よって置換してはならない。または置換しても意味が無い。
以下のようなλ式が、(e) の例である：

[z/x] λy.y         --> λy.y           ; x は含まれない
[z/x] λy.(λx.xx)   --> λy.(λx.xx)   ; x は束縛変数として含まれる
(f) [N/x] (λy.P) = λy.[N/x]P

(f) は、P に x は自由変数として含まれ、N に y が自由変数として含まれないケースである。自由変数、つまり誰にも束縛されていないため x について置換をする。

[z/x] λy.x --> λy.z
(g) [N/x] (λy.P) = λz.[N/x][z]y]P

(g) は P に x が自由変数として出現し、N に y が自由変数として出現するケースである。まず仮引数名として使用されている y を、未使用な名前の変数 z に置換する。次に x を置換する。

[y/x] λy.xy --> [y/x] λz.xz --> λz.yz

Haskell による実装

先ほどの定義を多少プログラムっぽく書き直すと

-- Definition of Substitution
--
--      N      M
-- (a) [N/x] Var x       = N
-- (b) [N/x] a           = a
-- (c) [N/x] (App P Q)   = ([N/x]P [N/x]Q)
-- (d) [N/x] (Lam x P)   = Lam x P
-- (e) [N/x] (Lam y P)   = Lam y P               ; if x /= FV(P)
-- (f) [N/x] (Lam y P)   = Lam y [N/x]P          ; if x <= FV(P) && y /= FV(N)
-- (g) [N/x] (Lam y P)   = Lam z [N/x][z/y]P     ; if x <= FV(P) && y <= FV(N)

まず (a), (b) の Haskell による定義：

-- subst   M          x       N     empty
subst_i (Var n)     (Var x)   nt      e
    | n == x    = nt
    | otherwise = (Var n)

empty e は、(g) に出てくる自由変数を定義するためにある。(g) 以外では使わない。
(c) の定義は以下：

subst_i (App t1 t2) (Var x) nt      e
                = App (subst t1 (Var x)  nt) (subst t2 (Var x) nt)

次に (d) 〜 (g) の定義：

subst_i (Lam y p)   (Var x) nt      e
    | y == x                                    = (Lam y p)
    | not (elem x (fv p))                       = (Lam y p)
    | (elem x (fv p)) && (not (elem y (fv nt))) = (Lam y (subst p (Var x) nt))
    | (elem x (fv p)) && (elem y (fv nt))       = (Lam e (subst (subst_i p (Var y) (Var e) (e + 1))
                                                                  (Var x) nt ))

(g) の例(最後の定義) で、empty の e に +1 をしていることで、新たな自由変数を作っている。
最後に、これらを呼び出す元の関数の定義。

subst t1 t2 t3  = subst_i t1 t2 t3 (maximum ((fv t1) ++ (fv t2) ++ fv(t3)) + 1)

置換の式 [N/x] M について、t1 = M, t2 = x, t3 = N である。
Hindley の体後と順番が違うのでわかりにくいが、

subst 元のλ式　置換ターゲット　置換内容

みたいな感じで読むといいかも。
subst_i に渡す e は、subst の引数となる項の変数(というか数字) の最大値をもとに作成している。

subst 例

(a), (b) の例：

> subst (Var 0) (Var 0) (Var 1)
Var 1
> subst (Var 1) (Var 0) (Var 2)
Var 1

例によって数字で変数を表現しているので分かりにくいが Var 0 を V0 という変数として見立てると
最初の例は、「V0 というλ式に出てくる V0 を V1 に置き換えて」
という意味である。
ふたつ目の例は「V1 というλ式に出てくる V0 を V2 に置き換えて」
次は (c) の例：

> subst (App (Var 0) (Var 1)) (Var 0) (Var 2)
App (Var 2) (Var 1)

続いて(d) の例：

> subst (Lam 3 (App (Var 3) (Var 3))) (Var 3) (Var 4)
Lam 3 (App (Var 3) (Var 3))

(e) の例：

> subst (Lam 0 (App (Var 0) (Var 0))) (Var 1) (Var 2)
Lam 0 (App (Var 0) (Var 0))

(f) の例：

> subst (Lam 0 (App (Var 0) (Var 1))) (Var 1) (Var 2)
Lam 0 (App (Var 0) (Var 2))

最後に(g)の例：

> subst (Lam 2 (App (Var 0) (App (Var 1) (Var 2)))) (Var 1) (Var 2)
Lam 3 (App (Var 0) (App (Var 2) (Var 3)))

Haskell でラムダ式を簡約させてみる - 1

ラムダ式について勉強する機会があったのでメモ。

ラムダ計算について前々から興味はあったのだが、残念ながら日本語による良質な書籍を私は知らない。ので勉強した内容をまとめてみました。
ラムダ計算の名を冠した本に高橋正子先生の本がある。

計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座)

計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座)

しかし合流性に関する議論が多く、例えばラムダ式で自然数を表現するとか、ラムダ式で足し算を実装するとか、ラムダ式で再帰式を記述する、というようなトピックは無い。
この記事では、ラムダ式を独自に定義した型で表現し、簡約（インタプリタによる実行）するエンジンを Haskell で実装する。

準備

ghc をインストールする。
https://www.haskell.org/ghc/download
current stable をクリックし、バイナリをダウンロードして適当なディレクトリに解凍、パスを通せば良い。
Windows の場合は DOS 窓で

C:\Users\hal>ghci
GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
Prelude>

となればインストールは成功である。
Cygwin でも使えないことはないが、矢印キーによる履歴の呼び出しやタブ補完が利かないので、Dos 窓で実行するほうが良い。

自然数の表現

Haskell で簡約エンジンを実装する前に、自然数についての簡単な例を挙げておく。
自然数にはれっきとした定義があり、古くは1900年代のペアノ、デーデキント等の著書にその定義が見受けられる。ペアノによる著書では、自然数の公理として5つが挙げられており、そのうちの2つを引用すると：

  • ゼロは自然数である。( = Z とする )
  • ある自然数の、次の数 が存在する。( = 次の数を表す関数 successor を S とする )

アラビア数字とペアノの定義による自然数は、以下のように対応可能である：

0 : Z
1 : S(Z)
2 : S(S(Z))
3 : S(S(S(Z)))
...

これを Haskell で実装してみる。まず、自然数 N の定義は以下となる：

Prelude> data N = Z | S N deriving Show

この式は、
自然数 N とは、「ゼロである(=Z)」または「自然数 N の次の数( = S )である」
という意味である。
S N という記述に注目すると、これはデータが再帰的になっていることを示す。
この型 N を定義すると、以下のように上で挙げたペアノの定義による自然数を表現可能となる。

Prelude> Z
Z
Prelude> S(Z)
S Z
Prelude> S(S(Z))
S (S Z)
Prelude> S(S(S(Z)))
S (S (S Z))

足し算

これからは、peano.hs というファイルに Haskell のプログラムを書いて実行してみる。
ghc を

Prelude> :quit
Leaving GHCi.

で抜け、適当なエディタで peano.hs を作る。

peano.hs :

data N = Z | S N deriving Show

add Z     y = y
add (S x) y = S (add x y)

この定義はデーデキントの著作より拝借した。

数とは何かそして何であるべきか (ちくま学芸文庫)

数とは何かそして何であるべきか (ちくま学芸文庫)

最初の式は、ゼロに y を足しても、答えは y であることを定義している。
（定義というか、置き換え可能、と考えたほうが分かりやすいかも）
次の式はゼロ以外の数字を y を足した定義である。
例として、2 + 1 を考える。
2 = S (S Z)
1 = S Z
であるので、2 + 1 は以下のように置き換え可能である：

  add (S (S Z)) (S Z)
= S ( add (S Z) (S Z))
= S ( S ( add Z (S Z)))
= S ( S ( S Z ) )

答えは S (S (S Z)) つまり 3 である。

Haskell で実行してみる。
DOS 窓からファイルを指定して ghci を起動する。

C:\Users\hal>ghci -i peano.hs

実際に足し算させてみると、

> add (S (S Z)) (S Z)
S (S (S Z))
> add (Z) (S Z)
S Z
> add (S Z) (S(S Z))
S (S (S Z))
> add (S(S Z)) Z
S (S Z)

ちゃんと計算されている。

後々の記事では、λ式で自然数を表現し、足し算や引き算等を実装する予定である。

Haskell でラムダ式を簡約させてみる - 2

Haskell でラムダ式を簡約させてみる - 1 - pragma666の日記

ここからはラムダ式を Haskell で表現していく。
そのためには幾つかの定義が必要だが、全ての定義は Hindley の著書 Lambda-Calculus and Combinators: An Introduction から拝借させて頂いた。

Lambda-Calculus and Combinators: An Introduction

Lambda-Calculus and Combinators: An Introduction

この本は(洋書ではあるが)ステップを踏んでラムダ式が何であるか説明があるので、お勧め。前述した高橋先生の著書では、ラムダ式の説明は2ページそこそこであるが、この本では1章をまるまる使っての説明となる。

ラムダ項

ここからは Hindley による定義を、Haskell で実装していく。

定義 1.1 ラムダ項
(a) 全ての変数と定数はラムダ項である
(b) M と N がラムダ項であれば (M N) はラムダ項である( application )
(c) M がラムダ項で x が変数であれば (λx.M) はラムダ項である

例：

(a) (λv0.(v0 v00))
(b) (λx.(x y))
(c) ((λy.y)(λx.(x y)))
(d) (x(λx.(λx.x)))
(e) (λx.(y z))

上記はすべてラムダ項である。

Haskell による定義は以下：

-- Definition of Term
--
data Term = 
    Var Int
  | App Term Term 
  | Lam Int Term deriving Show

変数は Var 1, Var 2 のように示す。
x, y のように文字列を使っても良いのだが、ユニークであれば何でも良いので数字にした。数字のほうが入力しやすいし。
以下は Haskell で定義したラムダ項の例である：

> Var 0
Var 0
> Var 1
Var 1
> App (Var 1) (Var 2)
App (Var 1) (Var 2)
> Lam 0 (App (Var 0) (Var 1))
Lam 0 (App (Var 0) (Var 1))
> (App (Lam 0 (App (Var 0 ) (Var 1))) (Lam 0 (Var 0)))
App (Lam 0 (App (Var 0) (Var 1))) (Lam 0 (Var 0))

x を Var 0, y を Var 1, z を Var 2 に見立てると、上の例は上から x, y, x z, λx.x y, (λx.x y)(λx.x) の意味となる。

自由/束縛変数

続いて Hindley の本では、自由/束縛変数についての定義が続く。

定義1.11 自由/束縛変数
λ項 P に出現する変数 x を以下のように定義する：
1. P に含まれる λy.M の M に x が含まれる場合、bound
2. P に λx.M が含まれる場合、bound and binding
3. それ以外、x は free = 自由変数

例：

(((x v)(λy.(λz.(y v))))w)

左から順に、x, v は free.
次の y は bound and binding,
z も bound and binding,
次の y は、この項より前に出てくるλy.() のスコープなので bound,
v は free, w は free.

P に含まれる全ての自由変数を関数 FV(P) で得られるとすると、

FV(((x v)(λy.(λz.(y v))))w) = {x, v, w}

となる。
別の例で

FV((λy.y x(λx.y(λy.z)x))v w) = {x, z, v, w}

この例では、x は複数回出現し、出現する位置によって bound, bound and binding, free となるが FV は全ての自由変数を返す関数であるため x は FV の返り値に含まれる。

少しプログラムっぽく FV を定義すると、以下のようになる：

-- --------------------------------------------------------------------
-- Definition of FV
--
-- FV(M) =   {M}                if M is Var
--         | FV(M1) U FV(M2)    if M = App M1 M2
--         | FV(N) / {x}        if M = Lam x.N
--

Haskell による定義は以下：

fv_i (Var m)     = m : []
fv_i (App m1 m2) = fv_i m1 ++ fv_i m2
fv_i (Lam x n)   = [ v | v <- fv_i n, v /= x]

uniq [] = []
uniq (x :xs) | elem x xs     = uniq xs
             | otherwise     = x : uniq xs

fv (t) = uniq (fv_i t)

> let t1 = (Lam 0 (Var 0))
> fv(t1)
[]
> let t2 = (Lam 0 (Var 1))
> fv(t2)
[1]

数字ではやはり少し見にくいので多少工夫をすると

gv (Var n)  = n

v   = Var 1
w   = Var 2
x   = Var 3
y   = Var 4
z   = Var 5

これらを定義した後で

> let t3 = (App (App v w) (App (Lam (gv x) (App x y)) (App (Lam (gv y) (App z y)) z) ))
> fv(t3)
[1,2,4,5]

変数を数字に置き換えてるので分かりにくいが、これは

FV((v w) ((λx.x y)((λy.z y)z))) = [v w y z]

のことである。よって自由変数は x (= 3) 以外の v, w, y, z となる。

RM と EDF を awk で実装する

代表的なハードリアルタイムスケジューリングアルゴリズムである RM ( Rate Monotonic ) と EDF ( Earliest Deadline First ) を awk で実装してみた。

https://sourceforge.net/projects/rmvsedf/
git clone git://git.code.sf.net/p/rmvsedf/code rmvsedf-code

スケジューリングの勉強をしている方なら経験があるかもわからないが、意外と良いタスクセットの例を作るのが難しい。方眼紙やエクセルでスケジューリングの例を作っては、「意図通りに振る舞ってくれなかった」「実はスケジュール可能じゃなかった」と気づくことが多く、時間の無駄である。



$ cat ./samples/task_set2.txt

# RM  ... miss

# EDF ... schedulable
t1 = { 2, 5 }

t2 = { 4, 7 }

こんなタスクセットに対して、



$ awk -f ./sched.awk ./samples/task_set2.txt | awk -f show.awk

t1 = { 2, 5 }

t2 = { 4, 7 }

Utilization U = 0.971429
t1       : |X X _ _ _|X X _ _ _|X X _ _ _|X X _ _ _|X X _ _ _|X X _ _ _|X X _ _ _|X _ _

t2       : |_ _ X X X _ _|X X X _ _ X _|X _ _ X X X _|_ X X X _ _ X|X X _ _ X X _|_ _ _

         :               ^

         :               |

         :               +--- DEADLINE MISS at period 7

RM だとスケジュール出来ないが、



hal@cobich-VAIO ~/src/rmvsedf-code

$ awk -f ./sched.awk -v edf=1 ./samples/task_set2.txt | awk -f show.awk

t1 = { 2, 5 }

t2 = { 4, 7 }

Utilization U = 0.971429
t1       : |X X _ _ _|_ X X _ _|_ _ X X _|X X _ _ _|X X _ _ _|_ X X _ _|X X _ _ _|X _

t2       : |_ _ X X X X _|_ X X X X _ _|X _ _ X X X _|_ X X X X _ _|X X _ _ X X _|_ _

EDF だとスケジュール可能。


この例は Buttazzo の Hard Real-Time Computing Systems 3rd Edition の Figure-4.13 から拝借した。

この本は RM、EDF だけでなく、サーバアルゴリズムも（静的優先度、動的優先度別に）まとめられている良書である。

yices, awk, ocaml を使って秒速で数独を解く

awk yices

yices という SMT Solver を使って、数独を秒速で解いてみた。

http://sourceforge.net/projects/ssyao/
git clone git://git.code.sf.net/p/ssyao/code ssyao-code

数独を解くための制約式を awk （と勉強を兼ねて ocaml ）で作ってやり、yices にその式を解かせる、というもの。

まず yices のインストール。
http://yices.csl.sri.com/
っといってもダウンロードして解凍し、パスを通せば良い。

awk/ocaml へ渡す入力はこんな感じ：

$ cat input_1.txt
11  5
12  3
15  7
21  6
24  1
25  9
26  5
32  9
33  8
38  6
41  8
45  6
49  3
51  4
54  8
56  3
59  1
61  7
65  2
69  6
72  6
77  2
78  8
84  4
85  1
86  9
89  5
95  8
98  7
99  9

この入力は wikipedia のを拝借した。
http://en.wikipedia.org/wiki/Sudoku

これを sudoku_solver.awk に食わせると：

$ awk -f sudoku_solver.awk input_1.txt
(define x11 :: int)
(define x12 :: int)
...
(define x98 :: int)
(define x99 :: int)
(assert
	(and
		(<= 1 x11) (<= x11 9)
		(<= 1 x12) (<= x12 9)
...
		(<= 1 x98) (<= x98 9)
		(<= 1 x99) (<= x99 9)
		(distinct x11 x12 x13 x14 x15 x16 x17 x18 x19)
...
		(distinct x91 x92 x93 x94 x95 x96 x97 x98 x99)
		(distinct x11 x21 x31 x41 x51 x61 x71 x81 x91)
...
		(distinct x19 x29 x39 x49 x59 x69 x79 x89 x99)
		(distinct x11 x12 x13 x21 x22 x23 x31 x32 x33)
...
		(distinct x77 x78 x79 x87 x88 x89 x97 x98 x99)
		(= x11 5)
		(= x12 3)
		(= x15 7)
		(= x21 6)
		(= x24 1)
		(= x25 9)
		(= x26 5)
		(= x32 9)
		(= x33 8)
		(= x38 6)
		(= x41 8)
		(= x45 6)
		(= x49 3)
		(= x51 4)
		(= x54 8)
		(= x56 3)
		(= x59 1)
		(= x61 7)
		(= x65 2)
		(= x69 6)
		(= x72 6)
		(= x77 2)
		(= x78 8)
		(= x84 4)
		(= x85 1)
		(= x86 9)
		(= x89 5)
		(= x95 8)
		(= x98 7)
		(= x99 9)
))
(check)
(show-model)

こんな感じで、yices へ入力する制約式を吐き出す。制約とは、

  • 各マスに入る数字は1?9
  • 行、列に並ぶ数字は重複してはいけない
  • 3x3のマトリックスの中の数字も重複してはいけない

の3つと、最初から数字が決まってるマスの情報。

あとはこれを yices へ渡してやると：

$ awk -f sudoku_solver.awk input_1.txt > to_yices.txt
$ yices to_yices.txt
sat
(= x56 3)
(= x59 1)
(= x61 7)
(= x18 1)
(= x33 8)
(= x98 7)
(= x71 9)
(= x86 9)
(= x62 1)
(= x35 4)
(= x48 2)
(= x65 2)
(= x52 2)
(= x74 5)
(= x25 9)
(= x82 8)
(= x11 5)
(= x44 7)
(= x39 7)
(= x49 3)
(= x54 8)
(= x77 2)
(= x91 3)
(= x79 4)
(= x94 2)
(= x83 7)
(= x38 6)
(= x95 8)
(= x87 6)
(= x28 4)
(= x53 6)
(= x21 6)
(= x81 2)
(= x45 6)
(= x46 1)
(= x64 9)
(= x58 9)
(= x43 9)
(= x42 5)
(= x31 1)
(= x73 1)
(= x24 1)
(= x36 2)
(= x72 6)
(= x16 8)
(= x97 1)
(= x99 9)
(= x69 6)
(= x17 9)
(= x89 5)
(= x26 5)
(= x92 4)
(= x93 5)
(= x85 1)
(= x37 5)
(= x68 5)
(= x23 2)
(= x96 6)
(= x32 9)
(= x41 8)
(= x51 4)
(= x88 3)
(= x75 3)
(= x13 4)
(= x27 3)
(= x67 8)
(= x34 3)
(= x76 7)
(= x63 3)
(= x84 4)
(= x15 7)
(= x55 5)
(= x66 4)
(= x29 8)
(= x47 4)
(= x57 7)
(= x14 6)
(= x78 8)
(= x12 3)
(= x19 2)
(= x22 7)

見難いので整形すると：

$ yices to_yices.txt > result.txt
$ sort result.txt  | awk '{ printf( "%d ", $3); if ( (NR % 9) == 0) printf( "\n" )
;}'
5 3 4 6 7 8 9 1 2
6 7 2 1 9 5 3 4 8
1 9 8 3 4 2 5 6 7
8 5 9 7 6 1 4 2 3
4 2 6 8 5 3 7 9 1
7 1 3 9 2 4 8 5 6
9 6 1 5 3 7 2 8 4
2 8 7 4 1 9 6 3 5
3 4 5 2 8 6 1 7 9
0

こんな感じ。
1秒かからずに解ける。

ちなみに yices はヤイクスと発音するらしい。色々応用出来そう。

TinySCHEME のソースを読む -5　define の例

scheme

TinySCHEME のソースを読む -1　セルの構造
TinySCHEME のソースを読む -2　シンボル、環境
TinySCHEME のソースを読む -3　TinySCHEME の処理エンジン
TinySCHEME のソースを読む -4　トップレベルからの処理の流れ
TinySCHEME のソースを読む -5　define の例
tsdbg TinyScheme 用デバッグ extension

define の例

最後に、

    (define (my-sum x y) (+ x y))

がどのようなデータで表現されていくのかを簡単にメモ。

1. OP_EVAL まで

評価される直前、(define (my-sum x y) (+ x y)) は以下の形のセルで表現される。

2. define の評価

シンボル define は syntax であるため、OP_EVAL で評価されたセルは OP_DEF0 に渡される。
ここでは、define された関数が (lambda (x y) (+ x y)) に置き換わる。
lambda に置き換わったセルは以下のように表現される：

3. クロージャへ

lambda に置き換わったセルは、さらにクロージャへ変換される。
OP_LAMBDA1 の mk_closure() がこの処理を行う。

4. 環境に関数を追加

OP_DEF1 で、現在の環境に関数を slot として追加する。
slot は以下の形になる：

TinySCHEME のソースを読む -4　トップレベルからの処理の流れ

scheme

TinySCHEME のソースを読む -1　セルの構造
TinySCHEME のソースを読む -2　シンボル、環境
TinySCHEME のソースを読む -3　TinySCHEME の処理エンジン
TinySCHEME のソースを読む -4　トップレベルからの処理の流れ
TinySCHEME のソースを読む -5　define の例
tsdbg TinyScheme 用デバッグ extension

処理の流れ

ここからは、トップレベルからの処理の流れを、オペレーション毎におおまかにメモ。

OP_T0LVL

このオペレーションが最初に呼ばれる。
s_save() で、OP_T0LVL( 自分自身 ), OP_VECTOR, OP_T1LVL を dump に積んでおき、OP_READ_INTERNAL に s_goto() する。

OP_READ_INTERNAL

トークンを得る処理。
sc->tok に token() の戻り値を代入する。
EOF なら終了処理へ。
そうでなければ、OP_RDSEXPR へ s_goto()

OP_RDSEXPR

入力された sc->tok の評価を行い、まだ読み続けるか、それとも戻るか判断する。
OP_RDSEXPR からさらに処理が分かれる場合があるが、最終的に戻るオペレーションは（ OP_RDSEXPR が最初に呼ばれた時点で一番最後に dump に積まれている）OP_T1LVL である。

OP_RDLIST

リストを作る処理である。作られたリストは sc->args へ代入される。

OP_T1LVL

eval するための準備をする。
OP_T1LVL が呼ばれた時点で、sc->value には入力されたプログラムが入っている。
sc->value を sc->code に代入し、OP_EVAL へ s_goto()

OP_EVAL, OP_REAL_EVAL

eval が評価するのは、sc_code である。
1. code がシンボルなら、envir からシンボルの値をひっぱってきて返す
2. code が cons セルなら、code の car 部に注目する
2.1 code の car 部が syntax の場合、syntax のオペレーションへ s_goto() する
( if、lambda, define 等が syntax である)
2.2 syntax で無ければ、s_save() でOP_E0ARGS へ処理を引き継ぐ。code を code の car 部に更新し、OP_EVAL を続ける
3. code がシンボルでも cons セルでもなければ、そのまま返す

OP_E0ARGS, OP_E1ARGS

引数を一つ一つ評価していく。評価し終えた引数のリストは sc->args に格納され、OP_APPLY へ。

OP_APPLY

sc->code が何であるかにより処理が分かれるが、ここではユーザが定義した関数など、T_CLOSURE のセルの場合のみ説明する。
OP_APPLY は新しい環境を作る。
そして、code (プログラム)で定義された引数と、実際にユーザが与えた引数から slot を作り、環境へ追加する処理を行う。

たとえば、(my-sum 1 2) を呼び出した場合の envir は以下のようになる：

処理は OP_BEGIN に引き継ぎ、OP_BEGIN、OP_EVAL で評価された値が戻される、というのを繰り返す。
次に OP_EVAL に処理が移ったとき、x と y はそれぞれ新しい環境において、上図のように実際の値を含んだ状態で定義されている。
よって eval は、x と y の値を envir からひっぱってきて返すことが出来るのである。