Prolog でわかる TAPL 4日目 - 第Ⅰ部 型無しの計算体系 (2)

ヘルメース

ヘルメース（古希: Ἑρμῆς、古代ギリシア語ラテン翻字: Hermēs）は、ギリシア神話に登場する青年神である[1]。長母音を省略してヘルメスとも表記される[1]。

オリュンポス十二神の一人。神々の伝令使、とりわけゼウスの使いであり、旅人、商人などの守護神である[1]。能弁、境界、体育技能、発明、策略、夢と眠りの神、死出の旅路の案内者などとも言われ、多面的な性格を持つ神である。その聖鳥は朱鷺および雄鶏。幸運と富を司り、狡知に富み詐術に長けた計略の神、早足で駆ける者、牧畜、盗人、賭博、商人、交易、交通、道路、市場、競技、体育などの神であるとともに、雄弁と音楽の神であり、竪琴、笛、数、アルファベット、天文学、度量衡などを発明し、火の起こし方を発見した知恵者とされた。プロメーテウスと並んでギリシア神話のトリックスター的存在であり、文化英雄としての面を有する。

ローマ神話におけるメルクリウス（マーキュリー）に相当する[1]。水星はギリシアではヘルメースの星といわれ、これはローマ人にも受け継がれた。現代ヨーロッパ諸語でメルクリウスに相当する語を水星に当てるのはこのためである。

今日は型無しラムダ計算を Prolog で実装します。

図5-3.型無しラムダ計算(λ)

→(型無し)

構文

t ::=     項：
  x       変数
  λx.t   ラムダ抽象
  t t     関数適用

v::=      値：
  λx.t   ラムダ抽象値


評価 t ==> t’

t1 ==> t1’
------------------------------------------ (E-App1)
t1 t2 ==> t1’ t2

t2 ==> t2’
------------------------------------------ (E-App2)
v1 t2 ==> v1  t2’

(λx.t12) v2 ==> [x->v2]t12                (E-AppAbs)

この図は、コアなラムダ計算の本質的部分のみを取り出したもので、メタな理論を議論するのに用いられています。
これをPrologで書くと以下のようになります:

プログラムの全体を見る

untyped.pl

:- style_check(-singleton).
:- op(920, xfx, [==>, ==>>]).
:- op(910, xfx, [/-]).
:- op(500, yfx, [$, !, subst, subst2]).
:- op(10, xf, [/]).

:- op(1200,xfx,::=), op(650,xfx,∈), op(250,yf,*).
G∈{G}. G∈(G|_). G∈(_|G1):-G∈G1. G∈G.
syntax(S/[S2],AEs) :- compound_name_arguments(AEs,A,Es),syntax(S,A),syntax(S2,Es).
syntax(G,E):-G=..[O|Gs],E=..[O|Es],maplist(syntax,Gs,Es),!.
syntax(G,E):-(G::=Gs),!,G1∈Gs,syntax(G1,E),!.
syntax(atom,I):- atom(I),!.

% ------------------------   SYNTAX  ------------------------

x ::= atom.        % 識別子:
m ::=              % 項:
      x            % 変数
    | (fn(x) -> m) % ラムダ抽象
    | m $ m        % 関数適用
    .
v ::=              % 値:
      fn(x) -> m   % ラムダ抽象
    . 

% ------------------------   SUBSTITUTION  ------------------------

            X![X -> M]  subst M              :- syntax(x,X).
            X![Y -> M]  subst X              :- syntax(x,X).
(fn(X) -> M2)![Y -> M]  subst (fn(X) -> M2_) :- M2![X, (Y -> M)] subst2 M2_.
      M1 $ M2![Y -> M]  subst (M1_ $ M2_)    :- M1![Y -> M] subst M1_, M2![Y -> M] subst M2_.
            A![Y -> M]  subst B              :- writeln(error : A![Y -> M] subst B), fail.
      M1![Y, (Y -> M)] subst2 M1.
      M1![X, (Y -> M)] subst2 M_             :- M1![Y -> M] subst M_.

% ------------------------   EVALUATION  ------------------------

Γ /- (fn(X) -> M12) $ V2 ==> R        :- syntax(v,V2), M12![X -> V2] subst R.
Γ /- V1 $ M2             ==> V1 $ M2_ :- syntax(v,V1), Γ /- M2 ==> M2_.
Γ /- M1 $ M2             ==> M1_ $ M2 :- Γ /- M1 ==> M1_.
Γ /- M                  ==>> M_       :- Γ /- M ==> M1, Γ /- M1 ==>> M_.
Γ /- M                  ==>> M.

% ------------------------   MAIN  ------------------------

run(X/, Γ/[X|Rs], [X - name | Γ]/Rs) :- !.
run(M, Γ/[M_|Rs], Γ/Rs) :- !, syntax(m,M), !, Γ /- M ==>> M_, !.
run(Ls,Rs)              :- foldl(run, Ls, []/Rs_, _/[]),!,Rs=Rs_.
run(Ls)                 :- run(Ls,Ms),writeln(Ms).

% ------------------------   TEST  ------------------------
:- begin_tests(untyped).
test(n):- run([x/, x],[x,x]). 
test(n):- run([(fn(x) -> x)],[(fn(x)->x)]). 
test(n):- run([(fn(x) -> x) $ (fn(x) -> x $ x)],[(fn(x)->x$x)]). 
test(n):- run([(fn(z) -> (fn(y) -> y) $ z) $ (fn(x) -> x $ x)],[(fn(x)->x$x)]). 
test(n):- run([(fn(x) -> (fn(x) -> x) $ x) $ (fn(x) -> x $ x)],[(fn(x)->x$x)]). 
test(n):- run([(fn(x) -> (fn(x) -> x) $ x) $ (fn(z) -> z $ z)],[(fn(z)->z$z)]).
:- end_tests(untyped).

:- run_tests.
:- halt.

項書換えをするための述語 subst/2 と subst2/2 で項内を一部置換します。X![X -> M] subst M :- x(X). の規則では変数XをMに書き換えます。Prologでは関数のつながりをそのまま書けないので $ 2項演算子を用いて関数適用を示しています。
OCamlの実装はド・ブラン・インデックス化するわけですが、図をそのまま動かすのであれば、代入、置換を行う処理を書かなければなりません。しかし、ド・ブラン・インデックス化をするにはプログラム読み込み時に変換処理が必要になります。どちらもそれなりの仕組みが必要となるので、一長一短と言えます。

プログラムの全体を見る

fulluntyped.pl

:- discontiguous((/-)/2).
:- op(1200, xfx, [:-]).
:- op(1100, xfy, [in]).
:- op(920, xfx, [==>, ==>>]).
:- op(910, xfx, [/-]).
:- op(600, xfy, [#]).
:- op(500, yfx, [$, !, subst, subst2]).
:- style_check(-singleton).

:- op(1200,xfx,::=), op(650,xfx,∈), op(250,yf,*).
G∈{G}. G∈(G|_). G∈(_|G1):-G∈G1. G∈G.
syntax(S/[S2],AEs) :- compound_name_arguments(AEs,A,Es),syntax(S,A),syntax(S2,Es).
syntax(G,E):-G=..[O|Gs],E=..[O|Es],maplist(syntax,Gs,Es),!.
syntax(G,E):-(G::=Gs),!,G1∈Gs,syntax(G1,E),!.
syntax(E*,Ls) :- maplist(syntax(E),Ls).
syntax(x,X):- \+syntax(w,X),atom(X),!.                % 識別子:
syntax(floatl,F)   :- float(F).                       % 浮動小数点数:
syntax(stringl,S)  :- string(S).                      % 文字列:
syntax(l,L)        :- atom(L) ; integer(L).           % ラベル:

% 構文

w ::= true | false | zero.                            % キーワード:
m ::=                   % 項:
      true              % 真
    | false             % 偽
    | if(m,m,m)         % 条件式
    | 0                 % ゼロ
    | succ(m)           % 後者値
    | pred(m)           % 前者値
    | iszero(m)         % ゼロ判定
    | floatl            % 浮動小数点数値
    | m * m             % 浮動小数点乗算
    | stringl           % 文字列定数
    | x                 % 変数
    | fn(x)->m          % ラムダ抽象
    | m $ m             % 関数適用
    | let(x)=m in m     % let束縛
    | {(l=m)*}          % レコード
    | m # l             % 射影
    .
n ::=                   % 数値:
      0                 % ゼロ
    | succ(n)           % 後者値
    .
v ::=                   % 値:
      true              % 真
    | false             % 偽
    | n                 % 数値
    | unit              % 定数unit
    | floatl            % 浮動小数点数値
    | stringl           % 文字列定数
    | fn(x)->m          % ラムダ抽象
    | {(l=v)*}          % レコード
    .

v(V) :- syntax(v,V). m(M) :- syntax(m,M).
x(X) :- syntax(x,X). n(X) :- syntax(n,X).
% 置換

               true![J -> M] subst true.
              false![J -> M] subst false.
     if(M1, M2, M3)![J -> M] subst if(M1_, M2_, M3_)     :- M1![J -> M] subst M1_, M2![J -> M] subst M2_,
                                                            M3![J -> M] subst M3_.
                  0![J -> M] subst 0.
           succ(M1)![J -> M] subst succ(M1_)             :- M1![J -> M] subst M1_.
           pred(M1)![J -> M] subst pred(M1_)             :- M1![J -> M] subst M1_.
         iszero(M1)![J -> M] subst iszero(M1_)           :- M1![J -> M] subst M1_.
                 F1![J -> M] subst F1                    :- float(F1).
            M1 * M2![J -> M] subst M1_ * M2_             :- M1![J -> M] subst M1_, M2![J -> M] subst M2_.
                  X![J -> M] subst X                     :- string(X).
                  J![J -> M] subst M                     :- x(J).
                  X![J -> M] subst X                     :- x(X).
      (fn(X) -> M2)![J -> M] subst (fn(X) -> M2_)        :- M2![X, (J -> M)] subst2 M2_.
            M1 $ M2![J -> M] subst (M1_ $ M2_)           :- M1![J -> M] subst M1_, M2![J -> M] subst M2_.
(let(X) = M1 in M2)![J -> M] subst (let(X) = M1_ in M2_) :- M1![J -> M] subst M1_, M2![X, (J -> M)] subst2 M2_.
               {Mf}![J -> M] subst {Mf_}                 :- maplist([L=Mi, L=Mi_]>>(Mi![J -> M] subst Mi_), Mf, Mf_).
           (M1 # L)![J -> M] subst (M1_ # L)             :- M1![J -> M] subst M1_.
                  S![J -> M] subst _                     :- writeln(error : subst(J, M, S)), fail.
             S![J, (J -> M)] subst2 S.
             S![X, (J -> M)] subst2 M_                   :- S![J -> M] subst M_.

% 評価

e([L = M | Mf], M, [L = M_ | Mf], M_)  :- \+ v(M).
e([L = M | Mf], M1, [L = M | Mf_], M_) :- v(M), e(Mf, M1, Mf_, M_).

Γ /- if(true, M2, _)     ==> M2.
Γ /- if(false, _, M3)    ==> M3.
Γ /- if(M1, M2, M3)      ==> if(M1_, M2, M3)      :- Γ /- M1 ==> M1_.
Γ /- succ(M1)            ==> succ(M1_)            :- Γ /- M1 ==> M1_.
Γ /- pred(0)             ==> 0.
Γ /- pred(succ(N1))      ==> N1                   :- n(N1).
Γ /- pred(M1)            ==> pred(M1_)            :- Γ /- M1 ==> M1_.
Γ /- iszero(0)           ==> true.
Γ /- iszero(succ(N1))    ==> false                :- n(N1).
Γ /- iszero(M1)          ==> iszero(M1_)          :- Γ /- M1 ==> M1_.
Γ /- F1 * F2             ==> F3                   :- float(F1), float(F2), F3 is F1 * F2.
Γ /- V1 * M2             ==> V1 * M2_             :- v(V1), Γ /- M2 ==> M2_.
Γ /- M1 * M2             ==> M1_ * M2             :-        Γ /- M1 ==> M1_.
Γ /- X                   ==> M                    :- x(X), member(X - m(M), Γ).
Γ /- (fn(X) -> M12) $ V2 ==> R                    :- v(V2), M12![X -> V2] subst R.
Γ /- V1 $ M2             ==> V1 $ M2_             :- v(V1), Γ /- M2 ==> M2_.
Γ /- M1 $ M2             ==> M1_ $ M2             :-        Γ /- M1 ==> M1_.
Γ /- (let(X) = V1 in M2) ==> M2_                  :- v(V1), M2![X -> V1] subst M2_.
Γ /- (let(X) = M1 in M2) ==> (let(X) = M1_ in M2) :-        Γ /- M1 ==> M1_.
Γ /- {Mf}                ==> {Mf_}                :- e(Mf, M, Mf_, M_), Γ /- M ==> M_.
Γ /- {Mf} # L            ==> M                    :- member(L = M, Mf).
Γ /- M1 # L              ==> M1_ # L              :- Γ /- M1 ==> M1_.
Γ /- M                  ==>> M_                   :- Γ /- M  ==> M1, Γ /- M1 ==>> M_.
Γ /- M                  ==>> M.

% ------------------------   MAIN  ------------------------

show(X, name,R)                :- format(atom(R),'~w', [X]).
show(X, m(M),R)                :- format(atom(R),'~w = ~w', [X, M]).
run(X/nil, Γ/[R|Rs], [X-name|Γ]/Rs) :- show(X, name,R).
run(X = M, Γ/[R|Rs], [X-m(M)|Γ]/Rs) :- m(M), Γ /- M ==>> M_, show(X, m(M),R).
run(M, Γ/[M_|Rs], Γ/Rs)             :- !, m(M), !, Γ /- M ==>> M_, !, !.
run(Ls,Rs)      :- foldl(run, Ls, []/Rs_, _/[]),!,Rs=Rs_.
run(Ls)         :- run(Ls,Rs),writeln(Rs).

% ------------------------   TEST  ------------------------

:- begin_tests(fulluntyped).
test(true):- run([true],[true]). 
test('if false then true else false'):- run([if(false, true, false)],[false]). 
test(x):- run([x/nil, x],[x,x]). 
test(variable):- run([x = true, x, if(x, false, x)],['x = true',true,false]). 
test(lambda):- run([(fn(x) -> x)],[(fn(x) -> x)]). 
test(lambda_app):- run([(fn(x) -> x) $ (fn(x) -> x $ x)],[(fn(x)->x$x)]). 
test(record):- run(
    [{[x = (fn(x)->x), y=(fn(x)->x) $ (fn(x)->x)]}],
    [{[x = (fn(x)->x), y=(fn(x)->x)]}]
  ).
test(field):- run(
  [{[x = (fn(x) -> x), y = (fn(x) -> x) $ (fn(x) -> x)]} # x],
  [(fn(x)->x)]). 
test(string):- run(["hello"],["hello"]). 
test(float):- run([2.0 * 3.0 * (4.0 * 5.0)],[120.0]). 
test(n):- run([0],[0]). 
test(n):- run([succ(pred(0))],[succ(0)]). 
test(iszero_succ):- run([iszero(pred(succ(succ(0))))],[false]). 
test(let):- run([(let(x) = true in x)],[true]). 
test(tuple):- run([{[1 = 0, 2 = 1.5]}],[{[1=0,2=1.5]}]).
:- end_tests(fulluntyped).

:- run_tests.
:- halt.

様々な機能を追加するとこのようになります。タプルはフィールド名が数字のレコードの構文糖として考えられるので、数字をそのまま用いています。これらの機能の図は 5日目 で紹介します。

まとめ

ラムダ計算は関数が引数を1つしか取らないため簡単な言語なので型理論の構築によく使われています。
ラムダ計算はMBNFにより構文定義され、操作的意味論により意味づけされます。

Crested ibis From Wikipedia, the free encyclopedia

The crested ibis (Nipponia nippon), also known as the Japanese crested ibis or Toki (トキ), variously written in kanji as 朱鷺, 鴇, 鵇, 鴾, or 桃花鳥, and written in hanzi as 朱䴉 or 朱鷺, is a large (up to 78.5 cm (30.9 in) long), white-plumaged ibis of pine forests. Its head is partially bare, showing red skin, and it has a dense crest of white plumes on the nape. This species is the only member of the genus Nipponia.

They make their nests at the tops of trees on hills usually overlooking their habitat. Crested ibises usually eat frogs, small fish, and small animals.