CSLMNtal (仮) チュートリアル
Table of Contents
1 概要
Context-sensitive FlatLMNtal (仮称、以下 CSLMNtal と呼びます) は、 LMNtal を下敷きに設計されたプログラミング言語です。
LMNtal では、グラフと書き換えルールとを合わせた グラフ書換え系 としてプログラムを記述します。CSLMNtal はこれを拡張したもので、グラフの型を定義し、これを書き換えルール中で用いることができます。
本ページでは CSLMNtal のプロトタイプ処理系、チュートリアル、およびいくつかの例題とその解説を公開しています。
(このページは Emacs によって自動生成されたものです。次の url からプレーンテキストで読むこともできます:index.org)
2 プロトタイプ処理系
3 起動とコマンドの実行
$ gosh lmn.scm
で起動すると REPL が立ち上がります。
LMN>
REPL では、グラフ・書き換えルールと以下のコマンドを入力することができます。
:quit
- REPL を終了します
:reset
- 書き換えルール・型定義をすべてクリアします
:trace
- 書き換えの結果だけでなく過程を表示します(トグル)
グラフ・書き換えルールの記法と意味については後述します。
行内に %
があると、行末までをコメントとみなし無視します。
4 CSLMNtal チュートリアル
CSLMNtal でのプログラミングを簡単に説明します。形式的な意味論もありますが、ここでは省略します。論文 を参照してください。
「(拡張機能)」と書かれた項目は、形式意味論に含まれていない言語機能を表しています。
4.1 グラフの表現
CSFLatLMNtal では、 アトム と リンク によってグラフを表現します。以下で具体的な記法を紹介します。
4.1.1 アトム
アトムは一般的なグラフのノードに相当する概念です。アトムは名前といくつかの 引数 を持ちます。引数とは、直感的にはエッヂを差し込む差し込み口と考えることができます。引数の個数を、そのアトムの 価数 と呼ぶことがあります。名前が a
であるような0価の (引数を持たない) アトムを次のように表現します。
a.
アトムの名前は次のいづれかです:
- 小文字アルファベットから始まる識別子 (
atom
,ok?
など) - 整数 (
-5
,2014
など)
- 引用符で囲まれた任意の文字列 (
'this is an atom'
,'>>='
など)
4.1.2 リンク
リンクはアトムの2つの引数を結びつけるもので、一般的なグラフのエッヂに相当する概念です。リンクは大文字アルファベットから始まる識別子で表現します。たとえば、2つの1価アトム a
, b
があり、これらが1本のリンクで接続されていることを次のように表現できます。
a(X), b(X).
リンクは同じアトム中の2つの引数を接続することもできます。
a(X, X).
同じリンク名は1つのグラフ中で必ず2度出現しなければなりません。たとえば次のようなグラフは、リンク Y
の接続先が決まらないためエラーです。
a(X, Y), b(X).
ただし、あるグラフの真部分グラフについて考えるときには、リンク名が1度しか出現しないことがあります。たとえば上のグラフは、次のグラフ
a(X, Y), b(X), c(Y).
の部分グラフとしては適切なものです。このとき、リンク Y
は上の部分グラフで 自由リンク であるといいます。他方、リンク X
はこの部分グラフの中で閉じている 局所リンク と呼ばれます。
4.1.3 リンクの改名 (α-同値)
リンクの名前はグラフの構造において本質的ではないので、局所リンク名を改名して得られるグラフは同じものとみなします。たとえば次の2つのグラフは等価です。
a(X), b(X).
a(Y), b(Y).
4.1.4 引数の順序
2つの2価アトム a
, b
が2本のリンクで (2重に) 接続されていることを
a(X, Y), b(X, Y).
あるいは
a(X, Y), b(Y, X).
と表現できます。
CSLMNtal では一般的なグラフと異なり、引数の順序を区別します。したがって上の2つの表現はそれぞれ別のグラフを表すものです。より現実的な例としては、たとえば次のような抽象構文木のノード
if(Test, Then, Else), ...
が
if(Test, Else, Then), ...
から区別されます。
4.1.5 = アトム
2価の '='
アトムには特別な意味があり、これに接続された2つのリンクをあたかも1つのリンクであるかのようにみなします。たとえば次のグラフ
a(X), b(Y), '='(X, Y).
は
a(X), b(X).
と等価です。逆にこのようなグラフがあったとき、勝手に '='
アトムを補って
a(X), b(Y), '='(X, Y)
とみなしても構いません。
4.2 略記法
CSLMNtal には、簡単のためにいくつかの略記法が用意されています。これによって、複雑なグラフをも簡潔に表現することが可能です。
4.2.1 演算子
いくつかの演算子 (四則演算, mod
, '='
など) は、前置記法や中置記法で表記することができます。たとえば
'='(X, Y).
を
X = Y.
と表記することができます。
4.2.2 最終引数の省略
次のグラフ
a(X, Y), b(X), c(Z, Z, Y).
を、 c
アトムの最終引数を外に出して次のように表現することができます。
a(X, Y), b(X), Y = c(Z, Z).
また =
の一辺がリンク名であるとき、他辺を対応するリンク名のある場所に代入して次のように表現することができます。
a(X, c(Z, Z)), b(X).
b
アトムにも同様の略記法を用いると、このグラフは次のようにも表現できます。
a(b, c(Z, Z)).
あるいは、このグラフにふたたび最終引数のくくり出しを適用して
c(Z, Z) = a(b).
と書くこともできます。
この略記法により、たとえば次の抽象構文木
expr(X), if(Test, Then, Else, X), equal?(1, 1, Test), true(Then), false(Else).
を以下のように書くことができます。
expr = if(equal?(1, 1), true, false).
4.2.3 (拡張機能) 演算子のユーザー定義
本ページで公開している処理系では、次の構文
defop アトム名, 結合性, 結合力 (, 価数).
で演算子として扱う文字列を追加することができます。結合性は prefix
,
left
, right
のいずれかで、価数は prefix
な演算子に対してのみ指定できます。以下はユーザー定義演算子の例です。
defop '!', prefix, 101, 1. defop if, prefix, 99 , 3. defop '&', left, 100.
この演算子定義のもとで、たとえば次の文字列
if (!a & b) c d.
は次のグラフを表現していると解釈されます。
if('&'('!'(a), b), c, d).
4.2.4 リスト記法
CSLMNtal ではリストを、空リストを表すアトム '[]'
とリストへの要素の追加 (cons) を表すアトム '.'
によって次のように表現します:
list = '.'(a, '.'(b, '[]')).
アトム名に '[]'
および '.'
を用いるのはあくまで慣習であって、もちろん他の名前のアトム (たとえば、 cons
と nil
) によっても等価な構造を表現することができます。
list = cons(a, cons(b, nil)).
ただし、 '.'
, '[]'
によって表現されるリストには次のような略記法が用意されていて便利です:
list = [a, b].
また、空リストで終端されていないリスト (improper list) を表現するために、あるいはリストを先頭のいくつかの要素と残りのリストに分割するために、次のような記法を用いることができます。
list = [a, b, | X] :- list = X.
これは次のルールと等価です:
list = '.'(a, '.'(b, X)) :- list = X.
4.3 書き換えルールの表現
書き換えルールは、ある部分グラフを別の部分グラフで置き換えてよいことを処理系に伝えるものです。 CSLMNtal のプログラムは、グラフといくつかの書き換えルールとを並べたものになります。
4.3.1 基本
CSLMNtal では、書き換えルールを :-
演算子によって表現します。たとえば次の書き換えルール
a :- b.
は、「0価の a
アトムを見つけたらこれを b
に書き換えてよい」ことを表します。
このルールに続けてアトム a
をいくつか含むグラフを入力すれば、
a, a, a.
これは次のように書き換えられ、停止するでしょう。
a, a, a. --> b, a, a. --> b, b, a. --> b, b, b.
ルールの左辺・右辺は空でもかまいません。たとえば次のルール
:- a.
は「 a
アトムを好き勝手に増やしてよい」ことを表します。あるいは次のルール
a :- .
は「 a
アトムを好き勝手に消してよい」ことを表します。
適用することのできるルールが複数ある場合には、そのうちどのルールが最初に適用されるかは規定されません (非決定性)。これによって、実行経路が一つに決まらないようなシステムを簡単に記述することができます。
一つのルールの中で、同じリンク名はちょうど2回出現しなければなりません。出現の仕方ごとに、例とその意味を挙げます。
a(X, X) :- a
- 左辺に2回 … 書き換えの過程でリンクが削除される
a :- a(X, X)
- 右辺に2回 … 書き換えの過程でリンクが生成される
a(X) :- b(X)
- 1回づつ … 書き換えの過程でリンクの接続先が変わる
4.3.2 プロセス文脈
CSLMNtal では、マッチするグラフを具体的に指定する代わりに、そのグラフの満たすべき性質 ( 型 と呼びます) を述べることでルールを記述することもできます。たとえば次のルール
a(X), $x[X] :- int($x) | a.
は、アトム a
に任意の整数アトム(名前が整数であるような1価アトム)が接続されているとき、この整数アトムを削除します。このルールにおいて、不特定多数の整数アトムを代表している $x
を プロセス文脈 と呼びます。
$
から始まる任意の識別子をプロセス文脈として用いることができます。プロセス文脈の引数リストは ()
でなく []
で書かれる点に注意してください。
プロセス文脈にも略記法を用いることができます。たとえば上のルールの左辺は
a($x) :- ...
と書くこともできます。
プロセス文脈が代表できるグラフは単一のアトムに限られません。たとえば次のルール
$x[a, b] :- connected($x) | .
は、1価のアトム a
, b
を含む連結グラフを削除します。
4.3.3 プロセス文脈の制限
CSLMNtal では、プロセス文脈の各引数の接続先は具体的なアトムでなければなりません。たとえば次のようなルールはエラーです。
$x[$y] :- connected($x), connected($y) | .
$x[X] :- atom($x) | a(X).
また、プロセス文脈には必ず型を指定しなければなりません。
4.3.4 組込みのプロセス文脈型
プロセス文脈に指定することのできる型には、次のようなものがあります。
int
- 1価で名前が整数であるようなアトム
例:
$x[X]
=14(X)
atom
- 単一のアトム (2価の
'='
アトムを除く)例:
$x[X, Y]
=a(Y, X)
linked
- 2価の
'='
アトム (⇔ 2つの引数が実は単一のリンク) ground
- 引数のリンクから辿ることのできるアトム全体
例:
$x[X, Y, Z]
=a(X), b(Y), c(Z, d)
connected
- 内部が連結グラフになっているような
ground
例:
$x[X, Y, Z]
=a(b(X), Y, c(Z, d))
'<'
- 2つの
int
のペアで、1つ目の方がその値が小さいもの ('<='
,'>'
,'>='
,'='
も同様)例:
$x[X, Y]
=3(X), 20(Y)
'=='
- 2つの等価な
atom
のペア例:
$x[X1, X2, Y1, Y2]
=a(X1, X2), a(Y1, Y2)
'==='
- 2つの等価な
ground
のペア例:
$x[X1, X2, Y1, Y2]
=a(X1, b(X2)), a(Y1, b(Y2))
比較演算を扱いやすくするために、型は単一のプロセス文脈だけでなくプロセス文脈をカンマで並べたもの全体に対して指定することもできます。たとえば、
a(X), b(Y), $x[X, Y] :- '<'($x) | 'a is less than b'.
と書く代わりに
a($x), b($y) :- '<'($x, $y) | 'a is less than b'.
あるいはアトムの中置記法を援用して
a($x), b($y) :- $x < $y | 'a is less than b'.
と書くことができます。
4.3.5 型のユーザー定義
CSLMNtal では、次のような記法で型をユーザー定義することができます。
typedef list(X) { X = []. X = [H|T] :- atom(H), list(T). }
この定義を次のように読むことができます:
リンク
X
にlist
型のグラフが接続されているとは、
X
に空リストアトム[]
が接続されているか- 1つのアトム
H
と、残りのリストT
のコンスが接続されていることである
型定義は相互再帰的でもかまいません。
2価以上のプロセス文脈に対する型も同様に定義できます。たとえば、差分リスト ( nil
で終端されていないリスト) 型を次のように定義することができます。
typedef dlist(Head, Tail) { Head = Tail. Head = [H | T] :- atom(H), dlist(T, Tail). }
このように自由リンクを2つ以上持つデータを自然に扱うことができるのは LMNtal (や Prolog) の特色です (たとえば代数データ型でこのような型を自然に定義することは難しいでしょう)。
型定義が1つのルールのみによってなされる場合、たとえば次のような型定義
typedef my_int(X) { :- int(X). }
は、波括弧を省略することができます。
typedef my_int(X) :- int(X).
4.3.6 (拡張機能) else if 節を持つルール
「型 a
を持たず、型 b
を持つ」のような複雑な型検査をするために、本ページで公開している処理系ではルールに else if 節を持たせることができます。
ルールの右辺に次のように波括弧が書かれたとき、
integer?($x) :- { int($x) | yes. ground($x) | no. }
型検査が上から順に試され、初めて成功したところで書き換えが行われます。
4.3.7 (拡張機能) システムルール
実用上、単純なアトムとリンクの繋ぎ替えだけでなく、算術演算などを行いたい場面は少なくありません。このような特別な計算のために、いくつかのアトムが予約されています。
たとえば次のルール:
X = succ($x) :- int($x) | X = $x + 1.
は、アトム succ
に接続されている整数アトムの値に1を加えます。
eval(succ(succ(2))). --> eval(succ(3)). --> eval(4).
この例では、次のようなルール群が暗黙に適用されていると考えられます:
X = 2 + 1 :- x = 3. X = 3 + 1 :- x = 4. ...
このように、ルール適用と別のレベルで暗黙に適用されるルールをシステムルールと呼びます (CSLMNtal の元となった言語 LMNtal では、この用語をやや異なった意味で用いるので注意してください)。
本ページで配布されている処理系には、四則演算に加えて、剰余 mod(X, Y)
、ユニークな名前を持ったアトムの生成 gensym(X)
システムルールが用意されています。
4.3.8 (拡張機能) システムルールのユーザー定義
あるシステムをモデリングするにあたって、実装上必要ではあるけれどシステムにとって本質的ではないようなルールを書かねばならないことはあります。このとき、そのルールをシステムルールとして、他のルールとは別のレベルで適用することができます。これは、たんにトレースを見やすくするだけでなく、たとえば将来的に処理系にモデル検査器が組み込まれた場合に、検査の対象をシステムのより本質的な部分に限定するためにも有効です。
あるルールをシステムルールとするためには、ルールの先頭に define
を付けます。
define a :- b.
このシステムルールのもとでは、0価の a
アトムはただちに b
アトムに置き換えられます。したがって0価の a
アトムを見ることはもうないでしょう。
システムルールの左辺は空であってはいけません。たとえば次のような CSLMNtal プログラム
define :- a.
はひたすら a
アトムを生産し続けるシステムルールではなく、 define
アトムを a
アトムに置き換える通常のルールと解釈されます。
5 例題
本ページの処理系で動作確認に成功したいくつかの例題と、その解説を掲載します。
5.1 簡単な言語のモデリング
次のような言語を考えます:
\begin{array}{rcl} v & := & \mathit{< IntegerConstant >} \\ e & := & v \mid \mathtt{add}\ e\ e \end{array}この言語の式としてはたとえば次のようなものがあります(可読性のために括弧を補いました)。
add (add 1 2) (add 3 4)
この式の抽象構文木を、 CSLMNtal のグラフとしてたとえば次のように表現することができるでしょう。
expr = add(add(1, 2), add(3, 4)).
この言語のプログラムの意味が、次のような簡約規則によって定義されていたとします。
\begin{equation} \mathtt{add}\ v_1\ v_2 \rightarrow v_3\ (v_3 = v_1 + v_2) \end{equation}すなわち、 add がいわゆる整数の加算を表しているとします。これを CSLMNtal でモデリングすることは簡単です。
X = add($v1, $v2) :- int($v1), int($v2) | X = $v1 + $v2.
このルールのもとで、上の抽象構文木はたとえば次のように書き換えられます。
expr = add(add(1, 2), add(3, 4)). --> expr = add(3, add(3, 4)). --> expr = add(3, 7). --> expr = add(10).
あるいは、次のように書き換えられるかもしれません。
expr = add(add(1, 2), add(3, 4)). --> expr = add(add(1, 2), 7). --> expr = add(3, 7). --> expr = add(10).
5.2 簡単な言語の評価順序
「簡単な言語」に評価順序 (left-to-right) を導入してみます。このために、新たな構文規則として文脈 E を次のように定義します。
\begin{equation} E := [] \mid \mathtt{add}\ v\ E \mid \mathtt{add}\ E\ e \end{equation} \([]\) は Hole と呼ばれる特殊な終端記号です。この文法の生成する式には、たとえば次のようなものがあります
- add 1 []
- []
- add [] (add 2 (add 3 4))
一方、次のような式をこの文法は生成しません
- add (add 1 2) []
Hole を「次に計算してよい場所」と考えると、これは右オペランドよりも先に左オペランドを評価しなければならないことの表現になっています。
文脈 \(E\) を使って、「簡単な言語」の評価順序を含めた意味を次のように定義できます。
\begin{equation} E[\mathtt{add}\ v_1\ v_2] \rightarrow E[v_3]\ (v_3 = v_1 + v_2) \end{equation}ただし \(E[e]\) は文脈 \(E\) の Hole を式 \(e\) で置換して得られる式を表します。たとえば次のような簡約が可能です。
add [(add 1 2)] (add 2 (add 3 4)) → add [3] (add 2 (add 3 4))
他方、 add 3 4
を先に計算することはできません。なぜなら、そこに Hole
を作ることは \(E\) の文法上できないからです。
これを CSLMNtal でモデリングするために、ユーザー定義のプロセス文脈型を用いることができます。文脈 \(E\) に相当する型を次のように定義することができます。
typedef ctx(Redex, Body) { Body = Redex. Body = add(L, R) :- int(L), ctx(Redex, R). Body = add(L, R) :- ctx(Redex, L), ground(R). }
この型を用いて、書き換えルールを次のように書きなおすことができます。
expr = $e[add($v1, $v2)] :- int($v1), int($v2), ctx($e) | expr = $e[$v1 + $v2].
この書き換えルールのもとでは、計算の順序が一意に決まります。
5.3 より複雑な制御構造 … 継続、部分継続
Casey Klein, Jay McCarthy, Steven Jaconette, and Robert Bruce Findler: A Semantics for Context-Sensitive Reduction Semantics を参考に、継続・部分継続を持ったラムダ計算の例を CSLMNtal で記述してみます。
継続とは、ある時点でやり残した計算をすべてまとめたオブジェクトで、これによって大域脱出、例外処理、コルーチンなどさまざまな制御構造をすべて説明することができるようなものです。
部分継続の実装においては、加えて Oleg Kiselyov: How to remove a dynamic prompt も参考にしました。
5.3.1 継続の概要
継続について簡単に紹介します。すでにご存知の方は次の節に進んでいただいて構いません。
ある計算の継続とは、その計算の結果を使ってこれから行うべき計算の全体です。たとえば、次の式
(- (+ 1 1) 1)
の (+ 1 1)
を計算しているとき、継続は「その結果から1を引く」ことです。同様に、次の式
(- (- (+ 1 1) 1) 1)
で (+ 1 1)
を計算しているときの継続は、「その結果から1を引き、また1を引く」ことです。
Scheme などの持つ組み込み関数 call/cc
は、一引数関数を引数にとり、
call/cc
の継続をその関数に渡します。たとえば次の式
(- (call/cc (lambda (x) (x 1))) 1)
において、式 (call/cc (lambda (x) (x 1)))
の継続は「その結果から1を引く」ことです。これを引数として、関数 (lambda (c) (c 1))
が呼ばれます。
継続はあたかも一引数関数かのように呼び出すことができます。継続に引数が渡され呼び出されると、その引数に対して「これからするべき計算」を行い、その結果を式全体の評価値とします。たとえば上の例では、受け取った継続
c
に 1
を渡しています。継続 c
は「その結果から1を引く」という「これからするべき計算」を表していたのですから、これに 1
を渡した結果は 0
です。これが式全体の評価値となります。
継続を用いた簡単な例外処理の例を挙げます。
(define (succ x ret) (if (integer? x) (+ x 1) (ret 0)))
関数 succ
は2つの引数を受け取ります。第一引数は整数 x
で、第二引数はエラー時に呼び出される一引数関数 ret
です。与えられた引数がほんとうに整数であればこれに1を加えて返しますが、そうでなければ ret
を 0
で呼び出します。
この succ
の定義のもとで、次の式
(+ (call/cc (lambda (cc) (+ (succ 1 cc) 1))) 1)
を評価することを考えます。 (call/cc (lambda (cc) ...))
は、「その時点での継続を cc
として ...
を評価する」と読めます。したがってこの式を、「『その結果に1を足す』という継続を cc
として、式 (+ (succ 1 cc) 1)
を評価する」と読めます。 1
は整数なので、 (succ 1 cc)
は 2
に評価されます。従って (call/cc (lambda (cc) ...))
全体として値は (+ 2 1)
すなわち 3
です。この結果に1を足せば、値は 4
です。
(+ (call/cc (lambda (cc) (+ (succ 1 cc) 1))) 1) ;; ~~~~~~~~~~~~~~~~~~~ 3 ~~~~~~~~~~~~~~~~~~~
では次の式ではどうでしょう。
(+ (call/cc (lambda (cc) (+ (succ "1" cc) 1))) 1)
この式は「『その結果に1を足す』という継続を cc
として、式 (+ (succ "1" cc) 1)
を評価する」と読めます。先程の例とは異なり、 succ
の第一引数が文字列になっていますから、 (succ "1" cc)
は失敗し、代わりに継続
cc
が 0
で呼び出されます。 cc
は「その結果に1を足す」という計算を表していたのですから、全体として値は 1
です。
(+ (call/cc (lambda (cc) (+ (succ "1" cc) 1))) 1) ; => 1 ;; ~~~~~~~~~~~~~~~~~~~~ 0 ~~~~~~~~~~~~~~~~~~~~
これは次のような Common Lisp の例外処理
(defun succ (x) (if (integerp x) (+ x 1) (throw 'err 0))) (+ (catch 'err (+ (succ "1") 1)) 1)
に似ています。ただし、戻り先が動的に決まる点は異なります。すなわち、関数 succ
で例外 'err
が投げられたとき、その戻り先は直近の (catch 'err ...
になります。対して、継続の例ではその戻り先が引数で与えられます。
例外に限らず、大域脱出やコルーチンなどの制御構造も継続によって説明することができます。
5.3.2 ステップ1:left-to-right ラムダ計算
まず、のちに継続を導入することを考えて、left-to-right に評価されるラムダ計算を定義・モデリングします。このようなラムダ計算は、たとえば次のように定義できます。 succ
は自然数の後者関数です。
- 構文
\begin{array}{rcl} x & := & \mathit{< Identifier >}\\ v & := & \mathtt{lambda}\ x.e \mid \mathtt{succ} \mid \mathit{< NaturalConstant >}\\ e & := & e\ e \mid x \mid v \end{array}
- 評価文脈
\begin{equation} C := [] \mid C\ e \mid v\ C \end{equation}
- 意味論
\begin{array}{rcl} C[(\mathtt{lambda}\ x\ e_1)\ e_2] & \rightarrow & C[e1\{x/e_2\}]\\ C[\mathtt{succ}\ v] & \rightarrow & C[v + 1]\\ \end{array} (ただし \(e1\{x/e_2\}\) は \(e1\) の \(x\) に \(e_2\) を代入したもの)
これを CSLMNtal でモデリングすることは簡単です。「簡単な言語」と同じ要領で、定義をたんに CSLMNtal の記法に書き直すことができます。ただし、
subst
は代入を表すシステムルールとし、その定義は後述します。
% ---- Notations defop infix, '$', 900, left. % application % ---- Grammar % x := <Identifier> typedef x(L) :- atom(L). % v := lambda x.e ... abstraction % | succ ... successor function % | <IntegerConstant> ... constant typedef v(L) { L = lambda(X, E) :- x(X), e(E). L = succ. :- int(L). } % e := e e ... application % | x ... variable % | v ... value typedef e(L) { L = E1 $ E2 :- e(E1), e(E2). :- x(L). :- v(L). } % --- Evaluation Context % C := [] | C e | v C typedef c(Redex, Body) { Body = Redex. Body = C $ E :- c(Redex, C), e(E). Body = V $ C :- v(V), c(Redex, C). } % --- Reduction Rules % C[(lambda x.e1) e2] -> C[e1{x/e2}] expr = $c[lambda(X, E1) $ E2] :- c($c) | expr = $c[subst(E1, X, E2)]. % C[succ v] -> C[v + 1] expr = $c[succ $ $v] :- c($c), int($v) | expr = $c[$v + 1].
閉じたラムダ項だけを考えることにすれば、代入を表すシステムルール
subst
を次のように帰納的に定義できます。
% --- Substitution % (e1 e2){x/v} = e1{x/v} e2{x/v} define Ret = subst(E1 $ E2, $x, $v) :- ground($x, $v) | Ret = subst(E1, $x, $v) $ subst(E2, $x, $v). % (lambda x1 e){x2/v} = lambda x1 e (if x1 = x2) % | lambda x1 e{x2/v} (otherwise) define Ret = subst(lambda($x1, E), $x2, $v) :- { $x1 == $x2, ground($v) | Ret = lambda($x1, E). ground($x1, $x2, $v) | Ret = lambda($x1, subst(E, $x2, $v)). } % x1[x2/v] = v (if x1 = x2) % | x1 (otherwise) define Ret = subst($x1, $x2, $v) :- { $x1 == $x2, ground($v) | Ret = $v. atom($x1), ground($x2, $v) | Ret = $x1. }
試しに次のようなグラフを入力し、実行できることを確認してもよいでしょう。
expr(lambda(x, lambda(y, x $ y)) $ lambda(x, succ $ 2) $ 3).
5.3.3 ステップ2:継続
継続は、文脈そのものです。たとえば次の簡約規則
\begin{equation} C[\mathtt{succ}\ v] \rightarrow C[v + 1] \end{equation}において、継続とはまさに C のことです。この簡約規則によって式
(lambda x.x) (succ 3)
が
(lambda x.x) 4
と簡約されるとき、 C は
(lambda x.x) []
となっていますが、これはまさしく「関数 lambda x.x
を []
の評価結果で呼び出す」という、 (succ 3)
の継続になっています。したがって、継続を捉えることは文脈を複製することに、また継続を呼び出すことは捉えてあった文脈で現在の文脈を置き換えることにそれぞれ相当します。
このアイデアを形式的に表現すると次のようになります。
- 構文の拡張
\begin{equation} v := \cdots \mid \mathtt{call/cc} \mid \mathtt{cont}\ C \end{equation}
- 意味論の拡張
\begin{array}{rcl} C[\mathtt{call/cc}\ v] & \rightarrow & C[v\ (\mathtt{cont}\ C)]\\ C_1[(\mathtt{cont}\ C_2)\ v] & \rightarrow & C_2[v] \end{array}
これを CSLMNtal で記述することは難しくありません。
typedef v(L) { ... L = call_cc. L = cont(Hole, Body) :- c(Hole, Body). } % C[call/cc v] -> C[v (cont C)] expr = $c[call_cc $ $v] :- c($c), v($v) | expr = $c[$v $ cont(Hole, $c[Hole])]. % C_1[(cont C_2) v] -> C_2[v] expr = $c1[cont(Hole, $c2[Hole]) $ $v] :- c($c1), c($c2), v($v) | expr = $c2[$v].
5.3.4 ステップ3:部分継続
継続が文脈全体を取り出すのに対して、文脈のさらに一部分だけを取り出すのが部分継続です。例として次のような Scheme の式を考えます。
(+ (reset (+ (shift x (x (x 1))) 2)) 3)
(shift x ...)
はその時点の部分継続を x
として ...
を評価し、その値を reset
の評価値とするような構文です。これは reset
よりも内側で用いられます。上の例で項 (shift x (x (x 1)))
の継続は (+ (reset (+ [] 2)) 3)
ですが、部分継続はそのうち特に reset
よりも下の部分、すなわち (+ [] 2)
を言います。これを x
として (x (x 1))
を評価すると、その値は (+ (+ 1 2) 2)
すなわち 5
になります。これが reset
の評価値となるので、結果は全体として (+ 5 3)
すなわち 8
になります。
形式的には、文脈を「 reset
を含むかもしれない文脈」と「 reset
を含んではいけない文脈」とに分けることで部分継続を表現することができます。ここでは、ラムダ計算の枠組みに合わせるために、 (shift x ...)
の代わりに call/comp (lambda x ...)
のような構文を用いることにします。
- 構文の拡張
\begin{array}{rcl} v & := & \cdots \mid \mathtt{call/comp} \mid \mathtt{comp}\ M\\ e & := & \cdots \mid \mathtt{reset}\ e \end{array}
- 評価文脈
\begin{array}{rcl} M & := & [] \mid M\ e \mid v M\\ C & := & M \mid C[\mathtt{reset}\ M] \end{array}
- ルールの拡張
\begin{array}{rcl} C[\mathtt{reset}\ M[\mathtt{call/comp}\ v]] & \rightarrow & C[\mathtt{reset}\ (v\ (\mathtt{comp}\ M))]\\ C[\mathtt{reset}\ v] & \rightarrow & C[v]\\ C[(\mathtt{comp}\ M)\ v] & \rightarrow & C[\mathtt{reset}\ M[v]] \end{array}
これも CSLMNtal によって簡潔に記述することができます。
typedef v(L) { ... L = call_comp. L = comp(Hole, Body) :- m(Hole, Body). } typedef e(L) { ... L = reset $ E :- e(E). } typedef m(Redex, Body) { Body = Redex. Body = M $ E :- m(Redex, M), e(E). Body = V $ M :- v(V), m(Redex, M). } typedef c(Redex, Body) { :- m(Redex, Body). Redex2 = reset $ M :- c(Redex2, Body), m(Redex, M). } % C[reset M[call/comp v]] -> C[reset (v (comp M))] expr = $c[reset $ $m[call_comp $ $v]] :- c($c), m($m), v($v) | expr = $c[reset $ ($v $ comp(Hole, $m[Hole]))]. % C[reset v] -> C[v] expr = $c[reset $ $v] :- c($c), v($v) | expr = $c[$v]. % C[(comp M) v] -> C[reset M[v]] expr = $c[comp(Hole, $m[Hole]) $ $v] :- c($c), m($m), v($v) | expr = $c[reset $ $m[$v]].
5.4 循環データの表現
LMNtal の扱うデータはグラフですから、循環を含むようなデータをも自然に扱うことができます。たとえば次のルールは、長さが偶数であるような循環リストを2つの同じ長さの循環リストに分割します。
typedef same_length(XT, XH, YT, YH) { XH = XT, YH = YT. XH = [X|XS], YH = [Y|YS] :- ground(X), ground(Y), same_length(XT, XS, YT, YS). } YT = [X | $x[XT]], XT = [Y | $y[YT]] :- same_length($x, $y) | '.'(X, $x[XX], XX), '.'(Y, $y[YY], YY).
このルールとともにグラフ
X = [1, 2, 3, 4, 5, 6, 7, 8 | X].
を入力すると、たとえば次のように分解されていきます。
--> L1 = [1, 2, 3, 4, 5, 6, 7, 8 | L1] --> L1 = [1, 2, 3, 4 | L1], L2 = [5, 6, 7, 8 | L2]. --> L1 = [5, 8 | L1], L2 = [1, 2, 3, 4 | L2], L3 = [7, 6 | L3]. --> L1 = [5 | L1], L2 = [8 | L2], L3 = [1, 2, 3, 4 | L3], L4 = [7, 6 | L4]. --> L1 = [5 | L1], L2 = [8 | L2], L3 = [7 | L3], L4 = [1, 2, 3, 4 | L4], L5 = [6 | L5]. --> L1 = [5 | L1], L2 = [1, 4 | L2], L3 = [8 | L3], L4 = [7 | L4], L5 = [3, 2 | L5], L6 = [6 | L4]. --> L1 = [5 | L1], L2 = [1 | L2], L3 = [4 | L3], L4 = [8 | L4], L5 = [7 | L5], L6 = [3 | L6], L7 = [6 | L7]. --> L1 = [5 | L1], L2 = [1 | L2], L3 = [4 | L3], L4 = [8 | L4], L5 = [3 | L5], L6 = [7 | L6], L7 = [2 | L7], L8 = [6 | L8].