現在の位置
backup プラグインを使用中
- List of Backups
- View the diff.
- View the diff current.
- View the backup.
- Go to LMNtalチュートリアル.
- 1 (2009-11-12 (Thu) 15:18:40)
- 2 (2009-11-12 (Thu) 15:40:16)
- 3 (2009-12-27 (Sun) 16:01:16)
- 4 (2017-03-02 (Thu) 05:38:19)
http://www.ueda.info.waseda.ac.jp/lmntal/local/pukiwiki.php?doc_basic から一部抜粋 *簡単チュートリアル(by ayano) [#de9806de] **ルール [#x335d659] LMNtal の書き換え規則をルールと言う。ルールは (左辺) :- (右辺) という形をしていて、「左辺の形の物があったら右辺の形に書き換える」という意味。 &br; a. b. c. d. a. b. a. c. a. a :- z. ↓ アトム a を全て z に置き換える z. b. c. d. z. b. z. c. z. &br; a. b. c. d. a. b. a. c. a. a :- z. b :- z. ↓ アトム a と b を全て z に置き換える z. z. c. d. z. z. z. c. z. &br; さらに (左辺) :- (ガード) | (右辺) という形でガード(条件文)を書くことができる。 n(-2). n(-1). n(0). n(1). n(2). n(3). n(N) :- N<0 | n(0). ↓ 負の数ならば0にする n(0). n(0). n(0). n(1). n(2). n(3). &br; ガード(条件文)一覧 int(N) (Nがintなら) float(N) (Nがfloatなら) string(N) (Nがstringなら) unary(N) (Nが1つのアトムなら) ground(N) (Nより先が膜を含まないアトム集団なら) = (groundの比較: = ) /= (groundの比較: ≠ ) =:= (intの比較: = ) =/= (intの比較: ≠ ) < =< > >= (intの比較: < ≦ > ≧ ) =:=. (floatの比較: = ) =/=. (floatの比較: ≠ ) <. =<. >. >=. (floatの比較: < ≦ > ≧ ) &br; LMNtalは非決定に実行が行われるのが特徴である。(どれが実行されるかわからない。)~ SLIMのモデルチェック機能(MC)を使えばどのような状態が存在するか確認することができる。 a. a :- b. a :- c. というプログラムを実行すると b または c となる。 SLIMにオプション『--nd』を付けると 7247352::::b. @1 7247752::::c. @1 7237712::7247352,7247752::a. @1 と出力される。見方は 状態番号 :: 遷移先の状態番号 :: 状態 となっている。よってこれからも a は b か c になることがわかる。 SLIMにオプション『--nd_result』を付けて実行すると execution result: 0( 7237712): a. @1 1( 7247752): c. @1 execution result: 0( 7237712): a. @1 1( 7247352): b. @1 と、最終状態のパターンを出力してくれる。 **整数アトム [#xc9a2ac3] 整数アトムは n(1). のように書くことができる。 1(n). も同じ意味。 &br; 四則演算もできて n(1),n(2),n(3). n(A),n(B) :- N=A+B | n(N). ↓ n(6). となる。 &br; for文のようにしたいならば i(0). i(I) :- J=I+1,J<10 | n(I),i(J). ↓ n(0), n(1), n(2), n(3), n(4), n(5), n(6), n(7), n(8), i(9) とすることによって0~9までの数を生成することができる。 &br; これらを応用して、階乗を求めるプログラムを書くと fact(5). fact(N) :- N>1, M=N-1 | n(N), fact(M). fact(N) :- N=1 | . n(X), n(Y) :- N=X*Y | n(N). ↓ n(120). となる。 **膜 [#ze87e6f7] 膜は計算を局所化できる。 { n(1), n(2), n(3). n(A), n(B) :- N=A+B | n(N). }. { n(4), n(5), n(6). n(A), n(B) :- N=A+B | n(N). }. ↓ { n(6), @601 }, { n(15), @602 } &br; 膜の中でルールの適用ができなくなると実行される、というルールも書くことができる。 { $p,@p }/ :- $p. $p は膜の中にあるすべてのアトム、 @p は膜の中にあるすべてのルール、を表すので~ それぞれの膜で計算が進み、最後にルールが適用できなくなったらアトムだけ外に出すことを表している。 &br; よってこれを入れると { n(1), n(2), n(3). n(A), n(B) :- N=A+B | n(N). }. { n(4), n(5), n(6). n(A), n(B) :- N=A+B | n(N). }. { $p,@p }/ :- $p. ↓ n(6), n(15), @603 となる。 &br; さらに膜の外でも計算を行えば { n(1), n(2), n(3). n(A), n(B) :- N=A+B | n(N). }. { n(4), n(5), n(6). n(A), n(B) :- N=A+B | n(N). }. { n(7), n(8), n(9). n(A), n(B) :- N=A+B | n(N). }. { $p,@p }/ :- $p. // 計算が止まったら実行 n(A),n(B) :- N=A+B | n(N). ↓ n(45), @604 と、並列計算のようにさせることができる。 **リスト [#l3ae114a] リストは list = [1,2,3,4]. のように書くことができる。(シンタックスシュガーなので実状態をunyoで見ることをお勧めします。)~ ここから値を取り出すことができて list = [1,2,3,4]. list = [N|T] :- n(N), list = T. ↓ n(1), n(2), n(3), n(4), list([]), @601 と、順番に先頭から数字を取り出すことができる。 &br; また途中からアトムをとる事もできて list = [1,2,3,4]. L = [N|T] :- n(N), L=T. ↓ n(4), n(1), n(2), n(3), list([]), @601 となる。unyoで見るとわかるが、先頭から順にアトムを取り出してはいない。 &br; リストに値を追加するときは n(1),n(2),n(3). res = []. res = T, n(N) :- res = [N|T]. ↓ res([2,3,1]), @601 とすることで、値を先頭へ追加していくことができる。~ 順に先頭から追加されていったので、 1を追加 3を追加 2を追加 が行われたことになる。 (この例ではn(N)がどれにマッチするかわからないのでこのような追加の順番になっています。) 応用としてバブルソートを書くと L=[A,B|T] :- A>B | L=[B,A|T]. list([1, 3, 4, 6, 2, 5, 8, 7, 0]). ↓ list([0, 1, 2, 3, 4, 5, 6, 7, 8]). となる。 **さらに詳しい解説 [#pfcd80a0] http://www.ueda.info.waseda.ac.jp/lmntal/local/pukiwiki.php?doc_basic~ を見てください。~ または論文等を参照してください。 **旧LTLの話 [#r7edb905] SLIMのオプションには『--ltl』というモードもある。~ 例えば a. a :- b,b. b :- a. は無限に走ってしまうプログラムであるが、 いつかbのアトムが3つになるか調べたいときに init{ a. a :- b,b. b :- a. }. init{$p,@p} :- init{$p,@p}. init{b,b,b,$p,@p} :- accept_all_end{b,b,b,$p,@p}. と、書いて、『--ltl』で走らせると cycle(or error) found: 0: {init{a. @2}. @1} 1: {init{b. b. @2}. @1} 2: {init{a. b. @2}. @1} 3: {init{b. b. b. @2}. @1} 4: {accept_all_end{a. b. b. @2}. @1} と、状態遷移(サイクル)を見つけて表示してくれる。 『--ltl_all』を付けるとすべての状態遷移を見つけれくれる。~ (上の例だとbが3つになる状態遷移は無限にあるので止まらなくなる。) MCにはさらに機能があるので調べてみることを薦めます。