With the proliferation of massively parallel computers, the need for parallel execution of programs becomes apparent and essential. Nowadays, logic programming paradigm stands in the spotlight of numerous researchers, especially owing to potential parallelism inherent in logic programs.
From the motives described above, interests in AND/OR-parallel evaluation of logic programs have been rapidly growing. Thus many algorithms have been proposed for AND/OR-parallel execution of logic programs. Nevertheless, they have still been in controversy from the viewpoint of completeness. This is caused by the "absence of really formalized model for AND parallelism".
Therefore, we propose a formalization of AND-parallel execution of logic programs. The behavior of an execution method can be described in algebraic form. The algebraic specification is written in Milner's Calculus of Communicating Systems. From this approach, we can prove the correctness of backward execution methods mathematically.
For the purpose of easy construction of algebraic model, we introduce a new backward execution method called Path Model. The based models of the algebraic specification are followings: (1) Naive backtracking, (2) Chang's semi-intelligent backtracking, (3) Path Model for intelligent backtracking.
Since Path Model determines the actions of the backward execution in compile-time, it is appropriate for the algebraic specification. Furthermore the model gives small overhead to run-time determination of the actions. So the model can be implemented efficiently. To show the practical efficiency, we propose an automation for an AND-process.
Though the actions are determined in compile-time, we show that Path Model outperforms other backward execution models. The improvement comes from precise analysis of the AND-parallelism and the descriptive data structure of the principle of backward execution.
본 論文에서는 論理 프로그램의 AND-竝列 遂行을 위한 定型化의 한 方法으로서 여러가지 遂行 模型에 대하여 代數學的인 表現法을 提示하였다.
점차 널리 퍼지게 될 大規模 竝列 處理 컴퓨터에 對備하여 竝列性을 자연스럽게 內在하고 있는 論理 프로그래밍이 많은 注目을 받아왔고, 最近 10여년간 활발한 硏究가 이루어지고 있다.
특히 AND-竝列性과 관련된 몇가지 問題를 解決하기 위한 여러 硏究들이 있어왔는데, 이러한 方法들이 完全性에 많은 論難이 있었다. 본 論文에서는 이러한 現象이 AND-竝列 遂行을 다루는 方法들에 대한 數學的인 模型의 不在에 있다고 보았다.
본 論文에서는 AND-竝列 遂行 方法들을 위한 數學的인 模型을 세우기 위하여 Milner의 Calculus of Communicating Systems(CCS)을 이용하였다. CCS라는 잘 定義된 數學的 基盤을 사용하여 竝列 遂行 方法들을 代數學的으로 表現하였고, CCS로 表現된 竝列 遂行 方法에 대하여 본 論文에서는 論理 프로그램의 宣言的 意味(declarative semantics)에 근거한 正確性 證明을 하였다. 代數學的인 表現은 다음의 遂行 方法들을 對象으로 하였다. (1) 原始的인 백트랙킹 (2) Chang등의 半 知能的인 백트랙킹(Semi-intelligent backtracking) (3) 知能的인 後方向 遂行 模型인 Path Model. 論理 프로그램의 竝列 遂行 方法을 數學的으로 다루기 위한 基盤을 마련했다는 것이 본 論文의 주요한 貢獻이다.
새로운 竝列 遂行 模型인 Path Model은 컴파일 時間에 後方向 遂行의 行動을 決定할 수 있기 때문에 代數學的인 表現에 적절하다. 또한 實行時의 負擔을 적게 주므로 實行時의 效率을 높일 수 있다. 본 論文에서는 AND-프로세스를 위한 오토마타를 構成함으로서 提案된 模型이 실제적인 效率性을 가짐을 보였다. 또한 비록 컴파일 時間에 많은 行動을 決定하기는 하지만, AND-竝列性을 더 깊이 考察하고 그 原理를 정확히 表現하였기 때문에 Path Model이 다른 方法들보다 좋은 結果를 낸다는 것을 보였다. 旣存의 方法보다 더 效率的이고 더 知能的인 竝列 遂行 模型을 提示하였다는 것이 본 論文의 또 하나의 貢獻이다.
