2.1.1 ゴール書換えモデル

KL1プログラムの実行は, ゴールをKL1プログラムで定義された規則に従って書 換えることにより行なわれる. KLIC処理系では, ゴールはゴールプールと呼ばれる領域におかれ, リダクションの実行により生成されるサブゴール群は再びゴールプールに入れられる. ゴール書換えモデルは, 基本的に図2.1に示すように, 以下の処理の繰り返しにより実現される.

1. ゴールプールからゴールを１つ取ってくる (ゴール呼びだし操作).
2. ゴール引数の値を, ガード部の規則にしたがってチェックする.
3. チェックに適合した節を１つ選んでそのボディ部を実行し, 生成されたサブゴール群をゴールプールに入れる (リダクション操作).

  
図 2.1: ゴールプールとリダクション操作