数理解析研究所講究録902 巻 1995 年 117-132

117

FGHC プログラムの意味を考える道具としての

$\pi$

計算

NTT 基礎研究所平田圭二 (Keiji Hirata)
1

はじめに

並行論理型言語の効率的な実行のためには, ソースプログラムの静的解析を行い, その結果をもとに最適化やプログラム変換などを施すことが必要である. 我々は, その効率化のためのプログラム変換手法の 1 つとして双対変換を提案した [3]. 次に解決すべき問題は双対変換を適用すべき個所を正しく言い出すことである. 誤った個所に双対変換を適用すると逆に効率が低下してしまう可能性がある. 双対変換を施したプログラムの抽象実行により双対変換の適用
個所, 及びどの程度の効率化が達成できるかの見積もりが得られると考えている. そこで, まず双対変換を形式的に記述するのに適した FGHC の操作的意味を定義する必要があった. 本
論文では, FGHC プログラムを Polyadic 計算 (PPC) へ翻訳する方法を述べるが, FGHCの述語や項がともに PPC のプロセスとして統–的に表現されるので, 双対変換との親和性が$\pi$高いと考えられる.
また並行論理型言語では, 変数が–度具体化されたらそれ以降その値は不変であるという論理性を壊すような操作は, 一般に許されていない. ところが, 論理性を壊す破壊的な書き換

えでも制限しつつ安全に用いることで, 実用的には効率的なアルゴリズム, 効率的な実行を達成することができる. 例えば, 通常のコーディングではリストを用いるところを配列を用いた
アルゴリズムで実現したり, 破壊書き換えの行える構造体を用意して入力本数に依存しない定
数オーダのマージャを実現することができる. しかし, 従来より提案されている並行論理型言語の意味論を, このような破壊的な書き換え操作をプリミティブとして持つような言語の意味論へと拡張するのはかなり困難に思える. そこで我々は 「計算に着目した; 並行論理型言語ではプロセス間で\tau - $-$ 構造自体を通信するのに対し, 計算では name つまりデータ構造への参照を通信することが基本となっている. 実際に, プロセス問で共有されるデータ構造に対して破壊書き換えを行う FGHC のプリミティブを PPC で記述することで, その操作的意味を定義することを試みる.
本論文の構成は次のようになっている. まず FGHC のサブセットを Polyadic 計算へ翻訳する方法について述べる; この翻訳は埋め込み (embedding) と言い換えてもよいだろう. この翻訳方法を検討することは, FGHC の持つ並行計算に関する概念をより単純な PPC の立場から考察することにつながる. 次に, この翻訳により, PPC のプログラムの上で FGHC
ログラムの動作の等価性を議論する. ここでは append プログラムと merge プログラムの例
を用いて双対なプログラムの動作が等しいことを検証する. 最後に, FGHC の新しい組込み述語の仕様を PPC で記述する. ここでは例として, 共有データをアクセスするプリミティブ
を FGHC に導入すると, 非決定的マージャと同じ動作が実現できることを示す. さらに, 共有
データをアクセスする他のプリミティブも PPC で記述し比較を行う.
$7$

$P$

$\pi$

$\pi$

$- \text{フ}$

.

$-$

118

2

$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

2.1と Polyadic

$\pi$

計算

FGHC

FGHC の操作的意味は上田式遷移システム [9] に従う. 即ち FGHC のゴール :-P. が与えにおいて, ガード部 $(H_{i}, G_{i})$ のられると, 同–のヘッドリテラルを持つ複数の節:-Gi
受動単–化 (passive unffication) が並行に行われる. ガード部の単–化に成功した節のどれかを通り抜けることができる. カ “-b’ を通り抜け
1 つだけが非決定的にコミットオペレータ$|B_{i}$$H_{i}$$(|)$

た節のボディ部 $(B)$ は, ガード部の単–化で得られた変数具体化で置換され新たなゴール群$P$. の実行は並行に行われる.
となる. 複数のゴール $:- P_{1,k}\ldots,$
は, FGHC の論理変数に対し入出力のモードを付与し, 論理変数に対する操作を単–書込み・複数読出しに制限した well-moded FGHC [11] にさらに多少の制限を加えたものである. 従って
では, ボディ部の能動単–化 (active unffication) を代入とみなすこ
プログラムの標準型では, リテラル, 項のトッとができ, 能動単–化は失敗しない 1.
プレベルには変数しか出現しないと定める (即ち flat form); 従って構造は必ず変数を介して参によるプログラム例を示す:
照される.
$(B\theta)$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

nrev$(X^{i},\mathrm{Y}^{O})$$:- X^{i}=nil$nrev$(X^{i},Y^{O})$$:- X^{i}=conS(Hm,\tau\circ)$

$|$

$|$

$Y^{O}=ni\iota$.

nrev $(Ti, R^{O}),$ $append$ ( $Ri,$ Ci,$\mathrm{Y}O$$C^{O}=conS(H^{\overline{m}}, N^{i}),$ $N^{O}=nil$

),

.

などと書く
本論文では, リストを構成する $[|]$ や $[]$ を陽に関数記号を用いて $cons/2,$(out) が付いている.
こととする. また各変数にはモード解析の結果として (in) とは, 現在は未定だがさらにモードに関する情報が増えると $in$ , out に具体化されるかも知れなである.
いモード変数である; ただし$nil/\mathrm{O}$

$|$

$o$

$m,\overline{m}$$m\neq\overline{m}$2.2Polyadic

$\pi$

計算

次に Polyadic $pi$ 計算
ような構文規則を持つ :$(\mathrm{P}\mathrm{P}\mathrm{C})[5]$について概説する. まずベースとなる$\pi$

計算があり, 次の$P::=\Sigma_{i\in I}\pi_{i}.P_{i}|P|Q|!P|(\nu x)P|A(x)|0$

ここでプロセス $\pi.P$ の$\pi$

は prefix と呼ばれ, atomic action を表わしている. この prefix に; これらがそれぞれ polyadic 入力と出力を表ね
は 2 つの基本型がある:
している . PPC に変換したプログラムは PIC システム 3 で実際に実行して確認する. しかし
PIC では複製子 (replicator, ) をサポートしていないために, PPC への翻訳に際して複製子$x(y_{1}\cdots y_{n}),\overline{x}y1\ldots y_{n}$

$2$

$!$

は導入せずに, ガードされた再帰呼出しを導入する.
$1\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{c}_{+}M_{\mathit{0}}de-Unification$

Failure より

2 本論文では [6] の構文を–部取り入れて, 以降

3Polyadic$\pi$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$と(とりあえず) 命名した.

$x([y_{1}, \cdots, y_{n}]),\overline{x}[y1, \cdots, y_{n}]$と記述する.

計算を基礎に設計されたプログラミング言語 [6]. 本研究には PIC 18 版を用いている.

119

PPC では, 構造同値性 (Structural Congruence, で表わす) という同値関係があり, 意
味的に等しい PPC の項は構文上も等しいと見なすための規則により表現される. 構造同値性$\equiv$の例を 2 つあげる:
が $P$ 中で自由出現していなければ $(\nu x)P\equiv P$ .

もし

$x$

もし

$P\equiv(\nu y)\overline{x}y$ならば, $x(z).\overline{y}z|!P\equiv(\nu y’)(X(\mathcal{Z}).\overline{y}z|\overline{x}y’)|!P$ .

そして PPC では, 簡約則 (reduction rules) によって, 通信による状態遷移 ( $arrow$ で表わす) が表現される. 遷移の例を 2 つあげる:$\overline{x}y|x(u).\overline{u}v|\overline{x}zarrow\overline{y}v|\overline{x}z$あるいは$\overline{x}y|\overline{z}v$.
.

$(\iota\ovalbox{\tt\small REJECT} Xw)(\overline{x}y|(x(u).\overline{u}v+w(u)))|\overline{x}zarrow\overline{y}v|\overline{x}z$3$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$の Polyadic$\pi$

計算への変換

本節では, FGHC を構成するいくつかの基本操作を PPC でどのように実現すればよいかを考察する.

3.1

項

FGHC の O-ary (アトム) も含む関数記号は, 文献 [5] に従って翻訳する. 例えばリストを構成する cons や nil を翻訳する場合は{ $TERM-\succ$ (CONS, NIL), $CONS-$, (TERM, TERM), $NIL\mapsto()$ } のようなソーティングを考える. これより以下のように翻訳する:$conS[t,x, y]$$nil[t]$$\mathrm{d}\mathrm{e}\mathrm{f}=$$t([c, n]).\overline{C}[x,y]$$\mathrm{d}\mathrm{e}\mathrm{f}=$$t([_{C,n}]).\overline{n}()$FGHC における項が PPC のプロセスに翻訳されているが, これらを項プロセスと呼ぶ. 項プ
プログ
ロセスは内容を 1 向読み出されたら終了する. ここで, タプル $[c, n]$ は, そのラムに出現する関数記号全部の個数分以上の長さを持ち, ソートタプルと呼ぶこととする. こ
こでは cons と nil しかないので, 長さは 2 である.
さらに, atomic なデータとして整数を持つようなプログラムに対して, Milner の Numeral
コーディング [5] を採用しても良いが, 本論文では便宜上 $INT-\succ(V)$ というソーティングを新たに加えることで対処した. 従って整数は次のような項プロセス (関数記号) に翻訳される:$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$int[t,v]$

3.2$t([c,n,i]).\overline{i}v$

論理変数と能動単–化$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$\bullet$$\mathrm{d}\mathrm{e}\mathrm{f}=$の論理変数の機能は以下のようである:

高々 1 回だけ書き込まれた値を$0$

回以上読み出す (複製)120

書き込みより先に発行された読み出しは待たされる (同期)$\bullet$

では出現する論理変数の $in$ , out のが決まっているので, チャネル
から書き込みを 1 回だけ受け付け (これは PPC の構文で保証される), チャネル から読さらに$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$\text{モ}-\mathrm{k}^{\vee}$

$w$

$+$

$r$

み出される回数分だけ項プロセスの内容を複製するように翻訳を行う:$va\dot{r}[w, r]^{\mathrm{d}\mathrm{e}\mathrm{f}}=(\nu cn)(\overline{w}[C,n]|(c([x,y]).repxonS[r, x,y]+n().rep-ni\iota[r]))$$repxons[p,x, y]^{\mathrm{d}\mathrm{e}\mathrm{f}}=p([c,n]).(\overline{c}[x,y]|rep_{-C}onS[p,x,y])$$rep-nil\beta p]^{\mathrm{d}\mathrm{f}}=^{\mathrm{e}}p([c,n]).(\overline{n}()|rep_{-}ni\iota[p])$ここでは関数記号として cons
rep-nil が行う.

Well-moded FGHC$\mathrm{b}$$\mathrm{c}$nil だけ出現すると仮定した.

$(\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-})$

次の 3 つに分類できる (以下$\mathrm{a}$と$\mathrm{H},$$\mathrm{G},$

内容の複製は rep-cons,の標準型 (flat form) における論理変数の出現パタ一で各々ヘッド部, ガード部, ボディ部を表わす):$J\backslash$は$\mathrm{B}$. ガード部での検査による節選択のため. チャネル変数として. ゴール間通信のため.

この内,は, ある節がコミットできるかどうかを知るため, ガード部で行う検査に必要な値とを読み出すための変数を指す. このパターンの変数はにのみ read-only 変数として出$in$である. このパターンでは, 最初の論理変数の出現で, 他の節で生成現する; モードは全て$var[w,\Gamma]$されたのチャネルを得て, 節内の他の出現個所ではそれを共有する.
のチャネル変数とは, 文献 [11] に従い, FGHC のとサブゴールの間で情報を運ぶチャネルの役割をする論理変数のことを指す. PPC のチャネルとは全く異なる.
での全
$in$
$in$
かつ
で
出現 (1 回以上) のモードがで out 出現する場合と
で1
出現か
で,
$in$
回 out 出現し, かっ
で 1 回 out 出現かで1回出現する場合がある. いずれの場合
も, . 同様に $var[w, \Gamma]$ の チャネルかチャネルを持ち回るだけで十分である.
のパターンは–般に,に含まれる複数のゴールが論理変数を共有して通信を行う場合を指す; 論理変数の機能であるデータの複製と同期を行う必要があるので, $var[w, r]$ を生成しなければならない. その時,に複数回出現する論理変数のは, out (1 回) と in (1 回以上) である.
に出現 (高々 1 回) があっても構わない. 例えば以下のようなの標準型において, ボディ部で first class のデータ構造 17 を生成する能動単–化を考える:$\mathrm{a}$$\mathrm{H}$$\mathrm{G}$$r$$\mathrm{b}$.

$\text{コ}-\mathrm{K}\mathrm{s}$$\mathrm{B}$$\mathrm{H},$$\mathrm{H}$$\mathrm{c}$.

$\mathrm{G}$$\mathrm{B}$$\mathrm{G}$

$w$

$r$

$\mathrm{a}$$\mathrm{G}$$\mathrm{B}$$\mathrm{B}$$\acute{\mathrm{H}},$$\text{モ}-$$\}^{\vee}\backslash$$\mathrm{G}$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$p(x^{\mathit{0}})$:-true $|q(X^{i}),$ $Xo=17$ .

17 は必ず論理変数 $X$ 経由でアクセスされる. 翻訳の結果生成された $var[w, r]$ の経由で17 が書き込まれ, $p(X)$ と $q(X)$ の $X$ には が渡され他の節において値が読み出される.
例として, $var[w, r]$ と項プロセスを用いた能動単–化の翻訳を示す:
$w$

$r$

$Y^{O}=X^{i},X^{o}=nil\Rightarrow(\nu px_{w})(var\lceil p,y_{r}]|var[x_{w},p]|nil[x_{w}])$

121の論理変数と PPC で表現された論理変数の対応を見ると,の(即ちチャネル),の(即ちチャネル) となっている. ボディ部で新しく生成される変数に対する能動単–化は, 単に対応するチャネルを共有するだけでよい. -方,他の節で生成されてチャネ j だけが渡されてくるような節がある. 例えば以下のようである:
ここで$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$X^{o}\Leftrightarrow x_{w},$

$x$

$p$

$r$

$\mathrm{Y}^{O}\Leftrightarrow p$

$w$

$y$

$u(x^{\mathit{0}}, \mathrm{Y}^{i})$$X^{i}\Leftrightarrow$:- true $|X^{o}=Y^{i}$ .

てれらの論理変数 $X,$ $Y$ に対する能動単–化は forwarder に翻訳される:$X^{o}=Y^{i}\Rightarrow x_{w}(t).y_{r}^{-}t$

ここで, 書き込まれる変数 $X$ の翻訳を $var[x_{w}, X_{r}]$ , 読み出される変数 $Y$ の翻訳を $var[y_{w}, y_{r}]$とした. この節の中では PPC で新たに論理変数を生成する必要はない. っまり,の論理変数の出現は $var[w, r]$ 個々の出現とは対応せず, そのチャネル $w,$$r$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

での出現に対応している.

3.3

述語呼出しと定義節

ボディ部に並んだ述語呼出し
は, 素直に PPC の並行なプロセ
ス呼出しに翻訳される. 述語の定義節は次のように翻訳される (ここでは in,
は out にモード付けされていると仮定):$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$p(x^{arrow})p’\cdots,$$p[X_{\mathrm{P}}arrow]|\cdots|q[x_{q}^{arrow]}$$\vec{X}$$q(x^{arrow})q$$p(\vec{X},\vec{\mathrm{Y}}^{\backslash })$$\vec{Y}$$p[\vec{x}, y]^{\mathrm{d}\mathrm{e}}=^{\mathrm{f}}(\nu_{\mathit{9}})(p1[\vec{x},g, y]|p_{2}[_{\vec{X}},g, y7|\cdots|\overline{g}())$

番目の定義節の翻訳がに対応する. 森の へのデータは $var[w, r]$ が複製して供給する.
のに対する出力は, ガードがあるので競合しない. チャネル はのコミット
オペレータに対応している (後述).
の再帰呼出しは PPC でも再帰呼出しに翻訳さ$k$$\vec{x}$$p_{k}$$y^{arrow}$$p_{k}$$g$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

れる.

3.4

ガード部

ガード部の受動単–化は, 入力された項プロセスを分解するだけであり, 外部の変数に対する具体化は行わない (副作用がない). 受動単–化は, 項プロセスと対称な (逆の) 通
信を行うように翻訳すればよい. 例えば $a(X^{i}):- X^{i}=conS(H, T)|\cdots$ という節のガード部
は以下のように翻訳する:$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$a[x,g]^{\mathrm{d}}=^{\mathrm{e}\mathrm{f}}(\nu Cn)(\overline{x}[_{C,n]}|c([h,t]).g().\cdots)$

また例えば変数同士の受動単–化を含む
翻訳すればよい:$a(X_{1}^{i}, x_{2}i):- X_{1}^{i}=X_{2}^{i}|\cdots$(1)という節は以下のように

122

(2)

$(\nu S)(matCher[x1,X2,s]|s().g().\cdots)$$a[x_{1},x_{2},g]^{\mathrm{d}\mathrm{e}\mathrm{f}}=$$matcher[a,b, s]^{\mathrm{d}\mathrm{f}}=^{\mathrm{e}}$$(\nu c_{a}n_{a}i_{ab}cn_{b}ib)(\overline{a}[c_{a’ a’ a}n\mathrm{i}]|\overline{b}[c_{b}, n_{b}, i_{b}]|$$((c_{a}([x_{a}, ya]).c_{b}([Xb, yb]).(\nu sS)xy(matCher[X_{a}, x_{b}, S_{x}]$$|matcher[ya’ yb, s_{y}]$$|s_{x}().S_{y}().\overline{s}()))$$+(n_{a}().nb().\overline{S}())$$+$$(i_{a}(v_{a}).ib(vb).(\nu b_{-)}(=[v_{a}, v_{b}, b]|b(b_{r}).\mathrm{i}\mathrm{f}[b_{r}, s,-]))))$

は PIC システ
ここでは, ソートは cons, nil, int の 3 種類あるとした. $=[v_{a}, v_{b}, b],$ムの組込みプロセスである. また, 簡単のために, ガード部には高々 1 つの受動単–化あるい$\mathrm{i}\mathrm{f}[b_{r}, t, f]$は, 変数に対して読はテスト述語が出現すると仮定している. 受動単–化のチャネルに書き込み (具体化) が行われるまで待たせることで実現する.
み出しを行った時,
また我々の翻訳では, 変数が具体化されるまで内容が読めず待たされるので, ガード部における未定義変数同士の受動単–化 (例えば, 未定義変数 $X$ に対する $X=X$ という受動単–化)$\mathrm{s}\mathrm{u}\mathrm{s}\mathrm{p}\mathrm{e}\mathrm{n}\mathrm{d}/\mathrm{r}\mathrm{e}\mathrm{s}\mathrm{u}\mathrm{m}\mathrm{e}$$w$

も suspend してしまう$4$.

FGHC の 1 つの特徴である非決定性とは,$\bullet$$\bullet$$\bullet$.

$\bullet$

ガード部の条件判定に十分な具体化が得られたら節を選べる,
どちらの節も選べるならどちらの節を選んでもよい,

どれかの節を選べるならいつかは必ずどれか選ばなくてはいけない,
選ばれなかった節は副作用を起こしてはいけない,. ということを意味するが, 我々の翻訳はこの意味において正しく動作する.
コミットオペレータの翻訳は (1), (2) のように, PPC プログ晃ムの対応する位置に $g()$ を置くだけである. ガードというのは共有資源 (上述の , のに対する排他制御の役割を果たしており, 排他制御すべきスレッドが節の形で並置されているともみなせる 5. 通常, 排他制御はガード部の条件判定とコミットオペレータで実現されているが, 決定的な述語ならコミットオ
ペレータがなくとも条件判定だけで排他制御が実現できる. 従って, 条件判定だけでは排他制が存在していると考えられる. これより我々は,御できない述語のためにコミットオペレのコミットオペレータを, critical region に入ったことを知らせるシグナルを非決定的に 1 回だけ通信する操作に翻訳する. -方, PPC は $\pi_{1}.P_{1}+\cdots+\pi_{n}.P_{n}$ という構文 (こ .
でを持ち非決定的な選択を表現することができるが, 我々の翻訳においてはこの強力な構文を用いる必然性はない.
$\vec{Y}$$-\text{タ}$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$\text{こ}$$\pi_{i}$$x(y)p_{\mathrm{a}}\overline{x}y)$4 ボディ部の $X=X$ という能動単–化は ill-moded である.
5 共有資源を持たない非決定的な述語は, 独立な 2 つのプロセスに置き換えられる.

123

3.5

append プログラムの翻訳プログラムを PPC プログラムに翻訳する. 整
本節では, ストリ一ム通信を行う数を要素とするリストを生成し $(intLiSt/2)$ , それを append する $(app/3)$ プログラムを取り上げる$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

元の$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

プログラム::- intList $(N^{io}, L),$ $app(Li, Yi, z^{\mathit{0}}),$$intLi_{St(N}i,$ $L^{o})$:- $N^{i}=<0$

intList:- $N^{i}>0$$(N^{i}, L^{\circ})$$app(X^{i}, Y^{i}, z^{\mathit{0}})$

$|$

$|$

$\cdots$$L^{o}=nil$$L^{o}=cons(N^{i},\underline{T^{i}}),$ $in7List(N^{-}1i, \underline{\tau \mathit{0}})$$:- X^{i}=nil$$|$$app(x^{i}, Y^{i}.z\circ)\text{ノ}:- X^{i}=cons(Em, xS^{o})$

,

.

$|$

$Y^{i}=Z^{o}$.

.

$z^{\mathit{0}}=cons(E^{\overline{m}},\underline{T^{i}}),$ $app(Xs^{i}, \mathrm{Y}i, \underline{\tau^{o}})$.

翻訳された PPC のプログラム:
トップレベル :$(\nu l_{w}l_{r}nwnrzwz_{r})(intList[n_{rw},\iota]|var[n_{w}, n_{r}]|int[nw’ n]$$|var[l_{w’ r}\iota]|app[\iota_{r}, y_{r}, z_{w}]|var[z_{w’ r}z]|\cdots)$$intLi_{St[]=}X,$$\iota \mathrm{d}\mathrm{e}\mathrm{f}$$(\nu g)((\nu cni)(\overline{X}[c, n, i]$$|i(k).(\nu bt_{-})$($=\langle[k,$$0,$ $b]|b(b_{r})$.if$[b_{r},$

$7$

,-]

$|t().g().ni\iota[’\lrcorner]$

)

$)$

,

$|(\nu cni).(_{\overline{X}[_{Cn,i]}}$$|i(k).(\nu bt-)(>[k, 0, b]|b(b_{r})$ .if $[b_{r},t,-]$$|t().g\{).(\nu trtwnwnr)(conS[l, X,t_{\gamma}]|var[t_{w},t_{r}]\Leftarrow\star 1$$|int[n_{w}, k-1]|var[n_{w}, n_{r}]\dagger$$|intLi_{S}l[n_{r},t]w)))$$|\overline{g}())$$app[x, y, z]^{\mathrm{d}\mathrm{f}}=^{\mathrm{e}}$$(\nu g)((\nu Cni)(\overline{X}[c, n, i]|n().g().fw[z, y])$$|(\nu cni)(_{\overline{X}[_{C,n,i]}}$$|c([e, X_{s}]).g().(\nu t_{r}t_{w})(Cons[z, e,i_{r}]|var[t_{w},t_{r}]|app[x_{S}, y, tw]))$$|\overline{g}())$(forwarder) であり, $=<[a, b, r],$ $>[a, b, r]$ は PIC システムの組込みプロセスである.
, PPC とも呼出しの引数の位置に $N-1,$ $k.-1$ とは書けないが簡単のためここでは略記する. $var[w, r]$ は基本的に第 3.2 節の翻訳方法に従いコーディングする.
ここで $var[w, r]$ が生成されるのは元のプログラムにおいて一 (下線) を付した変
ここで$fw[z, y]\mathrm{d}\mathrm{e}\mathrm{f}=Z(t).\overline{y}t$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

数である.

.

また第 3.1 節で述べたように, 整数は便宜的に $int/1$ という関数記号を用いて表現されている. 従ってここで用いられる $var[w, r]$ は, cons, nil, int の 3 つの関数記号が読み書きできるように 3 要素のソートタプルを持つ必要がある. さらに, 整数がボディ述語の引数として $in$

124

モードで出現する時には, 他の関数記号と同様の扱いをする必要があり, PPC への翻訳において $var[w, r]$ を生成する (上のプログラムにおける $var[n_{w},$).
$nr]\dagger$

双対なプログラムの PPC への翻訳

4

FGHC プログラムにおいて, そのアルゴリズムには変更を加えず, データを運ぶメッセー
ジとプロセスの役割を入れ換えるだけの変換を双対変換 [3] と呼ぶ. 直観的には双対変換を施してもプログラムの意味は不変であると考えられるが, まだ形式的には証明されていない. 本
プログラムを PPC に翻訳し, 双対変換されたプログラム間の等価性
章では双対なを考察する.
$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

4.1

append の双対変換

第 3.5 節と同じ例題に対して, $app/3$ の第 1 引数に関して双対なプログラムを示す::- intList $(N^{ii}, L),$
intList$(N^{i}, L^{i})$$intLi_{S}t(N^{i},L^{i})$$p_{-nil}(X^{i})$$L^{o}=app(\mathrm{Y}^{io}, Z),$ $\cdots$:- $N^{i}=<0$:- $N^{i}>0$$p-ni\iota(L^{i})$$|$$p-conS(Li, N^{i}, T^{O}),$ $intL\mathrm{i}St(N-1i,T^{i})$$|$$:- X^{i}=app(\mathrm{Y}^{\circ,z)}i$.

.

$\mathrm{Y}^{i}=Z^{o}$
$|$

.

.

$p_{-ConS}(Xi, E^{m},xs^{O})$ $:- X^{i}=app(\mathrm{Y}^{\circ,z)}i | Z^{o}=cons(E\overline{m},\tau i),Xs^{o}=app(Y^{i},\tau^{O})$

関数記号 cons, nil を述語に変換した際, 便宜上, 述語名, プロセス名を
以下は PPC への翻訳である.

$p$.

-cons, -nil とした.
$p$

125

トップレベル :$(\nu l_{w}l_{rwr}nnzzwr)(intLiSt[n\iota r’ r]|var[nnw’ r]|int[nw’ n]$$|var[\iota_{w}, l_{r}]|app[\iota_{w}, y_{r}, z_{w}]|var[z_{w’ r}z]|\cdots)$$intList[X, l]=\mathrm{d}\mathrm{e}\mathrm{f}$$(\nu g)((\nu Cni)(\overline{X}[a, C, n,i]$$|i(k).(\nu bt-)(=<[k, \mathrm{o}, b]|b(b_{r}).\mathrm{i}\mathrm{f}[b_{r}, t,-] |t().g().p-ni\iota[\iota]))$$|(\nu cni)(\overline{X}[a,C, n, i]$$|i(k).(\nu bt_{-})$($\rangle[k, \mathrm{o}, b]’|b(b_{r}).\mathrm{i}\mathrm{f}[b_{r},t,-]$$|t().g().(\nu t_{r}t_{w}n_{wr}n)(pxonS[l, X, t]w|var[t_{w},t_{r}]\Leftarrow\star 2$$|int[n_{w}, k-1]|var[n_{w}, n_{r}]$$|intList[nr’ t]r)))$$|\overline{g}())$$app[x, y, z]^{\mathrm{d}\mathrm{f}}=^{\mathrm{e}}$$p_{-nil}[p]^{\mathrm{d}\mathrm{f}}=^{\mathrm{e}}$$x([a, C, n, i]).\overline{a}[y, z]$$(\nu g)((\nu aCni)(\overline{p}[a, C, n, i]|a([y, z]).g().fw[z, y])$$|\overline{g}())$$P-ConS[p, e,x_{S}]^{\mathrm{d}\mathrm{e}}=^{\mathrm{f}}-(\nu g)((\nu acni)(\overline{p}[a, c,n, i]$$|a([y, z]).g().(\nu t_{r}t_{w})(Con.s[_{Z,e}, t_{r}]|var[t_{w}, t_{r}]|app[X_{S}, y, tw]))$$|\overline{g}())$

に関しては, 第 3.5 節のプログラムのをのように, 変数に対するモードを逆転させるだけでよい. トップレベルに関しても, 変数のモードを逆転させれば良い. さらに
この場合は -cons, pmil というプロセス名への書き換えも必要である. ここでソートタプル
が $[a,.c, n, i]$ となっている点に注意;
は双対変換後のプログラムにおける関数記$app/2$号のに対応している.
$intLi_{St[}n,$ $l]$$\star 1$$\star 2$

$p$

$a$

$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

PPC プログラムでは cons, nil という項プロセスがを供給し, データを受け取った $app$ が計算を行っていた. 双対変換されたプログラムでは逆に $app$ が項プロセス
としてデータを供給し, -cons, -nil の中で計算が行われる. 元の $intList/2$ での $L^{o}=$$cons(N^{i}, T^{i})$と双対変換後の $p_{-CO}nS(Li, N^{i}, \tau\circ)$ という述語呼出しが, PPC ではテキスト上
元の$p$$\overline{\tau}’-$

$P$

$P$

は全く同じプロセス呼出しに翻訳されている点に注意; ただしに関するデータ送受のモードは逆である. また, データ供給の向きを逆転させるために書き換えられたのは各述語のガー
ド部に対応する部分だけであり, ボディ部は変数のモード逆転を除いて変更はない.
PPC において, この元プログラムと双対なプログラムでは同じ振舞いが観測できる. 例として, 次の 2 つの翻訳の reduction を行う:
$l,$元の append プログラムの翻訳:

双対な append プログラムの翻訳:$t$$(\nu x_{w}x_{r}yzd\cdots)(aPP[X_{r}, y, z]|var[x_{w’ r}x]|conS[x_{w}, n, d\rfloor|\cdots)$$(\nu x_{w}x_{r}yzd\cdots)(aPP[X_{w}, y, z]|var[x_{w’ r}x]|pxonS[x_{r}, n, d]|\cdots)$126

これらはともに $arrow^{\star}(\nu t_{r}t_{w})(conS[z,n,t_{r}]|var[t_{w},t_{r}]|app[d,y,tw]|\cdots)$ となり, チャネル$z$に対して同じプロセス構造を生成することが分かる.

4.2

merge の双対変換. 非決定性を持つ述語の 1 つとして $merge/3$ を PPC プログラムに変換する. まず元となるで記述されたメッセージストリームをマージするプログラムは以下のようである:$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

merge$(x^{i},\mathrm{Y}i, Z^{O})$$:- X^{i}=cons(E^{m}, xS^{o})$merge$(Xi,Y^{i}, z^{\mathit{0}})$$:- Y^{i}=conS(E^{m},YS^{O})$merge$(x^{i},\mathrm{Y}i, Z^{O})$$:- X^{i}=nil$merge$(x^{i},\mathrm{Y}i, Z^{o})$:-,Y $=nil$

$|$

$|$

$|$

$|$

$Z^{o}=cons(E\overline{m}, zSi),$ $merge(x_{S}i, Yi, zs^{O})$.

$Z^{O}=conS(E\overline{m}, Zsi),$ $merge(X^{i},Ys^{io}, Zs)$.

$Z^{o}=Y^{i}$.

$Z^{o}=X^{i}$.

これは, 以下のような PPC プログラムに翻訳される:$merge[x,y,\mathcal{Z}]=^{\mathrm{e}}\mathrm{d}\mathrm{f}$$(\nu g)((\nu cn)(\overline{x}[C,n]|c([e,x_{s}]).g().(\nu rw)(conS[z,e,r]$$|var[w,r]|merge[xS’ y,w]))$$\Leftarrow\star 3$$|(\nu cn)(\overline{y}[_{C,n]}|c([e,y_{s}]).g().(\nu rw)(conS[\mathcal{Z},e,r]$$|var[w,r]|merge[x, ys’ w]))$$|(\nu cn)(\overline{x}[_{C,n]}|n().g().fw[z,y])$$|(\nu cn)(\overline{y}[_{C,n]}|n().g().fw[z,x])$$|\overline{g}())$の述語は双対変換できない. そこ
現在の双対変換の枠組みでは, 非決定性を持つ
で前出の $app/3$ プログラム例にならって, PPC レベルで双対変換 (のような書き換え) を施
す. $merge/3$ の第 1 引数に関して双対変換を行い, そのデータ供給の方向を逆転させる:$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

127

トップレベル:$(\nu x_{w}x_{r}y_{w}y_{r^{\mathcal{Z}}}twtr)(merge[\chi_{w},$$yr’ z||var[y_{w},y_{r}||intLi_{S}t[yw’ n]$$|var[x_{w’ r}x]|p-cons[xer" t_{w}]|var[t_{w}, t_{r}]|p_{-}nil[t_{r}]|$$merge[x, y, \mathcal{Z}]^{\mathrm{d}\mathrm{f}}=^{\mathrm{e}}$$(\nu g)(X([m, c, n]).\overline{m}[y, z].g()$.. )$\Leftarrow\star 4$$|(\nu mcn)(\overline{y}[m, c, n]|c([e, y_{s}]).g().(\nu rw)(conS[z, e, r]$$|var[w, r]|merge[x, y_{s}, w]))$$|(\nu mcn)(\overline{y}[m, c, n]|n().g().fw[z, X])$$\Leftarrow\star 5$$|\overline{g}())$$p_{-}conS[x, e,x]S=\mathrm{d}\mathrm{e}\mathrm{f}$$(\nu g)((\nu mcn)(\overline{X}[m, c, n]|m([y, z]).g().(\nu rw)(conS[z, e, r]$$|var[w, r]|merge[x_{S}, y, w]))\Leftarrow\star 6$$|\overline{g}())$$p_{-}nil\mathrm{r}p]=^{\mathrm{e}}\mathrm{d}\mathrm{f}$$(\nu g)((\nu mcn)(\overline{p}[m, c, n]|m([y, z]).g().fw[_{Z}, y])$$\Leftarrow\star 7$$|\overline{g}())$

双対変換後のトップレベルでも同様に, 第 1 引数を受ける論理変数に対応する $var[w, r]$ の ,.
の方向が逆転している. 双対変換前には入力の分解及び非決定的なコミットが $merge/3$ の
ガ一 t‘s 部で行われていたが, PPC の $merge/3$ の第 1 引数に関する双対変換を行うと, 元のボ
ディ部
の部分は,
のように項プロセスのボディ部と入れ換わる. -方, 元のボディ部と pxilは -consのボディ部に分かれて移動している.
この双対な $merge/3\text{は^{}6},$
への多重書き込みが生じて動作しない. 条件判定だけでは排他制御できない非決定的な述語に双対変換を施すと, 排他制御すべき操作が $merge/3$ のカ “ドにかからない所に出現してしまうからである (この場合 -cons, -nil の $g()$ 以降のボディ
ト $m$ の情報を出力し, 決定的に -cons か pmil のボディ部で共有資源部). 例えば,の $g()$ が先にシグナルを受けとる可能性があへの書き込みが生じているにもかかわらず,る. 従って, 非決定性の満たすべき性質である, $merge/3$ の 4 つの定義節のどれも選べない時はどれか選べるようになるまで (副作用を起こさずに) 待たねばならず, かつ選ばれなかった
節は共有資源に対して副作用を起こしてはならない, ということが満たされていない. また$X([m, c, n]).\overline{m}[y, z]$ となっていても, 同様に動作しない.
の行がこのような場合,で出力された情報をバックトラックによりキャンセルできれば良いのだが, 我々の翻訳の枠組みではできない. また, 異なる述語の定義値間で排他制御を行うような仕組みがあっても良いのだが,は言語としてそのような機能を備えていない.
$w$$\gamma$$\star 4$$(\star 3)$$(\star 6)$$p$$(\star 7.)$

$z$

$P$

$P$

$\star 4\text{で^{}\backslash }\dot{\text{ノ}}-$$P$$\star 5$$z$$\star 4$$g\mathrm{O}$$\star 4$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

6 これは間違った変換なので本当は双対ではない.

128

5

新しい組込み述語の仕様記述

5.1

共有データ操作のための組込み述語に共有データ操作のための新しいプリミティブ$swap_{-}shared\Lambda ata$ ()( $swap_{B}d$ と略す) を導入することを考える 7. 本述, Old, New,は共有データへの参照 (共有 T- $-$ の存在する場所) を表す. $SD_{0}$ に $V$
語の引数 $SD_{0},$という値が記憶されている時, swap-sd を実行すると, $SD_{0}$ 上の $V$ は New に置き換えられ,$V$ は
Old から読み出される. この–連の swap 操作は排他的に実行され, swap が終了するとに新しい共有データへの参照が具体化される. KL1 の $Set_{-}vect_{or_{-elnt}}eme/5[10]$ と異なが共有されていてもコピーを生成せず破壊代入を行い副作用を残すことでるのは, $SD_{0},$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$SD_{1}$$sD_{\dot{0}}$$p$$SD_{1}$$SD_{1}$$SD_{1}$

ある.
この $swap_{B}d$$swap_{B}d\beta p,$と, 共有データをアロケートする述語 alloc-sd の仕様を PPC で記述する.

$u,q]=^{\mathrm{e}}\mathrm{d}\mathrm{f}$$\mathit{0},$$(\nu cnis)(\overline{p}[C, n,i, S]$$|s(m).(\nu r)(\overline{m}[r, u].(r(v).fw[v, \mathit{0}]|q([c, n,i, S]).\overline{S}m)))\Leftarrow\star 8$$alloc_{-}sd\mathrm{r}p]=^{\mathrm{f}}\mathrm{d}\mathrm{e}p([c, n, i, S]).(\nu m_{-})(\overline{s}m|swap[m,-])$$swap[m, v]^{\mathrm{d}\mathrm{e}\mathrm{f}}=$$m([r, u]).(\overline{r}v|swap[m, u])$という要素が増えたが, チャネル 上で送受されるデータは常に allocBd で最初に定義された $m$ (定数) である点に注意. このswapBd のモードは が $in$ で が out である. 逆の が出力で が入力であるようなとすればよい. また, 共有メモリを複数セルに拡の所を
swap-sd は,ソートタプル $[c, n,i, S]$ に, 新しいソートに対応して

$s$

$s$

.

$u$

$\mathit{0}$$u$$\mathit{0}$$fw[v, \mathit{0}]\Rightarrow fw[\mathit{0}, v]$$\star 8$

張するのも容易である.

5.2

merge プログラムの実現

swap-sd 述語を用いると,述できる 8:merge$(x^{i},\mathrm{Y}^{io}, z)$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$:-true$|$の尋問の非決定性を利用せずに非決定的マージャが記$al\iota_{\mathit{0}}c-Sd(sD_{0}^{o}),$$swap_{B}d$($SD_{0}i,$

dumi, $Zo,$$mg_{-in}(x^{i}, sD^{i}1),$ $mg-in(\mathrm{Y}i, sD^{i})1$$mg_{-in}(X^{ii}, -)$$mg_{-in}(X^{i}, S_{0}^{i})$$:- X^{i}=nil$:- $X^{i}=conS$ ( $Hm,$ To)

$|$

$|$

),

.

true.
$swap_{-S}d(si0’ A^{i}, Ro, S1)\circ,$ $Ao–cons(H^{\overline{m}}, R^{i})$$mg_{-in}(\tau i, S^{i})1$.

この $swap_{B}d$ を用いた PPC マージャのプログラムを示す:.

$SD_{1}\circ$

7 本組込み述語のオリジナルアイデアは久門耕–氏 (ICOT) による.

8swap-sd を用いたマージャは正しく双対変換を行うことができる.

,

129

$merge[x, y, z]^{\mathrm{d}\mathrm{f}}=^{\mathrm{e}}$$(\nu g)(g().(\nu S0wS0rs1wS1r-)(al\iota oc_{-}sd[_{S}\mathit{0}_{w}]|var[s0_{w}, s_{0}]r$$|swap_{Bd}$ [ $s$ or’ $dum,$ $z,$$s_{1}$$w|var[S1w’
S_{1}]r$]$|mg_{-\mathrm{i}}n[x, s_{1r}]|mg_{-in}[y, s1r])$$|\overline{g}())$$mg_{-in}[X,p]\mathrm{d}\mathrm{e}\mathrm{f}=$$(\nu g)((\nu CniS)(\overline{X}[C, n, i,S]|n().g()’)$$|(\nu cniS)(\overline{x}[c, n, i, S]$$|c([h,t]).g().(\nu q_{w}qraa_{r}r_{w}r_{r}w)(swaparrow \mathrm{s}d\lceil p,$ $ar_{w}r$ $q_{w}$”] $|var[q_{w}, q_{r}]$$|fw[a_{r}, a_{w}]$$|conS[ah,r_{r}w’]|var[r_{w}, r_{r}]\Leftarrow\star 9$$|mg-in[t, qr1))$$|\overline{g}())$

ここで, 単–書込み単–読出しであることが分かっているような変数 (この場合 mg-in の $A$ )の場合は,には本来ならが来る筈であるが, 値の複製をする必要がなく同期だ
けをとれば良い\emptyset . で $fw[a_{r}, a_{w}](=a_{r}(t).a_{w}-t)$ で十分機能する.
本節で定義した $merge/3$ が, swap-sd を用いない従来のマージャと同じ動作をすることは, 第 4.1 節同様に, PPC 上で reduction
を行うことで確認できる 9.
$var[a_{w}, a_{\gamma}]$$\star 9$$(arrow^{\star})$

5.3$\mathrm{P}\mathrm{P}\mathrm{C}$による Port の仕様記述

並行論理型言語における共有データに対するアクセスプリミティブは, $swap_{B}d$ の他にも,
port[1], mutual referenceなどがあり, これらを PPC で記述することで統–的に比較$\mathrm{c}\mathrm{e}\mathrm{l}\mathrm{l}[7]$することが可能となる.
ここでは port を取り上げる.

port を生成するプリミティブは $open_{-}p_{ort}/2$ であり, portに 1 つのデータを送信するプリミティブは $send/2$ である. 以下のように動作する 10::- $open_{-}port(P, S),$ $send(P, 2),$ $Send(P, 3),$ $Send(P, 5),$
この時 $S$ は非決定的に $[2, 3, 5, \cdots],$ $[3,2,5, \cdots],$の $all_{oCB}d,$
れら各プリミティブはだろう:$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

9 ストリ一ムが nil$\cdots$.

のいずれかに具体化される. こで以下のように定義することができる$[3,5,2, \mathrm{n}\cdot\cdot]\cdots$$swap_{-}\mathrm{s}d$で閉じられた場合も含めると従来の $merge/3$ とは厳密には等しくない. 等しくするために, マージャの入力本数を記録するカウンタを swap,$d$で実現する方法と, 全ての mg-in プロセスが終了したことを short circuit で検出する方法がある.
$1_{\mathrm{p}_{\mathrm{o}\mathrm{r}}\mathrm{t}}$の仕様では, ある port への参照がなくなるとシステムがそれを検出し, 出力ストリ一ムを自動的に閉じることになっているが, ここでは簡単のため考慮しない.

130

上述の

$open_{-}p_{ort}(P^{o}, ZO)$$\equiv$

send $(P^{i}, E^{m})$$\equiv$

における$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

allocBd$(s^{\mathit{0}}),$$SwapBd(S^{i}, dum, z, P^{\circ})i\circ$$swap_{B}d(Pi, Ai, B^{Oo}, -),$ $AO=cons(Em, B^{i})$$open_{-}port/2$と $send/2$の定義が正しいかどうかを検証するために, PPC に翻訳し reduction を行う:
$open_{-p}ort[p, z]^{\mathrm{d}\mathrm{f}}=^{\mathrm{e}}$$send[p, e]=^{\mathrm{f}}\mathrm{d}\mathrm{e}$$(\nu m)(p([c, n,i, S]).\overline{S}m|swap[m, z])$$(\nu a_{wrw}abb_{r})(swap_{B}d[p, abr’ w’-]$$|fw[a_{r}, a_{w}]|cons[aw’ e, br]|var[b_{w}, b_{r}])$

これらの定義より$(\nu p_{w}p_{r})(open-p_{or}t\mathrm{k}^{y}w’ Z]|var[p_{w},p_{r}]|send[pr’ e_{1}]|send[pr’ e2])$$arrow^{\star}(\nu mp_{r}a_{w}a_{r}bwb_{r})(fw[Z, a_{r}]|fw[a_{r}, a_{w}]|cons[a_{w}, e_{1}, br]|var[b_{w}, b_{r}]$$|swap[m, b_{w}]|rep_{-^{S}}d[p_{r}, m]|send[pr’ 2e])$$arrow^{\star}(\nu mp_{r}a_{wr}abwbr^{C}w^{C}r.dwdr)$$(fw[z, a_{r}]|fw[a_{r}, a_{w}]|cons[aw’ e1, b_{r}]|var[b_{w}, b_{r}]$$|fw[b_{w}, C_{\gamma}]|fw[c_{r’ w}c]|cons[c_{w}, e_{2,r}d]|var[d_{w}, d_{r}]$$|swap[m, d_{w}]|rep_{-}sd[pr’ m])$$(fw[z, a_{r}]|fw[a_{r}, a_{w}]|cons[aw’ e1, b_{r}]|$$arrow^{\star}(\nu a_{w}a_{r}b_{r}dwd_{r})$$|rep_{\neg}cons[ber’ 2, d_{r}]|var[d_{w}, d_{r}])$

ここで, $var$ [$p_{w},p_{r}|$ の中から呼び出される $rep-\mathrm{S}d|p_{r},$ $m$ ] プロセスが値 $m$ を複製すると仮定した.

mutual reference cell に関しても, それを生成するプリミティブ$(all_{oC}ate_{-}mutua\iota-\Gamma eference/2)$とアクセスする$\text{フ^{}\mathrm{o}_{\mathrm{I}}}J$

ミティブ $(st^{e}ream-append/3)$ を PPC で記述することができる この時, $open-port/2$ の仕様と $alloCateJ\prime \mathrm{z}utual-reference/2$ の仕様は全く同じであり, $stream-append/2$ の仕様と $send/2$ の仕様は非常によく似ていることが分
かる.

6

おわりに

本論文では, まず FGHC を 計算に翻訳 (embedding) する方法を非形式的に述べた. 次にその応用として, 双対変換はプログラムの意味を変えない変換であることの検証, 共有変数
を破壊的に書き換える組込み述語の仕様定義を行った. これらの実例より, 本翻訳の応用範囲の広さを示すことができた.
関連研究としては, まず [4] がある. Prolog の実行における, バックトラックを含む述語の実行制御 (SLDNF resolution) とバックトラック付き単–化を, 計算にコーディングする方法を示した. この研究に用いられている
計算では, チャネル同士の等価性をテストするプリ
$\pi$

$\pi$

$\pi$

131

ミティブや, 型検査のプリミティブの存在を仮定している. また, 論理変数が未定義であることはタグにより判定している. WAM による実行を比較的素直に表現していると言えよう.
本研究は, プログラミング言語 Oz [2] とその意味論 [8] の研究にも重要な関連がある. Oz
は, 並行制約, オブジェクト指向, 高階という特徴をもった言語である. その意味論の考察を通して計算は, 大まかに言うと, 計算
計算という新しい並行計算モデルが得られている.
にプリミティブとして論理変数を加えたようなものである. Smolka らのアプロ $-\text{チ}[8]$ は, 表$.\pi$$\gamma$$\gamma$

現力の高い言語の意味を記述するためにはモデルを拡張する必要がありそのために新しいプ
リミティブを導入するというものである. -方, 我々のアプローチはその逆で, PPC に埋め込を考えて, その範囲で翻訳を行うというもの
むことのできる FGHC のサブセット$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

である.

以下, 今後め課題を述べる.
から PPC への我々の翻訳方法をもっとが付与できる FGHC
矛盾なく
形式的に記述する必要がある. そして, 上田式遷移システムに関して我々の翻訳が正しいことの操作的な意味とを示すことができれば, 翻訳の結果得られた PPC プログラムをが生じると無意味な見なすことができる. ただし, よ田式遷移システムで unffication failure
計算状態に陥り, reduction failure が生じると suspension (deadlock) に陥る. –方, 我々の翻訳の結果生成された PPC プログラムでは, これら failure が区別できず全て deadlock してし
まう. しかし,に制限することで unification failure を回避することができると考え$\text{モ}-$$(\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-})$$\mathrm{b}^{\vee}$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$ている.

また, 翻訳された PPC プログラムの型は, 元のいる. PPC 上の型システムから得られる情報が, 元程度寄与するのか, についても調べたいと思う.

$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$$\mathrm{F}\mathrm{G}\mathrm{H}\mathrm{C}^{+-}$

プログラムの型と関連を持ってプログラムの実行効率化にどの謝辞:
FGHC のモード解析について, 早稲田大学上田和紀助教授より大変貴重な助言を数多く頂きました. また本研究を行うにあたり, NTT 基礎研究所尾内 K. 理紀夫氏は著者を常に暖かく励まして下さいました.

参考文献[1] S. Haridi, S. Janson, J. Montelius

Programs (DRAFT). unpu blished$\overline{\subset}\mathrm{d}$$d_{(}$[2] M. Henz, G. Smolka and J\"org W\"urtz,

M. Nilsson, Ports for Objects in Concurrent Logic$\text{・}\iota \mathrm{m}\mathrm{e}\mathrm{n}t$$\sim_{1Z}-\mathrm{A}$(Dec. 1991).

Programming Language for Multi-Agent Systems,

In Proc. of IJCAI’93, pp.404-409 1 (..} $‘).3)$ .
$($[3] K. Kumon and K. Hirata, A New

Concurrent Logic Languages In$!^{\backslash }\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{s}\mathrm{f}_{0}\mathrm{r}\mathrm{m}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}$$P_{l:\prime}$[4] B. Li, A -calculus Specification ofof ICLP 1994, pp.684-698 (1994).

$\pi$[5] R. Milner, The Polyadic(1991).

$\pi$

Based on Process-Message Duality for$i_{l_{\backslash }^{\prime)}}.1li.0.\mathrm{g}\iota$

In Proc. of ESOP 1994 (1994).

-Calcul $ns:$ a Tutorial. ECS-LFCS-91-180, University of Edinburgh

132[6] B. Pierce, Programming in the $Pi$ -Calculus.

$\mathrm{f}\mathrm{t}\mathrm{p}$.dcs.ed.ac.uk より anonymous FTP 可能 (1993).

[7] E. Shapiro and S. Safra, Multiway Merge with Constant Delay in

Concur.rent Prolog. New

Generation Computing, Vol. 4, pp.211-216 (1986).
[8] G. Smolka, A Foundation for Higher-or der$Co\mathrm{n}$current$c_{o\mathrm{n}s}t$raint Program ming. RR-94-16,$-$

DFKI (1994).
[9] K. Ueda, Designing a Concurrent Programming Language. In Proc. of$I\mathrm{n}foJ\mathrm{a}pa\mathrm{n}’ \mathit{9}\mathit{0}$, pp.87-94(1990).
[10] K. Ueda and T. Chikayama, Design of the Kernel Language for the Parallel Inference Machine.

The Computer Journal, Vo1.33, No 6, pp.494-500 (1990).
[11] 上田, 並列論理型言語の言語処理系の効率化に関する調査研究報告書, ICOT (March 1994).