CSLMNtal (仮) チュートリアル

アトムは一般的なグラフのノードに相当する概念です。アトムは名前といくつかの 引数 を持ちます。引数とは、直感的にはエッヂを差し込む差し込み口と考えることができます。引数の個数を、そのアトムの 価数 と呼ぶことがあります。名前が a であるような０価の (引数を持たない) アトムを次のように表現します。

a.

アトムの名前は次のいづれかです：

• 小文字アルファベットから始まる識別子 (atom, ok? など)
• 整数 (-5, 2014 など)

• 引用符で囲まれた任意の文字列 (​'this is an atom'​, ​'>>='​ など)

リンクはアトムの２つの引数を結びつけるもので、一般的なグラフのエッヂに相当する概念です。リンクは大文字アルファベットから始まる識別子で表現します。たとえば、２つの１価アトム a, b があり、これらが１本のリンクで接続されていることを次のように表現できます。

a(X), b(X).

リンクは同じアトム中の２つの引数を接続することもできます。

a(X, X).

同じリンク名は１つのグラフ中で必ず２度出現しなければなりません。たとえば次のようなグラフは、リンク Y の接続先が決まらないためエラーです。

a(X, Y), b(X).

ただし、あるグラフの真部分グラフについて考えるときには、リンク名が１度しか出現しないことがあります。たとえば上のグラフは、次のグラフ

a(X, Y), b(X), c(Y).

の部分グラフとしては適切なものです。このとき、リンク Y は上の部分グラフで 自由リンク であるといいます。他方、リンク X はこの部分グラフの中で閉じている 局所リンク と呼ばれます。

リンクの名前はグラフの構造において本質的ではないので、局所リンク名を改名して得られるグラフは同じものとみなします。たとえば次の２つのグラフは等価です。

a(X), b(X).

a(Y), b(Y).

２つの２価アトム a, b が２本のリンクで (２重に) 接続されていることを

a(X, Y), b(X, Y).

あるいは

a(X, Y), b(Y, X).

と表現できます。

CSLMNtal では一般的なグラフと異なり、引数の順序を区別します。したがって上の２つの表現はそれぞれ別のグラフを表すものです。より現実的な例としては、たとえば次のような抽象構文木のノード

if(Test, Then, Else), ...

が

if(Test, Else, Then), ...

から区別されます。

２価の ​'='​ アトムには特別な意味があり、これに接続された２つのリンクをあたかも１つのリンクであるかのようにみなします。たとえば次のグラフ

a(X), b(Y), '='(X, Y).

は

a(X), b(X).

と等価です。逆にこのようなグラフがあったとき、勝手に ​'='​ アトムを補って

a(X), b(Y), '='(X, Y)

とみなしても構いません。

いくつかの演算子 (四則演算, mod, ​'='​ など) は、前置記法や中置記法で表記することができます。たとえば

'='(X, Y).

を

X = Y.

と表記することができます。

次のグラフ

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

本ページで公開している処理系では、次の構文

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

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.

CSLMNtal では、書き換えルールを :- 演算子によって表現します。たとえば次の書き換えルール

a :- b.

は、「０価の a アトムを見つけたらこれを b に書き換えてよい」ことを表します。

このルールに続けてアトム a をいくつか含むグラフを入力すれば、

a, a, a.

これは次のように書き換えられ、停止するでしょう。

a, a, a.
--> b, a, a.
--> b, b, a.
--> b, b, b.

ルールの左辺・右辺は空でもかまいません。たとえば次のルール

:- a.

は「 a アトムを好き勝手に増やしてよい」ことを表します。あるいは次のルール

a :- .

は「 a アトムを好き勝手に消してよい」ことを表します。

適用することのできるルールが複数ある場合には、そのうちどのルールが最初に適用されるかは規定されません (非決定性)。これによって、実行経路が一つに決まらないようなシステムを簡単に記述することができます。

一つのルールの中で、同じリンク名はちょうど２回出現しなければなりません。出現の仕方ごとに、例とその意味を挙げます。

a(X, X) :- a

左辺に２回 … 書き換えの過程でリンクが削除される

a :- a(X, X)

右辺に２回 … 書き換えの過程でリンクが生成される

a(X) :- b(X)

１回づつ … 書き換えの過程でリンクの接続先が変わる

CSLMNtal では、マッチするグラフを具体的に指定する代わりに、そのグラフの満たすべき性質 ( 型 と呼びます) を述べることでルールを記述することもできます。たとえば次のルール

a(X), $x[X] :- int($x) | a.

は、アトム a に任意の整数アトム（名前が整数であるような１価アトム）が接続されているとき、この整数アトムを削除します。このルールにおいて、不特定多数の整数アトムを代表している $x を プロセス文脈 と呼びます。 $ から始まる任意の識別子をプロセス文脈として用いることができます。プロセス文脈の引数リストは () でなく [] で書かれる点に注意してください。

プロセス文脈にも略記法を用いることができます。たとえば上のルールの左辺は

a($x) :- ...

と書くこともできます。

プロセス文脈が代表できるグラフは単一のアトムに限られません。たとえば次のルール

$x[a, b] :- connected($x) | .

は、１価のアトム a, b を含む連結グラフを削除します。

CSLMNtal では、プロセス文脈の各引数の接続先は具体的なアトムでなければなりません。たとえば次のようなルールはエラーです。

$x[$y] :- connected($x), connected($y) | .

$x[X] :- atom($x) | a(X).

また、プロセス文脈には必ず型を指定しなければなりません。

プロセス文脈に指定することのできる型には、次のようなものがあります。

int

１価で名前が整数であるようなアトム

例： $x[X] = 14(X)

atom

単一のアトム (２価の ​'='​ アトムを除く)

例： $x[X, Y] = a(Y, X)

linked

２価の ​'='​ アトム (⇔ ２つの引数が実は単一のリンク)

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

​'<'​

２つの int のペアで、１つ目の方がその値が小さいもの (​'<='​, ​'>'​, ​'>='​, ​'='​ も同様)

例： $x[X, Y] = 3(X), 20(Y)

​'=='​

２つの等価な atom のペア

例： $x[X1, X2, Y1, Y2] = a(X1, X2), a(Y1, Y2)

​'==='​

２つの等価な 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'.

と書くことができます。

CSLMNtal では、次のような記法で型をユーザー定義することができます。

typedef list(X) {
    X = [].
    X = [H|T] :- atom(H), list(T).
}

この定義を次のように読むことができます：

リンク X に list 型のグラフが接続されているとは、

• X に空リストアトム [] が接続されているか
• １つのアトム H と、残りのリスト T のコンスが接続されている

ことである

型定義は相互再帰的でもかまいません。

２価以上のプロセス文脈に対する型も同様に定義できます。たとえば、差分リスト ( nil で終端されていないリスト) 型を次のように定義することができます。

typedef dlist(Head, Tail) {
    Head = Tail.
    Head = [H | T] :- atom(H), dlist(T, Tail).
}

このように自由リンクを２つ以上持つデータを自然に扱うことができるのは LMNtal (や Prolog) の特色です (たとえば代数データ型でこのような型を自然に定義することは難しいでしょう)。

型定義が１つのルールのみによってなされる場合、たとえば次のような型定義

typedef my_int(X) { :- int(X). }

は、波括弧を省略することができます。

typedef my_int(X) :- int(X).

「型 a を持たず、型 b を持つ」のような複雑な型検査をするために、本ページで公開している処理系ではルールに else if 節を持たせることができます。

ルールの右辺に次のように波括弧が書かれたとき、

integer?($x) :- {
    int($x) | yes.
    ground($x) | no.
}

型検査が上から順に試され、初めて成功したところで書き換えが行われます。

実用上、単純なアトムとリンクの繋ぎ替えだけでなく、算術演算などを行いたい場面は少なくありません。このような特別な計算のために、いくつかのアトムが予約されています。

たとえば次のルール：

X = succ($x) :- int($x) | X = $x + 1.

は、アトム succ に接続されている整数アトムの値に１を加えます。

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) システムルールが用意されています。

あるシステムをモデリングするにあたって、実装上必要ではあるけれどシステムにとって本質的ではないようなルールを書かねばならないことはあります。このとき、そのルールをシステムルールとして、他のルールとは別のレベルで適用することができます。これは、たんにトレースを見やすくするだけでなく、たとえば将来的に処理系にモデル検査器が組み込まれた場合に、検査の対象をシステムのより本質的な部分に限定するためにも有効です。

あるルールをシステムルールとするためには、ルールの先頭に define を付けます。

define a :- b.

このシステムルールのもとでは、０価の a アトムはただちに b アトムに置き換えられます。したがって０価の a アトムを見ることはもうないでしょう。

システムルールの左辺は空であってはいけません。たとえば次のような CSLMNtal プログラム

define :- a.

はひたすら a アトムを生産し続けるシステムルールではなく、 define アトムを a アトムに置き換える通常のルールと解釈されます。

継続について簡単に紹介します。すでにご存知の方は次の節に進んでいただいて構いません。

ある計算の継続とは、その計算の結果を使ってこれから行うべき計算の全体です。たとえば、次の式

(- (+ 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))) の継続は「その結果から１を引く」ことです。これを引数として、関数 (lambda (c) (c 1)) が呼ばれます。

継続はあたかも一引数関数かのように呼び出すことができます。継続に引数が渡され呼び出されると、その引数に対して「これからするべき計算」を行い、その結果を式全体の評価値とします。たとえば上の例では、受け取った継続 c に 1 を渡しています。継続 c は「その結果から１を引く」という「これからするべき計算」を表していたのですから、これに 1 を渡した結果は 0 です。これが式全体の評価値となります。

継続を用いた簡単な例外処理の例を挙げます。

(define (succ x ret)
  (if (integer? x)
      (+ x 1)
      (ret 0)))

関数 succ は２つの引数を受け取ります。第一引数は整数 x で、第二引数はエラー時に呼び出される一引数関数 ret です。与えられた引数がほんとうに整数であればこれに１を加えて返しますが、そうでなければ ret を 0 で呼び出します。

この succ の定義のもとで、次の式

(+ (call/cc (lambda (cc) (+ (succ 1 cc) 1))) 1)

を評価することを考えます。 (call/cc (lambda (cc) ...)) は、「その時点での継続を cc として ... を評価する」と読めます。したがってこの式を、「『その結果に１を足す』という継続を cc として、式 (+ (succ 1 cc) 1) を評価する」と読めます。 1 は整数なので、 (succ 1 cc) は 2 に評価されます。従って (call/cc (lambda (cc) ...)) 全体として値は (+ 2 1) すなわち 3 です。この結果に１を足せば、値は 4 です。

  (+ (call/cc (lambda (cc) (+ (succ 1 cc) 1))) 1)
;;   ~~~~~~~~~~~~~~~~~~~ 3 ~~~~~~~~~~~~~~~~~~~

では次の式ではどうでしょう。

(+ (call/cc (lambda (cc) (+ (succ "1" cc) 1))) 1)

この式は「『その結果に１を足す』という継続を cc として、式 (+ (succ "1" cc) 1) を評価する」と読めます。先程の例とは異なり、 succ の第一引数が文字列になっていますから、 (succ "1" cc) は失敗し、代わりに継続 cc が 0 で呼び出されます。 cc は「その結果に１を足す」という計算を表していたのですから、全体として値は 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 ... になります。対して、継続の例ではその戻り先が引数で与えられます。

例外に限らず、大域脱出やコルーチンなどの制御構造も継続によって説明することができます。

ダウンロード

まず、のちに継続を導入することを考えて、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).

ダウンロード

継続は、文脈そのものです。たとえば次の簡約規則

において、継続とはまさに 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].

ダウンロード

継続が文脈全体を取り出すのに対して、文脈のさらに一部分だけを取り出すのが部分継続です。例として次のような 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]].