Guarded Horn Clauses

提供: miniwiki
2018/8/19/ (日) 20:02時点におけるAdmin (トーク | 投稿記録)による版 (1版 をインポートしました)
(差分) ← 古い版 | 最新版 (差分) | 新しい版 → (差分)
移動先:案内、検索
Guarded Horn Clauses
パラダイム 並行論理プログラミング
登場時期 1985年
設計者 上田 和紀
型付け 動的型付け
主な処理系 KLIC、Overlay GHC、Logix 他
影響を受けた言語 Concurrent Prolog、PARLOG83
影響を与えた言語 KL1、PARLOG86、Strand、Oz、CHR、Janus、AKL、PCN
テンプレートを表示


Guarded Horn Clauses (GHC)は、1984年末に設計され1985年に発表された並行論理プログラミング言語である[1]。第五世代コンピュータプロジェクトで並列マシンの核言語の検討をしていた上田和紀により設計された。核言語の候補だったConcurrent Prologを分析する過程で問題点を見付け、それを解決するさらに単純化した言語として設計した。

GHCのバリエーションであるFlat GHCを基に、近山 隆によりKL1 (Kernel Language One) が設計され、第五世代コンピュータプロジェクトでハードウェアと応用ソフトウェアとの間を繋ぐ核言語として、並列マシンのオペレーティングシステムやKL1を含む様々な言語処理系、各種応用プログラムの作成に利用された[2]。

概要

Guarded Horn Clauses (GHC) は並行プログラミングのためのプログラミング言語で、論理変数を介して通信を行う複数の軽量プロセスのネットワークとしてプログラムを記述する。「並行アルゴリズムを気持ちよく記述できる汎用プログラミング言語を論理プログラミングの枠組みを利用して開発すること」を目標として設計された[3]。多くの並行プログラミング言語が逐次処理言語に並行実行の機能を追加したものなのに対して、GHCは並行実行が基本で、並行処理を素直に記述できる。言語の特徴を以下に示す。

  • 逐次実行ではなく並行実行が基本。並行処理を素直に記述できる。
  • 動的にプロセスを生成できる。
  • 動的に通信チャネルを生成でき、他のプロセスに転送できる。
  • 通信ネットワークの動的な再構成が可能である。
  • 様々な形態のプロセス間通信を表現できる。
  • 理論的な背景を持ち、明確な意味論を持つ。

GHCではホーン節にガードを導入した以下のような規則(Clause)の集まりでプログラムを記述する。"|"はコミット演算子と呼ばれる。G はガード部、B はボディ部と呼ばれる。Head、G、Bはそれぞれ原子論理式である。ガード部の条件がない場合、ガード部とコミット演算子は省略できる。 

Head :- G1, ..., Gn| B1, ..., Bm.  (n,m≧0)

このガード付きホーン節は、エドガー・ダイクストラのガード付きコマンドと同様のものである。HeadとG1, ..., Gnはプロセス書き換えのための条件、B1, ..., Bmは書き換え後のプロセスを表す。生成されたプロセスはすべて並行に実行される。また、各プロセスごとの書き換え条件のチェックも複数の節で並行に実行してよく、コミット時にただ1つの節が選択される（コミッティッド・チョイス）。prologと異なりバックトラックの機能はない。

ガード付きホーン節とプロセス動作の指示との関係は以下のようになる。 

*停止　　　　　　　　　　　A :- Guard | True.
*プロセス状態の変更　　　　A :- Guard | B.
*並行したｍプロセスの生成　A :- Guard | B1, ..., Bm.


プロセス間の通信にはプロセス間で共有する論理変数を使用する。書き換え規則の適用に十分な情報がなければ書き換えを中断し、判断に必要な情報が得られるまで待つことで、プロセス間の同期が行われる。多くの場合、プロセス間の通信には論理変数を含んだリストで表現されたストリームを用いる。ストリームは [<メッセージ>|<変数>] のようなリストで実現する。論理変数を共有するプロセスの数に制限はないため、ストリーム通信は1対1だけではなく1対Nのブロードキャストなど、様々な形態が可能である。

GHCでは、プロセス間の同期のための中断のメカニズムとして入力ガード (Input Guard)を用いる。ヘッドおよびガード部でのユニフィケーションの際、呼び出し側の変数は入力モードでしかアクセスできず、呼び出し側の変数を具体化(Instantiation)するような試みは中断させられる。出力となる変数の具体化はボディ部のユニフィケーションで行う。

プログラム例

マージ

2本のストリームをマージして1本のストリームにするマージプロセスのプログラム例を以下に示す。Prologと同様、A や Xs など英大文字や"_"で始まる項は変数を表す。mergeの最初の2つの引数が入力、最後が出力のストリームである。 

merge([A|Xs],Ys,Zs0) :- true | Zs0=[A|Zs], merge(Xs,Ys,Zs).
merge(Xs,[A|Ys],Zs0) :- true | Zs0=[A|Zs], merge(Xs,Ys,Zs).
merge([],Ys,Zs) :- true | Zs=Ys.
merge(Xs,[],Zs) :- true | Zs=Xs.

例えば、上記プログラムの最初の節では、最初の引数が[A|Xs]のようなリストの形になっていない場合は中断し、他のプロセスにより[A|Xs]の形に具体化された(具体的に値が決まった)場合に実行を再開する。この時点でXs自体は具体化されていなくても構わないため、リストの先頭からインクリメンタルに具体化されるストリームを素直に処理できる。

素数生成

エラストテネスのふるいを使い素数生成を行うプログラム例を示す。 

gen_primes(Max,Primes) :- gen(2,Max,Ns), sift(Ns,Primes).

gen_primes/2を実行すると、gen/3とsift/2の2つのプロセスが生成される。gen/3はMaxまでの自然数のストリームを生成し、sift/2はそれをふるいにかけ素数のストリームをPrimesに返す。gen/3とsift/2とはそれぞれ並行して動き、gen/3で生成された自然数のストリームは変数Nsを介して順次sift/2に渡される。プロセス間の同期は、ストリームの各要素が具体化されるまで待つ、という形で自然に表現される。

gen/3、sift/2の各プログラムはそれぞれ以下のようになる。gen/3は、自然数のストリームを順次生成しMaxを超えたら終了する。sift/2は、2,3,5,7,..などの各素数の倍数をストリームから取り除くfilterプロセス（ふるい）を順に生成しながら、求まった素数を順次ストリームの要素として返す。各filterプロセスは変数を介して直列に繋がれていくため、自然数のストリームから素数のみのストリームを求めることができる。 

gen(N0,Max,Ns0) :- N0=<Max | Ns0=[N0|Ns1], N1:=N0+1, gen(N1,Max,Ns1).
gen(N0,Max,Ns0) :- N0 >Max | Ns0=[].

sift([Prime|Xs1],Zs0) :- Zs0=[Prime|Zs1], filter(Prime,Xs1,Ys), sift(Ys,Zs1).
sift([],         Zs0) :- Zs0=[].

filter(Prime,[X|Xs1],Ys0) :- X mod Prime=\=0 | Ys0=[X|Ys1], filter(Prime,Xs1,Ys1).
filter(Prime,[X|Xs1],Ys0) :- X mod Prime=:=0 |              filter(Prime,Xs1,Ys0).
filter(_,    [],     Ys0) :-                   Ys0=[].

クイックソート

与えられたリストのクイックソートを行うプログラム例を示す。part/4はリストをピボットより大きい数のリストと小さい数のリストの2つに分割する。2分割された各々のデータはそれぞれqsort/3でソートされる。 

qsort([Pivot|Xs], Ys0, Ys2) :- part(Xs,Pivot, Small, Large),
                               qsort(Small, Ys0, [Pivot|Ys1]),
                               qsort(Large, Ys1, Ys2).
qsort([],         Ys0, Ys1) :- Ys0 = Ys1.

part([X|Xs],Pivot,Small,Large) :- Pivot< X | Large=[X|L1], part(Xs,Pivot,Small,L1).
part([X|Xs],Pivot,Small,Large) :- Pivot>=X | Small=[X|S1], part(Xs,Pivot,S1,Large).
part([],    _,    Small,Large) :-            Small=[], Large=[].

qsort/3を呼び出すことで順次part/4とqsort/3とのプロセスネットワークが作られ、それらの間で並行処理が行われる。このプログラムには以下の2種類の並行性が含まれている。

  • part/4が生成したリストを順次qsort/3でパイプライン的に処理
  • 2分割された各々のデータのqsort/3による並行処理

part/4は先頭から順番に大小のリストを作成していくが、qsort/3はリスト全体の作成を待つことなく先頭の値が決まったものから順次処理を行う。また、大きい数のリストと小さい数のリストはそれぞれ並行して処理され、次のpart/4とqsort/3の処理が行われていく。逐次処理言語に並行実行の機能を追加した多くの並行プログラミング言語と異なり、GHCではプログラマーが特に指定しなくてもアルゴリズム自身が持つ並行性が自然に表現できる。

拡張

KL1

KL1 (Kernel Language One) は、GHCのガード部を組み込み述語のみに制限したFlat GHCをもとに近山隆により設計された。KL1では、論理的並行性の記述にはGHCの機能をそのまま使い、それを複数のマシンに分散する物理的並行性（並列性）などをそれに付加するプラグマとして追加することで、論理的並行性と物理的並行性を別々に指定可能にし、プログラムの正しさに影響を与えることなく負荷分散の仕方などを変えられるように設計された。つまり、各種プラグマはプログラムの効率にのみ影響し、KL1はFlat GHCと同じ意味を持つ。KL1 は第五世代コンピュータプロジェクトで並列マシン PIM 上の処理系として開発された。UNIX上での処理系として KLIC がある。

Overlay GHC

慶應義塾大学で作られた処理系で、地球規模オペレーティングシステムでのシェル言語として開発された。KL1と同様、プロセスを処理するマシンやプロセスの優先順序をプラグマとして指定する。

関連項目

参考文献

  • Ueda, K. Guarded Horn Clauses. ICOT Technical Report TR-103, ICOT, Tokyo. 1985.
  • Ueda, K. Guarded Horn Clauses.(pdf) Doctoral Thesis. Information Engineering Course, University of Tokyo, 1986 2010-01-20 閲覧
  • 近山 隆, KL1入門. 1991. 2014-07-05 閲覧
  • 近山 隆, オペレーティングシステムPIMOSと核言語KL1.(pdf) 1992. 2014-07-05 閲覧
  • 上田 和紀, 並列プログラミング. ICOT Technical Manual TM-782, ICOT, Tokyo. 1989.
  • 上田 和紀, 並行論理プログラミング言語　GHC/KL1.(pdf) 2000. 2010-01-20 閲覧
  • 斉藤 賢爾, Overlay GHC.(pdf) 2008. 2014-07-05 閲覧
  • 古川 康一,溝口 文雄(編) 並列論理型言語GHCとその応用 (知識情報処理シリーズ) 共立出版 1987, ISBN 978-4320022669
  1. ↑ Ueda, K. Guarded Horn Clauses. ICOT Technical Report TR-103
  2. ↑ 近山 隆, オペレーティングシステムPIMOSと核言語KL1
  3. ↑ 古川 康一, 溝口 文雄（編） 並列論理型言語GHCとその応用 (知識情報処理シリーズ) p. 34

外部リンク



「http:///http:///mymemo.xyz/mymemo.xyz/wiki/index.php?title=Guarded_Horn_Clauses&oldid=135697」から取得